English
Under the same hypothesis as above, and with a certain Subtype equality, exactness is equivalent to a restricted version.
Русский
При тех же предположениях точность эквивалентна ограниченной версии.
LaTeX
$$$\\text{Exact}(f,g) \\iff \\text{Exact}(f.range.subtype, g.rangeRestrict)$$$
Lean4
/-- Two maps `f : M → N` and `g : N → P` are exact if and only if 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 iff_rangeFactorization [Zero P] (hg : 0 ∈ Set.range g) :
letI : Zero (Set.range g) := ⟨⟨0, hg⟩⟩
Exact f g ↔ Exact ((↑) : Set.range f → N) (Set.rangeFactorization g) :=
by
letI : Zero (Set.range g) := ⟨⟨0, hg⟩⟩
have : ((0 : Set.range g) : P) = 0 := rfl
simp [Exact, Set.rangeFactorization, Subtype.ext_iff, this]
