quotient_map_mem_quasiIso_iff — Mathlib

English

For K,L objects and f: K → L, the morphism becomes a quasi-isomorphism after quotient if and only if f is a quasi-isomorphism.

Русский

Для K, L и f: K → L выполнение квантизации через quotient сохраняет квазиизоморфизм тогда и только тогда, когда само отображение f является квазиизоморфизмом.

LaTeX

$$$ \operatorname{quasiIso}(C,c,((quotient\ C\ c).map\ f)) \iff \operatorname{quasiIso}(C,c,f). $$$

Lean4

theorem quotient_map_mem_quasiIso_iff {K L : HomologicalComplex C c} (f : K ⟶ L) :
    quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f :=
  by
  have eq := fun (i : ι) => NatIso.isIso_map_iff (homologyFunctorFactors C c i) f
  dsimp at eq
  simp only [HomologicalComplex.mem_quasiIso_iff, mem_quasiIso_iff, quasiIso_iff, quasiIsoAt_iff_isIso_homologyMap, eq]

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