moduleCat_exact_iff — Mathlib

English

Exactness of a short complex in the module category is equivalent to the usual exactness condition of the pair (f,g).

Русский

Точность (ровность) в коротком комплексе в категории модулей эквивалентна обычному условию точности пары отображений (f,g).

LaTeX

$$$S\\text{.Exact}$ iff $\\text{Exact}(f,g)$$$

Lean4

theorem moduleCat_exact_iff : S.Exact ↔ ∀ (x₂ : S.X₂) (_ : S.g x₂ = 0), ∃ (x₁ : S.X₁), S.f x₁ = x₂ :=
  S.exact_iff_of_hasForget

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