English
A morphism f in SimplexCategory is mono if and only if its underlying order-preserving map f.toOrderHom is injective.
Русский
Морфизм f в SimplexCategory моно тогда и только тогда, когда соответствующая отображение порядка f.toOrderHom инъективно.
LaTeX
$$$\\mathrm{Mono}(f) \\iff \\operatorname{Injective}(f^{\\mathrm{toOrderHom}})$$$
Lean4
/-- A morphism in `SimplexCategory` is a monomorphism precisely when it is an injective function
-/
theorem mono_iff_injective {n m : SimplexCategory} {f : n ⟶ m} : Mono f ↔ Function.Injective f.toOrderHom :=
by
rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor]
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
simp only [skeletalFunctor_obj, skeletalFunctor_map, NonemptyFinLinOrd.mono_iff_injective, NonemptyFinLinOrd.coe_of,
ConcreteCategory.hom_ofHom]
