English
If f,g are exact and 0 ∈ range(g), then the induced map on ranges via factorization is exact.
Русский
Если f и g точны и 0 лежит в образе g, то индуцированная карта через факторизацию образа g точна.
LaTeX
$$$\\text{Exact}(f,g) \\land (0 \\in \\mathrm{range}(g)) \\Rightarrow \\text{Exact}((\\uparrow): \\mathrm{range}(f) \\to N)(\\mathrm{rangeFactorization}(g))$$$
Lean4
/-- If two maps `f : M → N` and `g : N → P` are exact, then the induced maps
`Set.range f → N → Set.range g` are exact.
Note that if you already have an instance `[Zero (Set.range g)]` (which is unlikely) this lemma
may not apply if the zero of `Set.range g` is not definitionally equal to `⟨0, hg⟩`. -/
theorem rangeFactorization [Zero P] (h : Exact f g) (hg : 0 ∈ Set.range g) :
letI : Zero (Set.range g) := ⟨⟨0, hg⟩⟩
Exact ((↑) : Set.range f → N) (Set.rangeFactorization g) :=
(iff_rangeFactorization hg).1 h
