exact_of_iso — Mathlib

English

If S1 ≅ S2 and S1 is Exact, then S2 is Exact.

Русский

Если S1 ≅ S2 и S1 является точным (Exact), то S2 тоже точен.

LaTeX

$$$\text{If } e: S_1 \cong S_2 \text{ and } S_1\text{ is exact, then } S_2\text{ is exact.}$$$

Lean4

theorem exact_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.Exact) : S₂.Exact
    where
  toIsComplex := isComplex_of_iso e h₁.toIsComplex
  exact i
    hi := ShortComplex.exact_of_iso (scMapIso e h₁.toIsComplex (isComplex_of_iso e h₁.toIsComplex) i) (h₁.exact i hi)

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