isIso_f_iff — Mathlib

English

In a balanced category, for a short exact S, the map f in the first part is an isomorphism iff the third object X3 is zero.

Русский

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

LaTeX

$$$IsIso(S.f) \iff IsZero(S.X_3)$$$

Lean4

theorem isIso_f_iff {S : ShortComplex C} (hS : S.ShortExact) [Balanced C] : IsIso S.f ↔ 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_epi S.g, ← cancel_epi S.f, S.zero_assoc, zero_comp]
  · intro hX₃
    have : Epi S.f := (S.exact_iff_epi (hX₃.eq_of_tgt _ _)).1 hS.exact
    apply isIso_of_mono_of_epi

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