Documentation Verification Report

CompStructTruncated

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean

Statistics

Metric	Count
Definitions `Edge`, `compId`, `idComp`, `idCompId`, `map`, `simplex`, `edge`, `id`, `map`, `mk'`	10
Theorems `d₀`, `d₁`, `d₂`, `exists_of_simplex`, `ext`, `ext_iff`, `idCompId_simplex`, `map_simplex`, `exists_of_simplex`, `ext`, `ext_iff`, `id_edge`, `instSubsingleton`, `map_edge`, `map_id`, `mk'_edge`, `src_eq`, `tgt_eq`	18
Total	28

SSet.Truncated

Definitions

Name	Category	Theorems
`Edge` 📖	CompData	4 math math: `Edge.instSubsingleton`, `Quasicategory₂.fill21`, `HomotopyCategory₂.homMk_surjective`, `SSet.OneTruncation₂.reflQuiver_Hom`

SSet.Truncated.Edge

Definitions

Name	Category	Theorems
`edge` 📖	CompOp	18 math math: `SSet.OneTruncation₂.homOfEq_edge`, `CompStruct.d₂`, `SSet.Edge.ofTruncated_edge`, `ext_iff`, `src_eq`, `exists_of_simplex`, `mk'_edge`, `map_edge`, `id_edge`, `tensor_edge`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `CompStruct.d₀`, `SSet.OneTruncation₂.hom_ext_iff`, `CompStruct.d₁`, `SSet.OneTruncation₂.id_edge`, `SSet.Edge.toTruncated_edge`, `tgt_eq`
`id` 📖	CompOp	11 math math: `SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk`, `SSet.OneTruncation₂.reflQuiver_id`, `id_tensor_id`, `SSet.Truncated.HomotopyCategory.homMk_id`, `SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id`, `map_id`, `SSet.Truncated.HomotopyCategory₂.homMk_id`, `id_edge`, `SSet.Truncated.HomotopyCategory.BinaryProduct.square`, `SSet.Edge.toTruncated_id`, `CompStruct.idCompId_simplex`
`map` 📖	CompOp	13 math math: `SSet.Truncated.mapHomotopyCategory_homMk`, `CategoryTheory.nerve.functorOfNerveMap_map`, `map_fst`, `map_associator_hom`, `map_whiskerLeft`, `map_snd`, `SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `map_id`, `map_tensorHom`, `map_edge`, `map_whiskerRight`, `CompStruct.map_simplex`, `SSet.OneTruncation₂.map_map`
`mk'` 📖	CompOp	2 math math: `SSet.Truncated.HomotopyCategory.homToNerveMk_app_one`, `mk'_edge`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_simplex` 📖	mathematical	—	`edge`	—	—
`ext` 📖	—	`edge`	—	—	—
`ext_iff` 📖	mathematical	—	`edge`	—	`ext`
`id_edge` 📖	mathematical	—	`edge` `id` `CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.σ₂`	—	—
`instSubsingleton` 📖	mathematical	—	`SSet.Truncated.Edge`	—	`ext`
`map_edge` 📖	mathematical	—	`edge` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `map`	—	—
`map_id` 📖	mathematical	—	`map` `id` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op`	—	`ext` `CategoryTheory.FunctorToTypes.naturality`
`mk'_edge` 📖	mathematical	—	`edge` `CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.δ₂` `mk'`	—	—
`src_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.δ₂` `edge`	—	—
`tgt_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.δ₂` `edge`	—	—

SSet.Truncated.Edge.CompStruct

Definitions

Name	Category	Theorems
`compId` 📖	CompOp	—
`idComp` 📖	CompOp	—
`idCompId` 📖	CompOp	1 math math: `idCompId_simplex`
`map` 📖	CompOp	1 math math: `map_simplex`
`simplex` 📖	CompOp	9 math math: `d₂`, `tensor_simplex_snd`, `ext_iff`, `tensor_simplex_fst`, `exists_of_simplex`, `d₀`, `map_simplex`, `d₁`, `idCompId_simplex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`d₀` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.δ₂` `simplex` `SSet.Truncated.Edge.edge`	—	—
`d₁` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.δ₂` `simplex` `SSet.Truncated.Edge.edge`	—	—
`d₂` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.δ₂` `simplex` `SSet.Truncated.Edge.edge`	—	—
`exists_of_simplex` 📖	mathematical	—	`simplex`	—	`CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.op_comp`
`ext` 📖	—	`simplex`	—	—	—
`ext_iff` 📖	mathematical	—	`simplex`	—	`ext`
`idCompId_simplex` 📖	mathematical	—	`simplex` `SSet.Truncated.Edge.id` `idCompId` `CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.σ₂`	—	—
`map_simplex` 📖	mathematical	—	`simplex` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `SSet.Truncated.Edge.map` `map`	—	—

---

← Back to Index