quasiIso_of_retractArrow — Mathlib

English

If f is a retract of f′, and all i-th homologies exist, and f′ is a quasi-isomorphism, then f is a quasi-isomorphism.

Русский

Если f является retract-изоморфизмом f′, и существуют все i-й гомологии, и f′ — квазиизоморфизм, тогда f — квазиизоморфизм.

LaTeX

$$$\text{RetractArrow}(f,f') \Rightarrow QI(f)\text{ if } QI(f').$$$

Lean4

theorem quasiIso_of_retractArrow {f : K ⟶ L} {f' : K' ⟶ L'} (h : RetractArrow f f') [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] [∀ i, K'.HasHomology i] [∀ i, L'.HasHomology i] [QuasiIso f'] : QuasiIso f where
  quasiIsoAt i := quasiIsoAt_of_retract h i

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