isIso_g_iff — Mathlib

English

In a balanced category, for a short exact S, the map g in the last part is an isomorphism iff X1 is zero.

Русский

В балансированной категории для кратко точной S отображение g является изоморфизмом тогда и только тогда, когда X1 равен нулю.

LaTeX

$$$IsIso(S.g) \iff IsZero(S.X_1)$$$

Lean4

theorem isIso_g_iff {S : ShortComplex C} (hS : S.ShortExact) [Balanced C] : IsIso S.g ↔ IsZero S.X₁ :=
  by
  have := hS.exact.hasZeroObject
  have := hS.mono_f
  have := hS.epi_g
  constructor
  · intro hf
    simp only [IsZero.iff_id_eq_zero, ← cancel_mono S.f, ← cancel_mono S.g, S.zero, zero_comp, assoc, comp_zero]
  · intro hX₁
    have : Mono S.g := (S.exact_iff_mono (hX₁.eq_of_src _ _)).1 hS.exact
    apply isIso_of_mono_of_epi

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