Theorems · Definition · category theory

SemiSimplexCategory.homOfMono

{n m : SemiSimplexCategory} →
  (f : SemiSimplexCategory.toSimplexCategory.obj n ⟶ SemiSimplexCategory.toSimplexCategory.obj m) →
    [CategoryTheory.Mono f] → n ⟶ m

Constructor for morphisms in SemiSimplexCategory which takes as an input a monomorphism in SimplexCategory.

Defined in: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
Cited by: 3 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Mono

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

DFunLike.coeproof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
Equiv.symmproof · cited by 3,681
SimplexCategorystatement · cited by 2,204
CategoryTheory.Monostatement and proof · cited by 893
SimplexCategory.Hom.toOrderHomproof · cited by 111
SemiSimplexCategorystatement and proof · cited by 15
OrderEmbedding.ofStrictMonoproof · cited by 15
SemiSimplexCategory.homEquivproof · cited by 4
SemiSimplexCategory.toSimplexCategorystatement and proof · cited by 4

Cited by4

Results whose statement or proof uses this declaration.

SSet.N.toSemiSimplexCategoryproof · cited by 3
SSet.N.toSemiSimplexCategory_mapstatement · cited by 0
SemiSimplexCategory.homOfMono.congr_simpstatement and proof · cited by 0
SemiSimplexCategory.toSimplexCategory_map_homOfMonostatement and proof · cited by 0