of_comp_eq_zero_of_ker_in_range — Mathlib

English

If 0 is in the range of g, then exactness of f and g is equivalent to exactness of the restricted induced map from range f to N after factoring through the range of g.

Русский

Если 0 лежит в образе g, то точность пары (f,g) эквивалентна точности композиции после факторизации через образ g.

LaTeX

$$$\\text{Exact}(f,g) \\iff \\text{Exact}( (\\uparrow):\\mathrm{range}(f) \\to N,\\; \\mathrm{rangeFactorization}(g) )$$$

Lean4

theorem of_comp_eq_zero_of_ker_in_range [Zero P] (hc : g.comp f = 0) (hr : ∀ y, g y = 0 → y ∈ Set.range f) :
    Exact f g := fun y ↦ ⟨hr y, fun ⟨x, hx⟩ ↦ hx ▸ congrFun hc x⟩

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