image_eq — Mathlib

English

If φ: Δ→Δ'' factors as φ = e ≫ i with e epi and i mono, then the image of φ is Δ'.

Русский

Если φ: Δ→Δ'' факторизуется как φ = e ∘ i с e эпиморфизмом и i моно, то образ φ равен Δ'.

LaTeX

$$$\\forall \\Delta,\\Delta' ,\\Delta'' ,\\phi:\\Delta\\to\\Delta'',\\ (\\exists e:\\Delta\\to\\Delta',\\text{ epi},\\exists i:\\Delta'\\to\\Delta'',\\text{ mono})\\text{ with } \\phi=e\\circ i \\Rightarrow \\mathrm{image}\\,\\phi=\\Delta'.$$$

Lean4

theorem image_eq {Δ Δ' Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ Δ'} [Epi e] {i : Δ' ⟶ Δ''} [Mono i]
    (fac : e ≫ i = φ) : image φ = Δ' := by
  haveI := strongEpi_of_epi e
  let e := image.isoStrongEpiMono e i fac
  ext
  exact le_antisymm (len_le_of_epi e.hom) (len_le_of_mono e.hom)

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