English
If f1₂ ↔ g1₂ and f2₃ ↔ g2₃ are connected by a ladder of linear equivalences, then Exact(f1₂,f2₃) ⇔ Exact(g1₂,g2₃).
Русский
Если отображения, образующие пару последовательностей, связаны линейными эквивалентами по «лестнице», то точность сохраняется.
LaTeX
$$$$ \\text{If } g_{12}, g_{23}, f_{12}, f_{23} \\text{ are linked by linear equivalences as in a ladder, then } \\operatorname{Exact}(f_{12},f_{23}) \\iff \\operatorname{Exact}(g_{12},g_{23}). $$$$
Lean4
theorem iff_of_ladder_linearEquiv (h₁₂ : g₁₂ ∘ₗ e₁ = e₂ ∘ₗ f₁₂) (h₂₃ : g₂₃ ∘ₗ e₂ = e₃ ∘ₗ f₂₃) :
Exact g₁₂ g₂₃ ↔ Exact f₁₂ f₂₃ :=
iff_of_ladder_addEquiv e₁.toAddEquiv e₂.toAddEquiv e₃.toAddEquiv (f₁₂ := f₁₂) (f₂₃ := f₂₃) (g₁₂ := g₁₂) (g₂₃ := g₂₃)
(congr_arg LinearMap.toAddMonoidHom h₁₂) (congr_arg LinearMap.toAddMonoidHom h₂₃)
