English
A natural transformation identity holds for the homomorphisms involved in mapping through UpToQuasiIso; in particular, a specific equality of certain composed morphisms is maintained after localization.
Русский
Для гомоморфизмов в отображении через UpToQuasiIso сохраняется соответствующее тождество сложения гомоморфизмов; сохранена порядок композиции после локализации.
LaTeX
$$$ (F.mapHomologicalComplexUpToQuasiIsoFactorsh\ c).hom.app\bigl( (\mathrm{HomotopyCategory.quotient}\ C\ c).\mathrm{obj}\ K \bigr) = \cdots $$$
Lean4
@[reassoc]
theorem mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app (K : HomologicalComplex C c) :
(F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient _ _).obj K) =
(F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
(F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
(HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app _ ≫
HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K) :=
by
dsimp [mapHomologicalComplexUpToQuasiIsoFactorsh]
rw [Localization.liftNatTrans_app]
dsimp
simp only [Category.comp_id, Category.id_comp]
change _ = (F.mapHomologicalComplexUpToQuasiIso c).map (𝟙 _) ≫ _ ≫ 𝟙 _ ≫ HomologicalComplexUpToQuasiIso.Qh.map (𝟙 _)
simp only [map_id, Category.comp_id, Category.id_comp]
