Basic

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

Statistics

Metric	Count
Definitions SSet, Augmented, cosk, fullyFaithful, reflective, sk, fullyFaithful, coreflective, trunc, uliftFunctor, const, cosk, coskAdj, sk, skAdj, truncation, truncationCompTrunc, uliftFunctor	18
Theorems comp_app, comp_app_assoc, faithful, full, cosk_reflective, hom_ext, hom_ext_iff, id_app, faithful, full, sk_coreflective, comp_app, comp_app_assoc, comp_const, const_app, const_comp, hom_ext, hom_ext_iff, id_app, δ_comp_δ''_apply, δ_comp_δ'_apply, δ_comp_δ_apply, δ_comp_δ_self'_apply, δ_comp_δ_self_apply, δ_comp_σ_of_gt'_apply, δ_comp_σ_of_gt_apply, δ_comp_σ_of_le_apply, δ_comp_σ_self'_apply, δ_comp_σ_self_apply, δ_comp_σ_succ'_apply, δ_comp_σ_succ_apply, δ_naturality_apply, σ_comp_σ_apply, σ_naturality_apply	34
Total	52

SSet

Definitions

Name	Category	Theorems
Augmented 📖	CompOp	6 math math: Augmented.stdSimplex_map_right, Augmented.stdSimplex_obj_left, Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex, Augmented.stdSimplex_obj_right, Augmented.stdSimplex_obj_hom_app, Augmented.stdSimplex_map_left
const 📖	CompOp	32 math math: PtSimplex.RelStruct.δ_map_of_lt, stdSimplex.δ_zero_eq_const, ι₀_snd_assoc, PtSimplex.MulStruct.δ_map_of_gt, yonedaEquiv_symm_zero, sSetTopAdj_homEquiv_stdSimplex_zero, PtSimplex.RelStruct.δ_castSucc_map, stdSimplex.δ_zero_toSSetObjI, PtSimplex.RelStruct.δ_castSucc_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map_assoc, RelativeMorphism.ofSimplex₀_map, PtSimplex.MulStruct.δ_succ_succ_map, ι₀_snd, PtSimplex.MulStruct.δ_succ_castSucc_map, ι₁_snd_assoc, ι₁_snd, comp_const, const_app, PtSimplex.MulStruct.δ_map_of_lt, stdSimplex.δ_one_toSSetObjI, yonedaEquiv_const, const_comp, PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, TopCat.toSSet_map_const, stdSimplex.δ_one_eq_const, Subcomplex.ofSimplex_ι, RelativeMorphism.const_map, PtSimplex.RelStruct.δ_succ_map, PtSimplex.RelStruct.δ_map_of_gt, PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, PtSimplex.RelStruct.δ_succ_map_assoc, PtSimplex.MulStruct.δ_castSucc_castSucc_map
cosk 📖	CompOp	—
coskAdj 📖	CompOp	1 math math: Truncated.cosk_reflective
sk 📖	CompOp	—
skAdj 📖	CompOp	1 math math: Truncated.sk_coreflective
truncation 📖	CompOp	30 math math: OneTruncation₂.nerveEquiv_apply, OneTruncation₂.ofNerve₂.natIso_hom_app_map, Truncated.HomotopyCategory.descOfTruncation_comp, instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, Truncated.sk_coreflective, Edge.ofTruncated_edge, OneTruncation₂.ofNerve₂.natIso_hom_app_obj, OneTruncation₂.nerveEquiv_symm_apply_map, Truncated.HomotopyCategory.descOfTruncation_map_homMk, Truncated.HomotopyCategory.homToNerveMk_app_one, horn.spineId_vertex_coe, horn.spineId_arrow_coe, Subcomplex.liftPath_arrow_coe, Truncated.HomotopyCategory.homToNerveMk_app_edge, OneTruncation₂.ofNerve₂.natIso_inv_app_map, OneTruncation₂.nerveEquiv_symm_apply_obj, Subcomplex.liftPath_vertex_coe, Truncated.cosk_reflective, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, OneTruncation₂.nerveHomEquiv_apply, Truncated.HomotopyCategory.homToNerveMk_app_zero, truncation_spine, Truncated.HomotopyCategory.homToNerveMk_comp, Edge.toTruncated_id, StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, Truncated.HomotopyCategory.descOfTruncation_obj_mk, Truncated.HomotopyCategory.homToNerveMk_comp_assoc, Edge.toTruncated_edge
truncationCompTrunc 📖	CompOp	—
uliftFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—
comp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.NatTrans.app SSet CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_app
comp_const 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types const	—	—
const_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types const CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.const SimplexCategory.len SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	—	—
const_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types const CategoryTheory.NatTrans.app Opposite.op	—	hom_ext CategoryTheory.types_ext CategoryTheory.FunctorToTypes.naturality
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types	—	—	CategoryTheory.SimplicialObject.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types	—	hom_ext
id_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.CategoryStruct.id SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—
δ_comp_δ''_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types Fin.le_iff_val_le_val	—	Fin.le_iff_val_le_val CategoryTheory.SimplicialObject.δ_comp_δ''
δ_comp_δ'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ'
δ_comp_δ_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ
δ_comp_δ_self'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ_self'
δ_comp_δ_self_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ_self
δ_comp_σ_of_gt'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE Nat.instPartialOrder contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Nat.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instAddCommMonoid Nat.instPreorder Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instLinearOrder IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add lt_of_lt_of_le	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add lt_of_lt_of_le CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'
δ_comp_σ_of_gt_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_of_gt
δ_comp_σ_of_le_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_of_le
δ_comp_σ_self'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_self'
δ_comp_σ_self_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_self
δ_comp_σ_succ'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_succ'
δ_comp_σ_succ_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_succ
δ_naturality_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.SimplicialObject.δ	—	CategoryTheory.SimplicialObject.δ_naturality
σ_comp_σ_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.σ CategoryTheory.types	—	CategoryTheory.SimplicialObject.σ_comp_σ
σ_naturality_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.σ_naturality

SSet.Truncated

Definitions

Name	Category	Theorems
cosk 📖	CompOp	3 math math: cosk.faithful, cosk.full, cosk_reflective
sk 📖	CompOp	3 math math: sk.full, sk_coreflective, sk.faithful
trunc 📖	CompOp	7 math math: Path.mk₂_arrow, SSet.horn.spineId_vertex_coe, SSet.horn.spineId_arrow_coe, SSet.Subcomplex.liftPath_arrow_coe, trunc_spine, SSet.Subcomplex.liftPath_vertex_coe, Path.mk₂_vertex
uliftFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.CategoryStruct.comp SSet.Truncated CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—
comp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.NatTrans.app SSet.Truncated CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_app
cosk_reflective 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor SSet.Truncated CategoryTheory.Functor.category Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.comp SSet cosk SSet.truncation CategoryTheory.Functor.id CategoryTheory.Adjunction.counit SSet.coskAdj	—	CategoryTheory.SimplicialObject.Truncated.cosk_reflective CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types	—	—	CategoryTheory.NatTrans.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types	—	hom_ext
id_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.CategoryStruct.id SSet.Truncated CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—
sk_coreflective 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor SSet.Truncated CategoryTheory.Functor.category Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.id CategoryTheory.Functor.comp SSet sk SSet.truncation CategoryTheory.Adjunction.unit SSet.skAdj	—	CategoryTheory.SimplicialObject.Truncated.sk_coreflective CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self

SSet.Truncated.cosk

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful SSet.Truncated CategoryTheory.Functor.category Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types SSet SSet.Truncated.cosk	—	CategoryTheory.SimplicialObject.Truncated.cosk.faithful CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self
full 📖	mathematical	—	CategoryTheory.Functor.Full SSet.Truncated CategoryTheory.Functor.category Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types SSet SSet.Truncated.cosk	—	CategoryTheory.SimplicialObject.Truncated.cosk.full CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self

SSet.Truncated.coskAdj

Definitions

Name	Category	Theorems
reflective 📖	CompOp	—

SSet.Truncated.sk

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful SSet.Truncated CategoryTheory.Functor.category Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types SSet SSet.Truncated.sk	—	CategoryTheory.SimplicialObject.Truncated.sk.faithful CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self
full 📖	mathematical	—	CategoryTheory.Functor.Full SSet.Truncated CategoryTheory.Functor.category Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types SSet SSet.Truncated.sk	—	CategoryTheory.SimplicialObject.Truncated.sk.full CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self

SSet.Truncated.skAdj

Definitions

Name	Category	Theorems
coreflective 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
SSet 📖	CompOp	392 math math: SSet.OneTruncation₂.nerveEquiv_apply, SSet.stdSimplex.objMk_bijective, SSet.Subcomplex.lift_ι, SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, SSet.RelativeMorphism.botEquiv_symm_apply_map, SSet.Subcomplex.prod_top_le_unionProd, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, SSet.PtSimplex.RelStruct.δ_map_of_lt, SSet.Subcomplex.toRange_ι, SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor, SSet.Subcomplex.prodIso_hom, SSet.horn₃₁.desc.multicofork_π_two, SSet.stdSimplex.δ_zero_eq_const, SSet.Truncated.sk.full, SSet.ι₀_snd_assoc, SSet.Truncated.HomotopyCategory.descOfTruncation_comp, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, SSet.Subcomplex.mem_unionProd_iff, SSet.modelCategoryQuillen.I_le_monomorphisms, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.horn.faceSingletonComplIso_inv_ι_assoc, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, SSet.Subcomplex.fromPreimage_ι_assoc, SSet.Subcomplex.toSSetFunctor_map, SSet.Subcomplex.unionProd.isPushout, SSet.iSup_subcomplexOfSimplex_prod_eq_top, SSet.stdSimplex.obj₀Equiv_symm_apply, SSet.OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, SSet.opFunctorCompOpFunctorIso_inv_app_app, SSet.modelCategoryQuillen.mono_of_cofibration, SSet.horn₃₁.exists_desc, SSet.Subcomplex.range_eq_ofSimplex, SSet.PtSimplex.MulStruct.δ_map_of_gt, SSet.instHasDimensionLETensorUnitOfNatNat, SimplexCategory.toTopHomeo_symm_naturality, SSet.tensorHom_app_apply, SSet.Truncated.sk_coreflective, CategoryTheory.nerveFunctor.faithful, SSet.hoFunctor.preservesTerminal', SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, SSet.Subcomplex.toImage_ι, SSet.stdSimplex.objMk₁_bijective, SSet.horn.yonedaEquiv_ι, SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, SSet.horn₃₂.desc.multicofork_π_one, SSet.yonedaEquiv_symm_zero, SSet.Subcomplex.topIso_inv_app_coe, SSet.prodStdSimplex.orderHomOfSimplex_coe, SSet.horn₃₂.ι₁_desc, SSet.prodStdSimplex.nonDegenerateEquiv₁_snd, SSet.Subcomplex.homOfLE_refl, SSet.opFunctorCompOpFunctorIso_hom_app_app, SSet.hasDimensionLT_prod, SimplexCategory.toTopHomeo_naturality_apply, SSet.instIsStableUnderFilteredColimitsMonomorphisms, SSet.Subcomplex.toRange_ι_assoc, SSet.RelativeMorphism.Homotopy.h₀_assoc, SSet.Subcomplex.unionProd.image_β_inv, instIsLeftAdjointSSetTopCatToTop, SSet.prodStdSimplex.objEquiv_apply_fst, SSet.stdSimplex.map_id, SSet.Subcomplex.lift_ι_assoc, SSet.Homotopy.h₁_assoc, SSet.modelCategoryQuillen.fibrations_eq, SSet.Subcomplex.unionProd.symmIso_inv, SSet.modelCategoryQuillen.cofibrations_eq, SSet.opEquivalence_inverse, SSet.stdSimplex.objMk₁_surjective, SSet.instFiniteTensorUnit, SSet.Edge.ofTruncated_edge, SSet.horn₂₂.sq, SSet.nonDegenerateEquivOfIso_symm_apply_coe, SSet.Subcomplex.image_id, SSet.stdSimplex.ext_iff, SSet.opFunctor_map, SSet.Subcomplex.toImage_ι_assoc, SSet.Subcomplex.topIso_inv_ι, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, sSetTopAdj_homEquiv_stdSimplex_zero, SSet.horn₃₁.ι₂_desc_assoc, SSet.prod_δ_snd, SSet.Subcomplex.ofSimplexProd_eq_range, SSet.stdSimplex.face_eq_ofSimplex, SSet.PtSimplex.RelStruct.δ_castSucc_map, SSet.prod_σ_fst, SSet.stdSimplex.obj₀Equiv_apply, SSet.horn₃₁.desc.multicofork_pt, SSet.prodStdSimplex.objEquiv_δ_apply, SSet.horn.faceSingletonComplIso_inv_ι, SSet.Subcomplex.toSSetFunctor_obj, SSet.stdSimplex.δ_zero_toSSetObjI, SSet.horn₃₁.ι₃_desc_assoc, SSet.Subcomplex.instSubsingletonHomToSSetBot, SSet.instBalanced, SSet.Subcomplex.unionProd.image_β_hom, SSet.prodStdSimplex.objEquiv_naturality, TopCat.toSSetObj₀Equiv_symm_apply, SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, SSet.stdSimplex.spineId_arrow_apply_zero, SSet.prod_δ_fst, SSet.comp_app_assoc, SSet.Subcomplex.eqToIso_hom, SSet.yonedaEquiv_symm_comp, SSet.stdSimplex.range_δ, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SSet.stdSimplex.objMk₁_apply, SSet.id_app, SSet.instFiniteTensorObj, SSet.stdSimplex.δ_objEquiv_symm_apply, SSet.stdSimplex.toSSetObj_app_const_zero, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, SSet.Augmented.stdSimplex_map_right, SSet.PtSimplex.MulStruct.δ_succ_succ_map, SSet.Subcomplex.homOfLE_comp_assoc, SSet.prodStdSimplex.objEquiv_apply_snd, SSet.Subcomplex.unionProd.symmIso_hom, SSet.Subcomplex.instEpiToImage, SSet.hoFunctor.unitHomEquiv_eq, SSet.Augmented.stdSimplex_obj_left, SSet.instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType, SSet.stdSimplex.σ_objMk₁_of_le, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.ι₁_app_snd_apply, SSet.stdSimplex.objMk₁_injective, SSet.horn.spineId_map_hornInclusion, SSet.instFiniteCoprod, SSet.horn₃₁.desc.multicofork_π_zero_assoc, SSet.horn_obj, SSet.finite_of_isColimit, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, SSet.Subcomplex.yonedaEquiv_coe, CategoryTheory.hoFunctor.preservesFiniteProducts, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, SSet.Subcomplex.homOfLE_ι_assoc, SSet.prod_map_fst, SSet.whiskerRight_app_apply, SSet.Subcomplex.unionProd.ι₂_ι, SSet.rightUnitor_inv_app_apply, SSet.stdSimplex.face_obj, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, SSet.modelCategoryQuillen.horn_ι_mem_J, CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex, SSet.stdSimplex.map_apply, SSet.ι₀_snd, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, SSet.Homotopy.h₀, CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor, SSet.RelativeMorphism.botEquiv_apply, SSet.Subcomplex.image_comp, SSet.stdSimplex.yonedaEquiv_symm_app_objEquiv_symm, SSet.horn₂₀.sq, SSet.horn₃₂.exists_desc, SSet.stdSimplex.mem_face_iff, SSet.hoFunctor.preservesTerminal, CategoryTheory.SimplicialThickening.functor_map, SSet.Subcomplex.unionProd.ι₁_ι, SimplexCategory.toTopHomeo_symm_naturality_apply, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, SSet.instIsStableUnderCobaseChangeMonomorphisms, SSet.ι₁_snd_assoc, SSet.horn.edge_coe, CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy, SSet.horn₃₁.ι₂_desc, SSet.modelCategoryQuillen.cofibration_of_mono, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, SSet.stdSimplex.isoNerve_hom_app_apply, SSet.stdSimplex.faceSingletonComplIso_hom_ι, SSet.instHasDimensionLETensorObjHAddNat, SSet.ι₁_app_fst, SSet.ι₁_snd, SSet.stdSimplex.objMk₁_of_castSucc_lt, SSet.hasDimensionLT_of_isColimit, SSet.whiskerLeft_app_apply, SSet.comp_app, CategoryTheory.nerveFunctor_map, SSet.stdSimplex.σ_objEquiv_symm_apply, SSet.Subcomplex.prod_obj, SSet.horn₃₂.ι₃_desc, SSet.comp_const, TopCat.toSSetObj₀Equiv_apply, SSet.stdSimplex.instFiniteObjOppositeSimplexCategory, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, SSet.Subcomplex.prod_le_unionProd, SSet.RelativeMorphism.comm_assoc, SSet.Subcomplex.instMonoToRange, SSet.Subcomplex.unionProd.ι₁_ι_assoc, SSet.modelCategoryQuillen.cofibration_iff, SSet.instHasDimensionLTTensorObjHAddNat, SSet.horn₃₂.ι₀_desc, SSet.Subcomplex.homOfLE_ι, SSet.face_le_horn, CategoryTheory.hoFunctor.preservesBinaryProducts, SSet.stdSimplex.objMk₁_of_le_castSucc, SimplexCategory.toTopHomeo_naturality, SSet.Subcomplex.image_eq_range, SSet.RelativeMorphism.comm, SSet.PtSimplex.MulStruct.δ_map_of_lt, SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk, SSet.stdSimplex.monotone_apply, SSet.horn.faceι_ι, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, SSet.stdSimplex.δ_one_toSSetObjI, SSet.prodStdSimplex.objEquiv_map_apply, SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, instIsRightAdjointSSetTopCatToSSet, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, SSet.Subcomplex.homOfLE_comp, SSet.horn.edge₃_coe_down, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, SSet.Subcomplex.topIso_inv_ι_assoc, SSet.horn₂₁.isPushout, SSet.horn_eq_iSup, SSet.Subcomplex.unionProd.ι₂_ι_assoc, SSet.yonedaEquiv_const, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, SSet.prodStdSimplex.nonDegenerateEquiv₁_fst, SSet.range_eq_iSup_sigma_ι, SSet.Subcomplex.BicartSq.isPushout, SSet.Subcomplex.range_comp, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, SSet.stdSimplex.objEquiv_symm_comp, SSet.Subcomplex.eqToIso_inv, SSet.Subcomplex.prod_monotone, SSet.ι₀_comp_assoc, SSet.Subcomplex.instMonoι, SSet.horn₃₂.ι₁_desc_assoc, SSet.ι₀_comp, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.Homotopy.h₀_assoc, SSet.opEquivalence_unitIso, SSet.Augmented.stdSimplex_obj_hom_app, SSet.horn.faceι_ι_assoc, SSet.Homotopy.h₁, SSet.stdSimplex.δ_objMk₁_of_le, SSet.prodStdSimplex.le_orderHomOfSimplex, SSet.RelativeMorphism.Homotopy.h₁_assoc, SSet.Subcomplex.prodIso_inv, CategoryTheory.nerveFunctor.full, SSet.Subcomplex.unionProd.preimage_β_inv, SSet.stdSimplex.yonedaEquiv_map, SSet.RelativeMorphism.Homotopy.ofEq_h, SSet.horn_obj_zero, SSet.horn.spineId_vertex_coe, SSet.rightUnitor_hom_app_apply, CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor, SSet.horn.multicoequalizerDiagram, SSet.horn.spineId_arrow_coe, SSet.iSup_range_eq_top_of_isColimit, SSet.stdSimplex.objEquiv_toOrderHom_apply, SSet.ι₁_fst, SSet.const_comp, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, SSet.ι₀_app_snd_apply, SSet.Truncated.cosk.faithful, SSet.horn₃₁.desc.multicofork_π_zero, SSet.Subcomplex.unionProd.preimage_β_hom, SSet.Subcomplex.liftPath_arrow_coe, SSet.horn₂₀.isPushout, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, TopCat.toSSet_map_const, SSet.Quasicategory.hornFilling, SSet.prodStdSimplex.nonDegenerate_max_dim_iff, SSet.stdSimplex.instFiniteObjSimplexCategory, SSet.Subcomplex.prod_le_top_prod, SSet.stdSimplex.objMk_apply, SSet.horn₃₂.desc.multicofork_π_three, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.RelativeMorphism.Homotopy.h₀, SSet.horn₃₁.ι₀_desc_assoc, SSet.nonDegenerateEquivOfIso_apply_coe, SSet.modelCategoryQuillen.boundary_ι_mem_I, SSet.Augmented.stdSimplex_map_left, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, SSet.RelativeMorphism.Homotopy.precomp_h, SSet.Finite.exists_epi_from_isCardinalPresentable, SSet.ι₀_fst, SSet.stdSimplex.δ_one_eq_const, SSet.associator_hom_app_apply, SSet.Truncated.cosk.full, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, SSet.Subcomplex.liftPath_vertex_coe, SSet.modelCategoryQuillen.J_le_monomorphisms, CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, SSet.boundary_eq_iSup, SSet.Subcomplex.unionProd.bicartSq, SSet.prod_σ_snd, SSet.RelativeMorphism.Homotopy.h₁, SSet.stdSimplex.spineId_vertex, SSet.Subcomplex.range_tensorHom, SSet.stdSimplex.objMk₁_apply_eq_zero_iff, SSet.Truncated.cosk_reflective, CategoryTheory.hoFunctor.preservesBinaryProduct, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, SSet.RelativeMorphism.Homotopy.postcomp_h, SSet.stdSimplex.σ_objMk₁_of_lt, SSet.stdSimplex.face_inter_face, CategoryTheory.nerveFunctor_obj, SSet.stdSimplex.mem_nonDegenerate_iff_mono, SSet.horn₃₂.desc.multicofork_pt, SSet.prodStdSimplex.strictMono_orderHomOfSimplex, SSet.Subcomplex.mono_homOfLE, SSet.horn₂₂.isPushout, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, SSet.yonedaEquiv_comp, SSet.stdSimplex.spineId_arrow_apply_one, SSet.Quasicategory.hornFilling', SSet.OneTruncation₂.nerveHomEquiv_apply, SSet.Subcomplex.instEpiToRange, SSet.instFiniteSigmaObjOfFinite, SSet.RelativeMorphism.Homotopy.rel, SSet.horn.primitiveEdge_coe_down, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, SSet.Subcomplex.range_eq_top_iff, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Subcomplex.fromPreimage_ι, SSet.stdSimplex.face_le_face_iff, SSet.Finite.instIsFinitelyPresentable, SSet.RelativeMorphism.Homotopy.refl_h, SSet.horn₃₁.ι₃_desc, SSet.truncation_spine, SSet.PtSimplex.RelStruct.δ_succ_map, SSet.stdSimplex.δ_objMk₁_of_lt, SSet.Truncated.HomotopyCategory.homToNerveMk_comp, CategoryTheory.SimplicialThickening.functor_id, SSet.Subcomplex.top_prod_le_unionProd, SSet.modelCategoryQuillen.fibration_iff, SSet.hasDimensionLE_prod, SSet.ι₁_fst_assoc, SSet.stdSimplex.objMk₁_apply_eq_one_iff, SSet.Subcomplex.topIso_hom, SSet.stdSimplex.toSSetObj_app_const_one, SSet.Edge.toTruncated_id, SSet.horn.ι_ι_assoc, SSet.Truncated.sk.faithful, SSet.opEquivalence_counitIso, SSet.leftUnitor_hom_app_apply, SSet.RelativeMorphism.comp_map, SSet.prod_map_snd, SSet.horn₃₂.desc.multicofork_π_zero, SSet.stdSimplex.objEquiv_symm_apply, SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.KanComplex.hornFilling, SSet.PtSimplex.RelStruct.δ_map_of_gt, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, SSet.associator_inv_app_apply, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, SSet.horn.ι_ι, SSet.Subcomplex.prod_le_prod_top, CategoryTheory.hoFunctor.isIso_prodComparison, SSet.horn₃₁.ι₀_desc, CategoryTheory.SimplicialThickening.functor_obj_as, SSet.instIsRegularEpiCategory, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SSet.horn.const_val_apply, SSet.horn₃₁.desc.multicofork_π_three, CategoryTheory.nerveAdjunction.isIso_counit, SSet.horn₃₂.ι₃_desc_assoc, SSet.horn₂₁.sq, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, SSet.instFinitePullback, SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.SimplicialThickening.functor_comp, SSet.horn.primitiveTriangle_coe, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, SSet.stdSimplex.face_singleton_compl, SSet.ι₀_app_fst, SSet.horn₃₂.ι₀_desc_assoc, SSet.Edge.toTruncated_edge, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc, SSet.range_eq_iSup_of_isColimit, SSet.Subcomplex.instIsIsoToRangeOfMono, SSet.ι₁_comp_assoc, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.opEquivalence_functor, SSet.stdSimplex.isoNerve_inv_app_apply, SSet.instFiniteInitial, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map, SSet.RelativeMorphism.Homotopy.rel_assoc

---

← Back to Index