Mathlib Map

Theorems · Definition · category theory

SimplexCategory.Hom.mk

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

Make a morphism in SimplexCategory from a monotone map of Fin's.

Defined in
Mathlib.AlgebraicTopology.SimplexCategory.Defs
Cited by
15 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimplexCategory.const · cited by 47SimplexCategory.constSimplexCategory.σ₀Iter · cited by 29SimplexCategory.σ₀IterSimplexCategory.δ₀Iter · cited by 25SimplexCategory.δ₀IterSSet.prodStdSimplex.objEquiv · cited by 21prodStdSimplex.objEquivSimplexCategory.rev · cited by 18SimplexCategory.revSimplexCategory.toMk₁ · cited by 13SimplexCategory.toMk₁SSet.stdSimplex.objMk · cited by 5stdSimplex.objMkSimplexCategory.σ₀Iter_zero · cited by 5SimplexCategory.σ₀Iter_ze…SemiSimplexCategory.toSimplexCategory · cited by 4SemiSimplexCategory.toSim…AugmentedSimplexCategory.inl'_eval · cited by 3AugmentedSimplexCategory.…AugmentedSimplexCategory.inr'_eval · cited by 3AugmentedSimplexCategory.…SimplexCategory.II · cited by 3SimplexCategory.IISSet.unique_nonDegenerate_map · cited by 3SSet.unique_nonDegenerate…SSet.stdSimplex.face_eq_ofSimplex · cited by 3stdSimplex.face_eq_ofSimp…SSet.stdSimplex.isoNerve · cited by 3stdSimplex.isoNerveSimplexCategory · cited by 2204SimplexCategoryOrderHom · cited by 934OrderHomSimplexCategory.len · cited by 542SimplexCategory.lenSimplexCategory.Hom · cited by 5SimplexCategory.HomHom.mkCITED BYCITES

Cites4

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

Cited by32

Results whose statement or proof uses this declaration.