StdSimplex

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

Statistics

Metric	Count
Definitions stdSimplex, S1, instInhabited, instInhabitedTruncated, stdSimplex, asOrderHom, const, edge, face, facePairIso, faceRepresentableBy, faceSingletonComplIso, faceSingletonIso, finSuccAboveOrderIsoFinset, instDecidableEqHomObjSimplexCategoryOfOppositeOp, instDecidableEqObjOppositeSimplexCategory, instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat, isoNerve, isoOfRepresentableBy, nonDegenerateEquiv, objEquiv, objMk, obj₀Equiv, triangle, yonedaEquiv, «termΔ[_]»	26
Theorems stdSimplex_map_left, stdSimplex_map_right, stdSimplex_obj_hom_app, stdSimplex_obj_left, stdSimplex_obj_right, range_eq_ofSimplex, yonedaEquiv_coe, coe_edge_down_toOrderHom, coe_triangle_down_toOrderHom, const_down_toOrderHom, ext, ext_iff, faceSingletonComplIso_hom_ι, faceSingletonComplIso_hom_ι_assoc, faceSingletonIso_one_hom_comp_ι_eq_δ, faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, faceSingletonIso_zero_hom_comp_ι_eq_δ, faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, face_eq_ofSimplex, face_inter_face, face_le_face_iff, face_obj, face_singleton_compl, instFiniteObjOppositeSimplexCategory, instFiniteObjSimplexCategory, instFiniteToSSetOfSimplex, instHasDimensionLEObjSimplexCategoryMk, isoNerve_hom_app_apply, isoNerve_inv_app_apply, map_apply, map_id, mem_face_iff, mem_nonDegenerate_iff_mono, mem_nonDegenerate_iff_strictMono, monotone_apply, nonDegenerateEquiv_apply_apply, nonDegenerateEquiv_symm_apply_coe, objEquiv_symm_apply, objEquiv_symm_comp, objEquiv_symm_mem_nonDegenerate_iff_mono, objEquiv_toOrderHom_apply, objMk_apply, obj₀Equiv_apply, obj₀Equiv_symm_apply, obj₀Equiv_symm_mem_face_iff, ofSimplex_yonedaEquiv_δ, range_δ, yonedaEquiv_map, yonedaEquiv_comp	49
Total	75

SSet

Definitions

Name	Category	Theorems
S1 📖	CompOp	—
instInhabited 📖	CompOp	—
instInhabitedTruncated 📖	CompOp	—
stdSimplex 📖	CompOp	133 math math: stdSimplex.mem_nonDegenerate_iff_strictMono, PtSimplex.RelStruct.δ_map_of_lt, ι₀_snd_assoc, instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, horn.faceSingletonComplIso_inv_ι_assoc, stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, stdSimplex.obj₀Equiv_symm_apply, Subcomplex.range_eq_ofSimplex, PtSimplex.MulStruct.δ_map_of_gt, prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, horn.yonedaEquiv_ι, Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, prodStdSimplex.orderHomOfSimplex_coe, RelativeMorphism.Homotopy.h₀_assoc, prodStdSimplex.objEquiv_apply_fst, stdSimplex.map_id, horn₂₂.sq, stdSimplex.ext_iff, prodStdSimplex.strictMono_orderHomOfSimplex_iff, Subcomplex.ofSimplexProd_eq_range, stdSimplex.face_eq_ofSimplex, PtSimplex.RelStruct.δ_castSucc_map, stdSimplex.obj₀Equiv_apply, prodStdSimplex.objEquiv_δ_apply, horn.faceSingletonComplIso_inv_ι, prodStdSimplex.objEquiv_naturality, modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, stdSimplex.spineId_arrow_apply_zero, stdSimplex.range_δ, PtSimplex.RelStruct.δ_castSucc_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map_assoc, Augmented.stdSimplex_map_right, PtSimplex.MulStruct.δ_succ_succ_map, prodStdSimplex.objEquiv_apply_snd, Augmented.stdSimplex_obj_left, stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, horn.spineId_map_hornInclusion, horn_obj, ι₀_fst_assoc, ι₁_comp, Subcomplex.yonedaEquiv_coe, stdSimplex.face_obj, stdSimplex.nonDegenerateEquiv_apply_apply, modelCategoryQuillen.horn_ι_mem_J, stdSimplex.map_apply, ι₀_snd, PtSimplex.MulStruct.δ_succ_castSucc_map, horn₂₀.sq, stdSimplex.mem_face_iff, stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, ι₁_snd_assoc, horn.edge_coe, stdSimplex.isoNerve_hom_app_apply, stdSimplex.faceSingletonComplIso_hom_ι, ι₁_app_fst, ι₁_snd, stdSimplex.instFiniteObjOppositeSimplexCategory, face_le_horn, PtSimplex.MulStruct.δ_map_of_lt, stdSimplex.instHasDimensionLEObjSimplexCategoryMk, stdSimplex.monotone_apply, horn.faceι_ι, prodStdSimplex.objEquiv_map_apply, stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, horn.edge₃_coe_down, horn₂₁.isPushout, horn_eq_iSup, stdSimplex.obj₀Equiv_symm_mem_face_iff, prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, stdSimplex.objEquiv_symm_comp, ι₀_comp_assoc, ι₀_comp, Augmented.stdSimplex_obj_hom_app, horn.faceι_ι_assoc, RelativeMorphism.Homotopy.h₁_assoc, stdSimplex.yonedaEquiv_map, RelativeMorphism.Homotopy.ofEq_h, horn_obj_zero, horn.spineId_vertex_coe, horn.multicoequalizerDiagram, horn.spineId_arrow_coe, stdSimplex.objEquiv_toOrderHom_apply, ι₁_fst, PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, horn₂₀.isPushout, stdSimplex.ofSimplex_yonedaEquiv_δ, prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Quasicategory.hornFilling, stdSimplex.instFiniteObjSimplexCategory, stdSimplex.objMk_apply, RelativeMorphism.Homotopy.h₀, modelCategoryQuillen.boundary_ι_mem_I, Augmented.stdSimplex_map_left, stdSimplex.faceSingletonComplIso_hom_ι_assoc, RelativeMorphism.Homotopy.precomp_h, ι₀_fst, boundary_eq_iSup, RelativeMorphism.Homotopy.h₁, stdSimplex.spineId_vertex, RelativeMorphism.Homotopy.postcomp_h, stdSimplex.face_inter_face, stdSimplex.mem_nonDegenerate_iff_mono, horn₂₂.isPushout, prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, yonedaEquiv_comp, stdSimplex.spineId_arrow_apply_one, Quasicategory.hornFilling', RelativeMorphism.Homotopy.rel, horn.primitiveEdge_coe_down, stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, stdSimplex.face_le_face_iff, RelativeMorphism.Homotopy.refl_h, PtSimplex.RelStruct.δ_succ_map, ι₁_fst_assoc, horn.ι_ι_assoc, stdSimplex.objEquiv_symm_apply, KanComplex.hornFilling, PtSimplex.RelStruct.δ_map_of_gt, stdSimplex.nonDegenerateEquiv_symm_apply_coe, horn.ι_ι, PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, horn.const_val_apply, horn₂₁.sq, horn.primitiveTriangle_coe, stdSimplex.face_singleton_compl, ι₀_app_fst, ι₁_comp_assoc, PtSimplex.RelStruct.δ_succ_map_assoc, stdSimplex.isoNerve_inv_app_apply, PtSimplex.MulStruct.δ_castSucc_castSucc_map, RelativeMorphism.Homotopy.rel_assoc
yonedaEquiv 📖	CompOp	7 math math: Subcomplex.range_eq_ofSimplex, horn.yonedaEquiv_ι, Subcomplex.ofSimplexProd_eq_range, Subcomplex.yonedaEquiv_coe, stdSimplex.yonedaEquiv_map, stdSimplex.ofSimplex_yonedaEquiv_δ, yonedaEquiv_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
yonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app	—	—

SSet.Augmented

Definitions

Name	Category	Theorems
stdSimplex 📖	CompOp	6 math math: stdSimplex_map_right, stdSimplex_obj_left, StandardSimplex.nonempty_extraDegeneracy_stdSimplex, stdSimplex_obj_right, stdSimplex_obj_hom_app, stdSimplex_map_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stdSimplex_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex CategoryTheory.Limits.terminal Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.terminal.from CategoryTheory.Functor.map SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex	—	—
stdSimplex_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex CategoryTheory.Limits.terminal Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.terminal.from CategoryTheory.Functor.map SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex CategoryTheory.Comma.right	—	—
stdSimplex_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id SSet SSet.largeCategory SSet.stdSimplex CategoryTheory.SimplicialObject.const CategoryTheory.Limits.terminal CategoryTheory.Comma.hom SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex CategoryTheory.Limits.terminal.from	—	—
stdSimplex_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex SSet SSet.largeCategory SSet.stdSimplex	—	—
stdSimplex_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex CategoryTheory.Limits.terminal	—	—

SSet.Subcomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_eq_ofSimplex 📖	mathematical	—	range CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex ofSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv	—	CategoryTheory.Subfunctor.range_eq_ofSection'
yonedaEquiv_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.stdSimplex CategoryTheory.Subfunctor.toFunctor Set.Elem toSSet EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv CategoryTheory.CategoryStruct.comp ι	—	—

SSet.stdSimplex

Definitions

Name	Category	Theorems
asOrderHom 📖	CompOp	1 math math: SSet.horn_obj
const 📖	CompOp	3 math math: obj₀Equiv_symm_apply, const_down_toOrderHom, SSet.horn.spineId_vertex_coe
edge 📖	CompOp	2 math math: coe_edge_down_toOrderHom, SSet.horn.edge_coe
face 📖	CompOp	40 math math: SSet.horn₃₁.desc.multicofork_π_two, SSet.horn.faceSingletonComplIso_inv_ι_assoc, faceSingletonIso_zero_hom_comp_ι_eq_δ, SSet.horn₃₂.desc.multicofork_π_one, SSet.horn₂₂.sq, face_eq_ofSimplex, SSet.horn₃₁.desc.multicofork_pt, SSet.horn.faceSingletonComplIso_inv_ι, range_δ, faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, face_obj, SSet.horn₂₀.sq, mem_face_iff, faceSingletonIso_one_hom_comp_ι_eq_δ, faceSingletonComplIso_hom_ι, SSet.face_le_horn, SSet.horn.faceι_ι, SSet.horn_eq_iSup, obj₀Equiv_symm_mem_face_iff, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.horn.faceι_ι_assoc, SSet.horn.multicoequalizerDiagram, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, ofSimplex_yonedaEquiv_δ, SSet.horn₃₂.desc.multicofork_π_three, faceSingletonComplIso_hom_ι_assoc, SSet.boundary_eq_iSup, face_inter_face, SSet.horn₃₂.desc.multicofork_pt, faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, face_le_face_iff, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.horn₃₁.desc.multicofork_π_three, SSet.horn₂₁.sq, face_singleton_compl
facePairIso 📖	CompOp	—
faceRepresentableBy 📖	CompOp	—
faceSingletonComplIso 📖	CompOp	16 math math: SSet.horn₃₁.desc.multicofork_π_two, SSet.horn.faceSingletonComplIso_inv_ι_assoc, SSet.horn₃₂.desc.multicofork_π_one, SSet.horn.faceSingletonComplIso_inv_ι, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, faceSingletonComplIso_hom_ι, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three, faceSingletonComplIso_hom_ι_assoc, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.horn₃₁.desc.multicofork_π_three
faceSingletonIso 📖	CompOp	4 math math: faceSingletonIso_zero_hom_comp_ι_eq_δ, faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, faceSingletonIso_one_hom_comp_ι_eq_δ, faceSingletonIso_one_hom_comp_ι_eq_δ_assoc
finSuccAboveOrderIsoFinset 📖	CompOp	—
instDecidableEqHomObjSimplexCategoryOfOppositeOp 📖	CompOp	—
instDecidableEqObjOppositeSimplexCategory 📖	CompOp	—
instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat 📖	CompOp	17 math math: mem_nonDegenerate_iff_strictMono, SSet.prodStdSimplex.orderHomOfSimplex_coe, SSet.prodStdSimplex.objEquiv_apply_fst, ext_iff, obj₀Equiv_apply, spineId_arrow_apply_zero, SSet.prodStdSimplex.objEquiv_apply_snd, nonDegenerateEquiv_apply_apply, mem_face_iff, isoNerve_hom_app_apply, monotone_apply, objEquiv_toOrderHom_apply, objMk_apply, spineId_arrow_apply_one, objEquiv_symm_apply, SSet.horn.const_val_apply, isoNerve_inv_app_apply
isoNerve 📖	CompOp	2 math math: isoNerve_hom_app_apply, isoNerve_inv_app_apply
isoOfRepresentableBy 📖	CompOp	—
nonDegenerateEquiv 📖	CompOp	2 math math: nonDegenerateEquiv_apply_apply, nonDegenerateEquiv_symm_apply_coe
objEquiv 📖	CompOp	10 math math: face_obj, map_apply, objEquiv_symm_mem_nonDegenerate_iff_mono, objEquiv_symm_comp, yonedaEquiv_map, objEquiv_toOrderHom_apply, mem_nonDegenerate_iff_mono, objEquiv_symm_apply, nonDegenerateEquiv_symm_apply_coe, face_singleton_compl
objMk 📖	CompOp	2 math math: face_eq_ofSimplex, objMk_apply
obj₀Equiv 📖	CompOp	8 math math: SSet.ι₀_snd_assoc, obj₀Equiv_symm_apply, obj₀Equiv_apply, SSet.ι₀_snd, SSet.ι₁_snd_assoc, SSet.ι₁_snd, obj₀Equiv_symm_mem_face_iff, spineId_vertex
triangle 📖	CompOp	2 math math: coe_triangle_down_toOrderHom, SSet.horn.primitiveTriangle_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_edge_down_toOrderHom 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len Opposite.unop SimplexCategory Opposite.op PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda edge Matrix.vecCons Matrix.vecEmpty	—	—
coe_triangle_down_toOrderHom 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len Opposite.unop SimplexCategory Opposite.op PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda triangle Matrix.vecCons Matrix.vecEmpty	—	—
const_down_toOrderHom 📖	mathematical	—	SimplexCategory.Hom.toOrderHom Opposite.unop SimplexCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda const DFunLike.coe OrderHom SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.const	—	—
ext 📖	—	DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	ext
faceSingletonComplIso_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton CategoryTheory.Iso.hom faceSingletonComplIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	—
faceSingletonComplIso_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton CategoryTheory.Iso.hom faceSingletonComplIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' faceSingletonComplIso_hom_ι
faceSingletonIso_one_hom_comp_ι_eq_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	—
faceSingletonIso_one_hom_comp_ι_eq_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' faceSingletonIso_one_hom_comp_ι_eq_δ
faceSingletonIso_zero_hom_comp_ι_eq_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	—
faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' faceSingletonIso_zero_hom_comp_ι_eq_δ
face_eq_ofSimplex 📖	mathematical	—	face SSet.Subcomplex.ofSimplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex objMk Opposite.op OrderHom.comp SimplexCategory.len Opposite.unop Finset SetLike.instMembership Finset.instSetLike PartialOrder.toPreorder Fin.instPartialOrder Subtype.preorder OrderHom.Subtype.val OrderEmbedding.toOrderHom OrderIso.toOrderEmbedding	—	le_antisymm mem_face_iff OrderHom.monotone ext OrderIso.apply_symm_apply
face_inter_face 📖	mathematical	—	SSet.Subcomplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite face Finset Finset.instLattice	—	CategoryTheory.Subfunctor.ext Set.ext
face_le_face_iff 📖	mathematical	—	SSet.Subcomplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite CategoryTheory.Category.opposite face Finset Finset.partialOrder	—	obj₀Equiv_symm_mem_face_iff LE.le.trans
face_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.stdSimplex face setOf CategoryTheory.types Finset SimplexCategory.len Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Finset.image Opposite.unop DFunLike.coe OrderHom Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike objEquiv Top.top BooleanAlgebra.toTop Finset.booleanAlgebra SimplexCategory.instFintypeToTypeOrderHomFinHAddNatLenOfNat	—	—
face_singleton_compl 📖	mathematical	—	face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton SSet.Subcomplex.ofSimplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Opposite.op Opposite CategoryTheory.Category.opposite CategoryTheory.types EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv SimplexCategory.δ	—	face_eq_ofSimplex
instFiniteObjOppositeSimplexCategory 📖	mathematical	—	Finite CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex	—	Equiv.finite_iff SimplexCategory.instFiniteHom
instFiniteObjSimplexCategory 📖	mathematical	—	SSet.Finite CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex	—	SSet.finite_of_hasDimensionLT instHasDimensionLEObjSimplexCategoryMk Subtype.finite instFiniteObjOppositeSimplexCategory
instFiniteToSSetOfSimplex 📖	mathematical	—	SSet.Finite SSet.Subcomplex.toSSet SSet.Subcomplex.ofSimplex	—	Equiv.surjective SSet.Subcomplex.range_eq_ofSimplex SSet.finite_range instFiniteObjSimplexCategory
instHasDimensionLEObjSimplexCategoryMk 📖	mathematical	—	SSet.HasDimensionLE CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex	—	Set.ext mem_nonDegenerate_iff_mono SimplexCategory.len_le_of_mono
isoNerve_hom_app_apply 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory.len Opposite.unop SimplexCategory Opposite.op Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ULift.instPreorder CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex CategoryTheory.nerve CategoryTheory.Iso.hom isoNerve DFunLike.coe instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
isoNerve_inv_app_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat CategoryTheory.NatTrans.app CategoryTheory.nerve Preorder.smallCategory ULift.instPreorder PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.inv isoNerve SimplexCategory.len Opposite.unop	—	—
map_apply 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	—
map_id 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex OrderHom.id SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id
mem_face_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj face Finset Finset.instMembership DFunLike.coe instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
mem_nonDegenerate_iff_mono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate CategoryTheory.Mono Opposite.unop DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike objEquiv	—	mem_nonDegenerate_iff_strictMono SimplexCategory.mono_iff_injective StrictMono.injective Fin.strictMono_iff_lt_succ LE.le.lt_or_eq monotone_apply Fin.castSucc_le_succ
mem_nonDegenerate_iff_strictMono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate StrictMono PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	SSet.nonDegenerate_iff_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom PartialOrder.mem_nerve_nonDegenerate_iff_strictMono
monotone_apply 📖	mathematical	—	Monotone PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	OrderHom.monotone
nonDegenerateEquiv_apply_apply 📖	mathematical	—	DFunLike.coe RelEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Fin.instLinearOrder Fin.instPartialOrder RelEmbedding.instFunLike Equiv Set.Elem CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op SSet.nonDegenerate OrderEmbedding EquivLike.toFunLike Equiv.instEquivLike nonDegenerateEquiv instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat Set Set.instMembership	—	—
nonDegenerateEquiv_symm_apply_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate DFunLike.coe Equiv OrderEmbedding Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm nonDegenerateEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct objEquiv OrderEmbedding.toOrderHom PartialOrder.toPreorder Fin.instPartialOrder	—	—
objEquiv_symm_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv OrderHom SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom	—	—
objEquiv_symm_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SimplexCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
objEquiv_symm_mem_nonDegenerate_iff_mono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.Mono	—	Equiv.apply_symm_apply
objEquiv_toOrderHom_apply 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike objEquiv instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
objMk_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat objMk OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike	—	—
obj₀Equiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike obj₀Equiv instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
obj₀Equiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm obj₀Equiv const	—	—
obj₀Equiv_symm_mem_face_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet SSet.largeCategory SSet.stdSimplex Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj face DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm obj₀Equiv Finset Finset.instMembership	—	—
ofSimplex_yonedaEquiv_δ 📖	mathematical	—	SSet.Subcomplex.ofSimplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv CategoryTheory.CosimplicialObject.δ face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton	—	face_eq_ofSimplex
range_δ 📖	mathematical	—	SSet.Subcomplex.range CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton	—	SSet.Subcomplex.range_eq_ofSimplex ofSimplex_yonedaEquiv_δ
yonedaEquiv_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv CategoryTheory.Functor.map Opposite.unop Equiv.symm objEquiv	—	Equiv.injective

Simplicial

Definitions

Name	Category	Theorems
«termΔ[_]» 📖	CompOp	—

---

← Back to Index