quasiIso_iff_isIso_liftCycles — Mathlib

English

If there is an isomorphism between Arrow.mk φ and Arrow.mk φ′, then φ is quasi-iso iff φ′ is quasi-iso.

Русский

Если существует изоморфизм между Arrow.mk φ и Arrow.mk φ′, то φ квазиизоморфизм тогда и только тогда, когда φ′ квазиизоморфизм.

LaTeX

$$$Arrow.mk φ \cong Arrow.mk φ' \Rightarrow (\operatorname{QuasiIso}(φ) \iff \operatorname{QuasiIso}(φ'))$$$

Lean4

theorem quasiIso_iff_isIso_liftCycles (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :
    QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp])) :=
  by
  let H :
    LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
      (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ _ S₂.cyclesIsKernel) :=
    { φK := S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp])
      φH := S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp]) }
  exact H.quasiIso_iff

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