quasiIsoAt_map_iff_of_preservesHomology

English

If F reflects isomorphisms, then QuasiIsoAt φ i is equivalent to QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i.

Русский

Если F отражает изоморфизмы, то QuasiIsoAt φ i эквивалентно QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i.

LaTeX

$$$[F.ReflectsIsomorphisms] \Rightarrow QI_i(\varphi) \iff QI_i((F.mapHomologicalComplex c).map \varphi).$$$

Lean4

theorem quasiIsoAt_map_iff_of_preservesHomology [F.ReflectsIsomorphisms] :
    QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i :=
  by
  simp only [quasiIsoAt_iff]
  exact ShortComplex.quasiIso_map_iff_of_preservesLeftHomology F ((shortComplexFunctor C₁ c i).map φ)

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