ab_exact_iff_range_eq_ker — Mathlib

English

Let S be a ShortComplex in Ab. S.Exact is equivalent to the image of f equaling the kernel of g; i.e., im(f) = ker(g).

Русский

Пусть S — краткая точная последовательность в абелевых группах. Tогда S.Exact эквивалентно тому, что образ f совпадает с ядром g; то есть im(f) = ker(g).

LaTeX

$$$$ S.Exact \\iff \\mathrm{im}(f) = \\ker(g). $$$$

Lean4

theorem ab_exact_iff_range_eq_ker : S.Exact ↔ S.f.hom.range = S.g.hom.ker :=
  by
  rw [ab_exact_iff_ker_le_range]
  constructor
  · intro h
    refine le_antisymm ?_ h
    rintro _ ⟨x₁, rfl⟩
    rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]
    rfl
  · intro h
    rw [h]

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