eq_liftCycles_homologyπ_up_to_refinements

English

The inversion of a quasi-isomorphism in the homological category remains a quasi-isomorphism.

Русский

Обратное к квазиизоморфизму сохраняется в гомологической категории.

LaTeX

$$$QI(e^{-1})$$$

Lean4

theorem eq_liftCycles_homologyπ_up_to_refinements {A : C} {i : ι} (γ : A ⟶ K.homology i) (j : ι) (hj : c.next i = j) :
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : z ≫ K.d i j = 0),
      π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i :=
  by
  subst hj
  exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ

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