Documentation Verification Report

Truncated

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean

Statistics

Metric	Count
Definitions `Truncated`, `instDecidableEqHom`, `δ`, `δ₂`, `σ`, `σ₂`	6
Theorems `initial_incl`, `initial_inclusion`, `δ₂_one_comp_σ₂_one`, `δ₂_one_comp_σ₂_one_assoc`, `δ₂_one_comp_σ₂_zero`, `δ₂_one_comp_σ₂_zero_assoc`, `δ₂_one_eq_const`, `δ₂_two_comp_σ₂_one`, `δ₂_two_comp_σ₂_one_assoc`, `δ₂_two_comp_σ₂_zero`, `δ₂_two_comp_σ₂_zero_assoc`, `δ₂_zero_comp_δ₂_two`, `δ₂_zero_comp_δ₂_two_assoc`, `δ₂_zero_comp_σ₂_one`, `δ₂_zero_comp_σ₂_one_assoc`, `δ₂_zero_comp_σ₂_zero`, `δ₂_zero_comp_σ₂_zero_assoc`, `δ₂_zero_eq_const`	18
Total	24

SimplexCategory

Definitions

Name	Category	Theorems
`Truncated` 📖	CompOp	110 math math: `SSet.Truncated.tensor_map_apply_snd`, `SSet.Truncated.mapHomotopyCategory_homMk`, `SSet.Truncated.Path.mk₂_arrow`, `SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk`, `CategoryTheory.nerve.functorOfNerveMap_map`, `SSet.Truncated.StrictSegal.spine_spineToSimplex`, `CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj`, `SSet.Truncated.Edge.map_fst`, `CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app`, `SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app`, `SSet.Truncated.Edge.CompStruct.d₂`, `SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app`, `SSet.Truncated.Path.map_arrow`, `SSet.Truncated.StrictSegal.spineToSimplex_spine`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `SSet.Truncated.HomotopyCategory₂.mk_surjective`, `CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj`, `CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj`, `CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app`, `SSet.Truncated.Edge.CompStruct.tensor_simplex_snd`, `SSet.Truncated.Edge.id_tensor_id`, `SSet.Truncated.spine_map_subinterval`, `CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left`, `CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app`, `SSet.Truncated.HomotopyCategory.mk_surjective`, `SSet.Truncated.StrictSegal.spine_δ_arrow_lt`, `SSet.Truncated.id_app`, `SSet.Truncated.spine_map_vertex`, `SSet.Truncated.Edge.CompStruct.tensor_simplex_fst`, `SSet.Truncated.Edge.map_associator_hom`, `SSet.Truncated.Edge.src_eq`, `SSet.Truncated.rightExtensionInclusion_right_as`, `Truncated.morphismProperty_eq_top`, `SSet.Truncated.StrictSegal.spine_δ_arrow_gt`, `SSet.Truncated.StrictSegal.spineInjective`, `CategoryTheory.SimplicialObject.isCoskeletal_iff`, `CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app`, `SSet.Truncated.Edge.map_whiskerLeft`, `SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id`, `SSet.Truncated.Edge.map_snd`, `SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂`, `SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk`, `SSet.Truncated.Edge.map_id`, `CategoryTheory.SimplicialObject.Truncated.trunc_obj_map`, `CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as`, `SSet.Truncated.StrictSegal.spineToSimplex_vertex`, `Truncated.initial_inclusion`, `SSet.Truncated.StrictSegal.spine_δ_vertex_ge`, `SSet.Truncated.StrictSegal.spineToSimplex_edge`, `SSet.Truncated.spine_arrow`, `SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_one`, `SSet.Truncated.Edge.mk'_edge`, `SSet.Truncated.comp_app_assoc`, `SSet.Truncated.Edge.map_tensorHom`, `SSet.Truncated.StrictSegal.spineToSimplex_arrow`, `SSet.Truncated.rightExtensionInclusion_left`, `SSet.Truncated.spine_vertex`, `CategoryTheory.SimplicialObject.Truncated.trunc_map_app`, `SSet.Truncated.mapHomotopyCategory_obj`, `SSet.Truncated.Edge.map_edge`, `SSet.Truncated.Edge.id_edge`, `SSet.Truncated.Path.arrow_src`, `SSet.horn.spineId_vertex_coe`, `SSet.Truncated.tensor_map_apply_fst`, `SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj`, `SSet.horn.spineId_arrow_coe`, `CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension`, `SSet.Truncated.Edge.tensor_edge`, `SSet.Truncated.Path.map_vertex`, `SSet.Truncated.StrictSegal.spine_δ_arrow_eq`, `CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map`, `SSet.Subcomplex.liftPath_arrow_coe`, `SSet.Truncated.HomotopyCategory.BinaryProduct.square`, `SSet.Truncated.Path₁.arrow_tgt`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge`, `SSet.Truncated.StrictSegal.spineToSimplex_interval`, `SSet.Truncated.hom_ext_iff`, `SSet.Truncated.Path.arrow_tgt`, `SSet.Subcomplex.liftPath_vertex_coe`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map`, `SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁`, `SSet.Truncated.Path.mk₂_vertex`, `SSet.Truncated.IsStrictSegal.spine_bijective`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero`, `SSet.Truncated.Edge.CompStruct.d₀`, `SSet.Truncated.Edge.map_whiskerRight`, `SSet.Truncated.comp_app`, `SSet.Truncated.Edge.CompStruct.map_simplex`, `CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map`, `SSet.OneTruncation₂.map_obj`, `SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map`, `SSet.Truncated.rightExtensionInclusion_hom_app`, `CategoryTheory.nerve.functorOfNerveMap_obj`, `SSet.Truncated.Path₁.arrow_src`, `SSet.Truncated.Edge.CompStruct.d₁`, `SSet.OneTruncation₂.id_edge`, `SSet.Truncated.StrictSegal.spine_δ_vertex_lt`, `SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk`, `SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj`, `Truncated.initial_incl`, `SSet.StrictSegal.isRightKanExtension`, `SSet.Truncated.IsStrictSegal.segal`, `SSet.Truncated.spine_injective`, `CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app`, `SSet.Truncated.Edge.CompStruct.idCompId_simplex`, `SSet.Truncated.Edge.tgt_eq`, `SSet.Truncated.StrictSegal.spineToSimplex_map`

SimplexCategory.Truncated

Definitions

Name	Category	Theorems
`instDecidableEqHom` 📖	CompOp	—
`δ` 📖	CompOp	—
`δ₂` 📖	CompOp	24 math math: `δ₂_two_comp_σ₂_one_assoc`, `δ₂_zero_comp_σ₂_zero`, `SSet.Truncated.Edge.CompStruct.d₂`, `δ₂_one_comp_σ₂_one`, `δ₂_zero_comp_δ₂_two_assoc`, `δ₂_zero_eq_const`, `δ₂_zero_comp_σ₂_zero_assoc`, `SSet.Truncated.Edge.src_eq`, `δ₂_zero_comp_δ₂_two`, `δ₂_zero_comp_σ₂_one_assoc`, `δ₂_one_eq_const`, `δ₂_one_comp_σ₂_zero`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_one`, `SSet.Truncated.Edge.mk'_edge`, `δ₂_two_comp_σ₂_zero`, `δ₂_two_comp_σ₂_zero_assoc`, `δ₂_one_comp_σ₂_one_assoc`, `δ₂_zero_comp_σ₂_one`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `SSet.Truncated.Edge.CompStruct.d₀`, `δ₂_one_comp_σ₂_zero_assoc`, `SSet.Truncated.Edge.CompStruct.d₁`, `δ₂_two_comp_σ₂_one`, `SSet.Truncated.Edge.tgt_eq`
`σ` 📖	CompOp	—
`σ₂` 📖	CompOp	15 math math: `δ₂_two_comp_σ₂_one_assoc`, `δ₂_zero_comp_σ₂_zero`, `δ₂_one_comp_σ₂_one`, `δ₂_zero_comp_σ₂_zero_assoc`, `δ₂_zero_comp_σ₂_one_assoc`, `δ₂_one_comp_σ₂_zero`, `SSet.Truncated.Edge.id_edge`, `δ₂_two_comp_σ₂_zero`, `δ₂_two_comp_σ₂_zero_assoc`, `δ₂_one_comp_σ₂_one_assoc`, `δ₂_zero_comp_σ₂_one`, `δ₂_one_comp_σ₂_zero_assoc`, `δ₂_two_comp_σ₂_one`, `SSet.OneTruncation₂.id_edge`, `SSet.Truncated.Edge.CompStruct.idCompId_simplex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`initial_incl` 📖	mathematical	—	`CategoryTheory.Functor.Initial` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `incl`	—	`CategoryTheory.Functor.initial_of_natIso` `initial_inclusion` `CategoryTheory.Functor.initial_of_comp_full_faithful` `CategoryTheory.ObjectProperty.full_ι` `CategoryTheory.ObjectProperty.faithful_ι`
`initial_inclusion` 📖	mathematical	—	`CategoryTheory.Functor.Initial` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `inclusion`	—	`CategoryTheory.zigzag_isConnected` `CategoryTheory.Zigzag.trans` `CategoryTheory.Zigzag.of_inv` `CategoryTheory.Zigzag.of_hom` `le_of_not_ge`
`δ₂_one_comp_σ₂_one` 📖	mathematical	`SimplexCategory.len`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.ObjectProperty.hom_ext` `SimplexCategory.δ_comp_σ_self`
`δ₂_one_comp_σ₂_one_assoc` 📖	mathematical	`SimplexCategory.len`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_one_comp_σ₂_one`
`δ₂_one_comp_σ₂_zero` 📖	mathematical	`SimplexCategory.len`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.ObjectProperty.hom_ext` `SimplexCategory.δ_comp_σ_succ`
`δ₂_one_comp_σ₂_zero_assoc` 📖	mathematical	`SimplexCategory.len`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_one_comp_σ₂_zero`
`δ₂_one_eq_const` 📖	mathematical	—	`δ₂` `Hom.tr` `SimplexCategory.const` `SimplexCategory.len` `SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—
`δ₂_two_comp_σ₂_one` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.ObjectProperty.hom_ext` `SimplexCategory.δ_comp_σ_succ'`
`δ₂_two_comp_σ₂_one_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_two_comp_σ₂_one`
`δ₂_two_comp_σ₂_zero` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.ObjectProperty.hom_ext` `SimplexCategory.δ_comp_σ_of_gt'`
`δ₂_two_comp_σ₂_zero_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_two_comp_σ₂_zero`
`δ₂_zero_comp_δ₂_two` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂`	—	—
`δ₂_zero_comp_δ₂_two_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_zero_comp_δ₂_two`
`δ₂_zero_comp_σ₂_one` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.ObjectProperty.hom_ext` `SimplexCategory.δ_comp_σ_of_le`
`δ₂_zero_comp_σ₂_one_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_zero_comp_σ₂_one`
`δ₂_zero_comp_σ₂_zero` 📖	mathematical	`SimplexCategory.len`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.ObjectProperty.hom_ext` `SimplexCategory.δ_comp_σ_self`
`δ₂_zero_comp_σ₂_zero_assoc` 📖	mathematical	`SimplexCategory.len`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ObjectProperty.FullSubcategory` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `δ₂` `σ₂`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ₂_zero_comp_σ₂_zero`
`δ₂_zero_eq_const` 📖	mathematical	—	`δ₂` `Hom.tr` `SimplexCategory.const` `SimplexCategory.len` `SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—

---

← Back to Index