English
If there exist linear equivalences forming a ladder connecting two pairs of maps with compatibilities, then exactness is preserved along the ladder: Exact(g12,g23) iff Exact(f12,f23).
Русский
Если существуют линейные эквиваленты, образующие «лестницу», связывающую две пары отображений с совместимостью, то точность сохраняется вдоль лестницы: Exact(g12,g23) ⇔ Exact(f12,f23).
LaTeX
$$$$ \\text{If } g_{12},g_{23} \\text{ and } f_{12},f_{23} \\text{ are connected by linear equivalences as in a ladder, then } \\operatorname{Exact}(g_{12},g_{23}) \\iff \\operatorname{Exact}(f_{12},f_{23}). $$$$
Lean4
theorem comp_exact_iff_exact {p : M' →ₗ[R] M} (h : Surjective p) : Exact (f ∘ₗ p) g ↔ Exact f g :=
iff_of_eq <| forall_congr fun x => congrArg (g x = 0 ↔ x ∈ ·) (h.range_comp f)
