quasiIsoAt_iff_exactAt — Mathlib

English

For a map f between complexes, QuasiIsoAt f i is equivalent to L.ExactAt i provided K has homology at i.

Русский

Для отображения f между комплексами QuasiIsoAt f i эквивалентно L.ExactAt i при условии существования K.Homology i.

LaTeX

$$QuasiIsoAt f i \iff L.ExactAt i$$

Lean4

theorem quasiIsoAt_iff_exactAt (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hK : K.ExactAt i) :
    QuasiIsoAt f i ↔ L.ExactAt i :=
  by
  simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff, ShortComplex.exact_iff_isZero_homology] at hK ⊢
  constructor
  · intro h
    exact IsZero.of_iso hK (@asIso _ _ _ _ _ h).symm
  · intro hL
    exact ⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩

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