factorThruImage_eq — Mathlib

English

If φ has image via e and i with φ = e ≫ i, then the canonical factorThroughImage φ equals e.

Русский

Если φ имеет образ через e и i с φ = e ∘ i, то каноническое factorThroughImage φ равно e.

LaTeX

$$$\\phi=e\\circ i\\ \&\\ i\\text{ mono},\\ e\\text{ epi} \\Rightarrow \\mathrm{factorThruImage}\\,\\phi = e.$$$

Lean4

theorem factorThruImage_eq {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ image φ} [Epi e] {i : image φ ⟶ Δ''}
    [Mono i] (fac : e ≫ i = φ) : factorThruImage φ = e := by rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]

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