of_ladder_addEquiv_of_exact — Mathlib

English

If the bottom row is exact and the ladders commute, then the top row is exact.

Русский

Если нижняя строка точна и лестницы коммутируют, то верхняя строка точна.

LaTeX

$$$\\text{Exact}(f_{12},f_{23}) \\Rightarrow \\text{Exact}(g_{12},g_{23})$ given commutativity data$$

Lean4

theorem of_ladder_addEquiv_of_exact (comm₁₂ : g₁₂.comp e₁ = AddMonoidHom.comp e₂ f₁₂)
    (comm₂₃ : g₂₃.comp e₂ = AddMonoidHom.comp e₃ f₂₃) (H : Exact f₁₂ f₂₃) : Exact g₁₂ g₂₃ :=
  (iff_of_ladder_addEquiv _ _ _ comm₁₂ comm₂₃).2 H

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