ι_descQ_eq_zero_of_boundary — Mathlib

English

Under suitable zero conditions on f and g, φ is quasi-iso iff the opDescCycles map is an iso.

Русский

При подходящих условиях нулевого поведения функций f и g, φ — квазиизоморфизм тогда и только тогда, когда соответствующая карта opDescCycles является изоморфизмом.

LaTeX

$$$\operatorname{QuasiIso}(φ) \iff \operatorname{IsIso}(S_1.descOpcycles φ.τ_2 (\dots))$$$

Lean4

@[reassoc]
theorem ι_descQ_eq_zero_of_boundary (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = S.g ≫ x) :
    h.ι ≫ h.descQ k (by rw [hx, S.zero_assoc, zero_comp]) = 0 :=
  by
  rw [show 0 = h.ι ≫ h.g' ≫ x by simp]
  congr 1
  simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]

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