English
If φ: Δ→Δ'' factors through image φ via epi e and mono i, then the canonical image inclusion equals i: image φ ⟶ Δ''.
Русский
Если φ факторизуется через образ через epi e и моно i, то каноническое включение образа в Δ'' равно i: image φ ⟶ Δ''.
LaTeX
$$$\\text{if } e:\\Delta\\to\\mathrm{im}\\,\\phi\\text{ is epi},\\ i:\\mathrm{im}\\,\\phi\\to \\Delta''\\text{ is mono},\\ φ=e\\circ i,\\ \\text{then } \\mathrm{image.}\\,\\iota\\,\\phi = i.$$$
Lean4
theorem image_ι_eq {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ image φ} [Epi e] {i : image φ ⟶ Δ''} [Mono i]
(fac : e ≫ i = φ) : image.ι φ = i := by
haveI := strongEpi_of_epi e
rw [← image.isoStrongEpiMono_hom_comp_ι e i fac, SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom,
Category.id_comp]
