moduleCat_exact_iff_ker_sub_range

English

Exactness is equivalent to the inclusion ker g ⊆ range f when viewed through the left homology data.

Русский

Точность эквивалентна включению ker g в образ f в рамках левых данных гомологии.

LaTeX

$$$S.Exact \\iff \\mathrm{ker} S.g.hom \\leq \\mathrm{range} S.f.hom$$$

Lean4

theorem moduleCat_exact_iff_ker_sub_range : S.Exact ↔ LinearMap.ker S.g.hom ≤ LinearMap.range S.f.hom :=
  by
  rw [moduleCat_exact_iff]
  aesop

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