English
Exact f g is equivalent to Exact of the restricted map range(f).subtype and g.rangeRestrict.
Русский
Точность f g эквивалентна точности ограниченного отображения range(f).subtype и g.rangeRestrict.
LaTeX
$$$$ \\operatorname{Exact}(f,g) \\iff \\operatorname{Exact}\\big( \\operatorname{range}(f).\\mathrm{subtype},\\; g_{\\mathrm{rangeRestrict}} \\big). $$$$
Lean4
/-- Two maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P` are exact if and only if the induced maps
`LinearMap.range f → N → LinearMap.range g` are exact. -/
theorem iff_linearMap_rangeRestrict : Exact f g ↔ Exact (LinearMap.range f).subtype g.rangeRestrict :=
iff_rangeFactorization (zero_mem (LinearMap.range g))