iff_of_ladder_addEquiv — Mathlib

English

If there are additive equivalences e1,e2,e3 making the ladders commute, then exactness of the top row is equivalent to that of the bottom row.

Русский

Если существуют аддитивные эквиваленты, делающие лестницы коммутативными, то точность верхней строки эквивалентна точности нижней.

LaTeX

$$$\\text{Exact}(g_{12},g_{23}) \\iff \\text{Exact}(f_{12},f_{23})$ under commutativity conditions via AddEquiv$$

Lean4

theorem iff_of_ladder_addEquiv (comm₁₂ : g₁₂.comp e₁ = AddMonoidHom.comp e₂ f₁₂)
    (comm₂₃ : g₂₃.comp e₂ = AddMonoidHom.comp e₃ f₂₃) : Exact g₁₂ g₂₃ ↔ Exact f₁₂ f₂₃ :=
  (exact_iff_of_surjective_of_bijective_of_injective _ _ _ _ e₁ e₂ e₃ comm₁₂ comm₂₃ e₁.surjective e₂.bijective
      e₃.injective).symm

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