exact_iff_of_hasForget — Mathlib

English

If S is a Short Exact in C, then the induced map on the forgetful image to Ab, namely (forget₂ C Ab).map S.g, is surjective.

Русский

Если S является кратким точным в C, то образующее отображение на забывающую абелеву группу, соответствующее S.g, сюръективно.

LaTeX

$$$\\operatorname{Surjective}(((\\forget_2\\ C\\ Ab).map S.g))$$$

Lean4

theorem exact_iff_of_hasForget [S.HasHomology] :
    S.Exact ↔
      ∀ (x₂ : (forget₂ C Ab).obj S.X₂) (_ : ((forget₂ C Ab).map S.g) x₂ = 0),
        ∃ (x₁ : (forget₂ C Ab).obj S.X₁), ((forget₂ C Ab).map S.f) x₁ = x₂ :=
  by
  rw [S.exact_iff_exact_map_forget₂, ab_exact_iff]
  rfl

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