moduleCat_of_range_eq_ker — Mathlib

English

If the range of f equals the kernel of g, then the constructed short complex in ModuleCat is exact.

Русский

Если образ f равен ядру g, то сконструированный короткий комплекс в ModuleCat точен.

LaTeX

$$$\\text{moduleCatMkOfKerLERange}(f,g,\\text{hfg}).Exact$ when $\\mathrm{range}(f)=\\ker(\\!g)$$$

Lean4

theorem moduleCat_of_range_eq_ker {X₁ X₂ X₃ : ModuleCat.{v} R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
    (hfg : LinearMap.range f.hom = LinearMap.ker g.hom) : (moduleCatMkOfKerLERange f g (by rw [hfg])).Exact := by
  simpa only [moduleCat_exact_iff_range_eq_ker] using hfg

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