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	180 math math: SSet.OneTruncation₂.nerveEquiv_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, SSet.Truncated.tensor_map_apply_snd, SSet.oneTruncation₂_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂, SSet.Truncated.sk.full, SSet.Truncated.HomotopyCategory.descOfTruncation_comp, SSet.Truncated.mapHomotopyCategory_homMk, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.oneTruncation₂_map, SSet.Truncated.Path.mk₂_arrow, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, SSet.OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, SSet.Truncated.StrictSegal.spine_spineToSimplex, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj, SSet.Truncated.sk_coreflective, SSet.Truncated.Edge.map_fst, CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, CategoryTheory.SimplicialObject.Truncated.cosk.full, SSet.Truncated.Edge.CompStruct.d₂, SSet.Truncated.liftOfStrictSegal.hδ'₂, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, SSet.Truncated.Path.map_arrow, CategoryTheory.SimplicialObject.Truncated.cosk.faithful, SSet.Truncated.StrictSegal.spineToSimplex_spine, SSet.Edge.ofTruncated_edge, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, 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.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, SSet.Truncated.Edge.id_tensor_id, SSet.Truncated.spine_map_subinterval, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂, SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top, CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app, SSet.Truncated.HomotopyCategory.mk_surjective, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal_hom, SSet.Truncated.id_app, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, SSet.Truncated.spine_map_vertex, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, SSet.Truncated.Edge.map_associator_hom, SSet.Truncated.Edge.src_eq, SSet.Truncated.rightExtensionInclusion_right_as, Truncated.morphismProperty_eq_top, CategoryTheory.SimplicialObject.Truncated.sk.full, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, SSet.Truncated.StrictSegal.spineInjective, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, 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.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, SSet.Truncated.Edge.map_snd, CategoryTheory.SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, SSet.Truncated.Edge.exists_of_simplex, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, SSet.Truncated.Edge.map_id, CategoryTheory.SimplicialObject.Truncated.trunc_obj_map, SSet.Truncated.hoFunctor₂_naturality, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, SSet.Truncated.liftOfStrictSegal.hσ'₀, SSet.Truncated.StrictSegal.spineToSimplex_vertex, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor, 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.liftOfStrictSegal.hδ'₁, 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.Truncated.liftOfStrictSegal_app_0, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, 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.cosk.faithful, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, SSet.Truncated.spine_surjective, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.SimplicialObject.Truncated.cosk_reflective, SSet.Subcomplex.liftPath_arrow_coe, SSet.Truncated.HomotopyCategory.BinaryProduct.square, SSet.Truncated.Path₁.arrow_tgt, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, SSet.Truncated.StrictSegal.spineToSimplex_interval, SSet.Truncated.hom_ext_iff, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.Truncated.Path.arrow_tgt, CategoryTheory.SimplicialObject.Truncated.sk_coreflective, SSet.Truncated.trunc_spine, CategoryTheory.SimplicialObject.Truncated.sk.faithful, SSet.Truncated.liftOfStrictSegal_app_1, SSet.Truncated.liftOfStrictSegal.hδ'₀, SSet.Truncated.cosk.full, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, SSet.Subcomplex.liftPath_vertex_coe, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, SSet.Truncated.cosk_reflective, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, SSet.Truncated.Path.mk₂_vertex, SSet.Truncated.IsStrictSegal.spine_bijective, SSet.OneTruncation₂.nerveHomEquiv_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, SSet.Truncated.Edge.CompStruct.exists_of_simplex, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Truncated.liftOfStrictSegal.hσ'₁, SSet.Truncated.Edge.CompStruct.d₀, SSet.Truncated.Edge.map_whiskerRight, SSet.Truncated.comp_app, SSet.Truncated.Edge.CompStruct.map_simplex, SSet.truncation_spine, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map, SSet.OneTruncation₂.map_obj, SSet.Truncated.HomotopyCategory.homToNerveMk_comp, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso, SSet.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.nerve.functorOfNerveMap_obj, SSet.Truncated.Path₁.arrow_src, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, SSet.Truncated.Edge.CompStruct.d₁, SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, SSet.OneTruncation₂.id_edge, SSet.Edge.toTruncated_id, SSet.Truncated.sk.faithful, SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, 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.HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one, SSet.Truncated.spine_injective, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app, SSet.Edge.toTruncated_edge, SSet.Truncated.Edge.CompStruct.idCompId_simplex, SSet.Truncated.Edge.tgt_eq, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero, SSet.Truncated.StrictSegal.spineToSimplex_map

SimplexCategory.Truncated

Definitions

Name	Category	Theorems
instDecidableEqHom 📖	CompOp	—
δ 📖	CompOp	—
δ₂ 📖	CompOp	29 math math: δ₂_two_comp_σ₂_one_assoc, δ₂_zero_comp_σ₂_zero, SSet.Truncated.Edge.CompStruct.d₂, SSet.Truncated.liftOfStrictSegal.hδ'₂, δ₂_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, SSet.Truncated.liftOfStrictSegal.hδ'₁, δ₂_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, SSet.Truncated.liftOfStrictSegal.hδ'₀, δ₂_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.liftOfStrictSegal.spineEquiv_f₂_arrow_one, SSet.Truncated.Edge.tgt_eq, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero
σ 📖	CompOp	—
σ₂ 📖	CompOp	17 math math: δ₂_two_comp_σ₂_one_assoc, δ₂_zero_comp_σ₂_zero, δ₂_one_comp_σ₂_one, δ₂_zero_comp_σ₂_zero_assoc, SSet.Truncated.liftOfStrictSegal.hσ'₀, δ₂_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, SSet.Truncated.liftOfStrictSegal.hσ'₁, δ₂_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 SimplexCategory.len 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 SimplexCategory.len 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 SimplexCategory.len 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 SimplexCategory.len 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 SimplexCategory.len 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 SimplexCategory.len 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