quasiIso — Mathlib

English

If F reflects isomorphisms, then QuasiIso φ maps to QuasiIso φ under F.mapHomologicalComplex.

Русский

Если F отражает изоморфизмы, тогда QuasiIso φ переходит в QuasiIso φ под F.mapHomologicalComplex.

LaTeX

$$$F.ReflectsIsomorphisms \Rightarrow QI((F.mapHomologicalComplex c).map \varphi) \Leftrightarrow QI(\varphi).$$$

Lean4

/-- The morphism property on `HomologicalComplex C c` given by quasi-isomorphisms. -/
def quasiIso [CategoryWithHomology C] : MorphismProperty (HomologicalComplex C c) := fun _ _ f => QuasiIso f

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