Mathlib Map

Theorems · Definition · category theory

SimplexCategory.Hom.toOrderHom

{a b : SimplexCategory} → a.Hom b → Fin (a.len + 1) →o Fin (b.len + 1)

Recover the monotone map from a morphism in the simplex category.

Defined in
Mathlib.AlgebraicTopology.SimplexCategory.Defs
Cited by
111 results in Mathlib
Foundations
Depth 26 from the axioms, rests on 225 definitions · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.stdSimplex.face · cited by 77stdSimplex.faceSimplexCategory.Hom.ext · cited by 40Hom.extSSet.prodStdSimplex.objEquiv · cited by 21prodStdSimplex.objEquivCategoryTheory.Arrow.cechNerve · cited by 18Arrow.cechNerveCategoryTheory.Limits.FormalCoproduct.cech · cited by 13FormalCoproduct.cechAlgebraicTopology.DoldKan.Isδ₀ · cited by 11DoldKan.Isδ₀SimplexCategory.len_le_of_epi · cited by 9SimplexCategory.len_le_of…SSet.horn_eq_iSup · cited by 9SSet.horn_eq_iSupCategoryTheory.Arrow.cechConerve · cited by 9Arrow.cechConerveSimplexCategory.len_le_of_mono · cited by 8SimplexCategory.len_le_of…SimplexCategory.δ_comp_σ_self · cited by 8SimplexCategory.δ_comp_σ_…SimplexCategory.const_comp · cited by 7SimplexCategory.const_compSimplexCategory.skeletalFunctor · cited by 7SimplexCategory.skeletalF…SSet.stdSimplex.asOrderHom · cited by 7stdSimplex.asOrderHomSimplexCategory.const_eq_id · cited by 6SimplexCategory.const_eq_…SimplexCategory · cited by 2204SimplexCategoryOrderHom · cited by 934OrderHomSimplexCategory.len · cited by 542SimplexCategory.lenSimplexCategory.Hom · cited by 5SimplexCategory.HomHom.toOrderHomCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by131

Results whose statement or proof uses this declaration.