quasiIsoAt_iff — Mathlib

English

If f is a quasi-isomorphism at i, then it yields a quasi-isomorphism between the corresponding short complexes at i.

Русский

Если отображение f является квазиизоморфизмом на позиции i, то оно индуцирует квазиизоморфизм между соответствующими краткими комплексами на i.

LaTeX

$$QuasiIsoAt f i$$

Lean4

theorem quasiIsoAt_iff (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
    QuasiIsoAt f i ↔ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) :=
  by
  constructor
  · intro h
    exact h.quasiIso
  · intro h
    exact ⟨h⟩

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