epi_iff_surjective — Mathlib

English

A morphism f in SimplexCategory is epi if and only if its underlying order-preserving map f.toOrderHom is surjective.

Русский

Эпиморфизм в SimplexCategory эквивалентен сюръективному отображению порядка f.toOrderHom.

LaTeX

$$$\\mathrm{Epi}(f) \\iff \\text{Surjective}(f^{\\mathrm{toOrderHom}})$$$

Lean4

/-- A morphism in `SimplexCategory` is an epimorphism if and only if it is a surjective function
-/
theorem epi_iff_surjective {n m : SimplexCategory} {f : n ⟶ m} : Epi f ↔ Function.Surjective f.toOrderHom :=
  by
  rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor]
  dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
  simp only [skeletalFunctor_obj, skeletalFunctor_map, NonemptyFinLinOrd.epi_iff_surjective, NonemptyFinLinOrd.coe_of,
    ConcreteCategory.hom_ofHom]

Похожие утверждения