instQuasiIsoShortComplexTruncLEX₃ToTruncGE

English

The morphism K.shortComplexTruncLEX₃ToTruncGE ac is a quasi-isomorphism in the ambient Abelian category, i.e., it induces isomorphisms on homology.

Русский

Морфизм K.shortComplexTruncLEX₃ToTruncGE ac является квазиизоморфизмом в абелевой категории, то есть индуцирует изоморфизмы на гомологии.

LaTeX

$$$\\text{QuasiIso}\\big( K.shortComplexTruncLEX₃ToTruncGE\\, ac\\big)$$$

Lean4

instance : QuasiIso (K.shortComplexTruncLEX₃ToTruncGE ac) where
  quasiIsoAt
    i := by
    obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i
    · have h₁ := ((ac.isSupportedOutside₁_iff (K.truncGE e₂)).2 inferInstance).exactAt i₁
      have h₂ := (K.shortComplexTruncLE_X₃_isSupportedOutside e₁).exactAt i₁
      simpa only [quasiIsoAt_iff_exactAt _ _ h₂] using h₁
    · have := quasiIsoAt_shortComplexTruncLE_g K e₁ (e₂.f i₂) (fun _ => ac.disjoint _ _)
      rw [← quasiIsoAt_iff_comp_left (K.shortComplexTruncLE e₁).g (K.shortComplexTruncLEX₃ToTruncGE ac),
        g_shortComplexTruncLEX₃ToTruncGE]
      dsimp
      infer_instance

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