The category of homological complexes up to quasi-isomorphisms

Given a category C with homology and any complex shape c, we define the category HomologicalComplexUpToQuasiIso C c which is the localized category of HomologicalComplex C c with respect to quasi-isomorphisms. When C is abelian, this will be the derived category of C in the particular case of the complex shape ComplexShape.up ℤ.

Under suitable assumptions on c (e.g. chain complexes, or cochain complexes indexed by ℤ), we shall show that HomologicalComplexUpToQuasiIso C c is also the localized category of HomotopyCategory C c with respect to the class of quasi-isomorphisms.

@[reducible, inline]

abbrev HomologicalComplexUpToQuasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] : Type (max (max u_1 u_2) u_3)

The category of homological complexes up to quasi-isomorphisms.

Equations

• HomologicalComplexUpToQuasiIso C c = (HomologicalComplex.quasiIso C c).Localization'

@[reducible, inline]

abbrev HomologicalComplexUpToQuasiIso.Q {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] : CategoryTheory.Functor (HomologicalComplex C c) (HomologicalComplexUpToQuasiIso C c)

The localization functor HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c.

Equations

• HomologicalComplexUpToQuasiIso.Q = (HomologicalComplex.quasiIso C c).Q'

theorem HomologicalComplex.homologyFunctor_inverts_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (i : ι) : (HomologicalComplex.quasiIso C c).IsInvertedBy (HomologicalComplex.homologyFunctor C c i)

noncomputable def HomologicalComplexUpToQuasiIso.homologyFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] (i : ι) : CategoryTheory.Functor (HomologicalComplexUpToQuasiIso C c) C

The homology functor HomologicalComplexUpToQuasiIso C c ⥤ C for each i : ι.

Equations

• HomologicalComplexUpToQuasiIso.homologyFunctor C c i = CategoryTheory.Localization.lift (HomologicalComplex.homologyFunctor C c i) ⋯ HomologicalComplexUpToQuasiIso.Q

noncomputable def HomologicalComplexUpToQuasiIso.homologyFunctorFactors (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] (i : ι) : HomologicalComplexUpToQuasiIso.Q.comp (HomologicalComplexUpToQuasiIso.homologyFunctor C c i) ≅ HomologicalComplex.homologyFunctor C c i

The homology functor on HomologicalComplexUpToQuasiIso C c is induced by the homology functor on HomologicalComplex C c.

Equations

• HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i = CategoryTheory.Localization.fac (HomologicalComplex.homologyFunctor C c i) ⋯ HomologicalComplexUpToQuasiIso.Q

theorem HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K ⟶ L) : CategoryTheory.IsIso (HomologicalComplexUpToQuasiIso.Q.map f) ↔ HomologicalComplex.quasiIso C c f

theorem HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Q

def HomotopyCategory.quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : CategoryTheory.MorphismProperty (HomotopyCategory C c)

The class of quasi-isomorphisms in the homotopy category.

Equations

• HomotopyCategory.quasiIso C c f = ∀ (i : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c i).map f)

theorem HomotopyCategory.mem_quasiIso_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : HomotopyCategory C c} {Y : HomotopyCategory C c} (f : X ⟶ Y) : HomotopyCategory.quasiIso C c f ↔ ∀ (n : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c n).map f)

theorem HomotopyCategory.quotient_map_mem_quasiIso_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K ⟶ L) : HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

instance HomotopyCategory.respectsIso_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : (HomotopyCategory.quasiIso C c).RespectsIso

Equations

• ⋯ = ⋯

theorem HomotopyCategory.homologyFunctor_inverts_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (i : ι) : (HomotopyCategory.quasiIso C c).IsInvertedBy (HomotopyCategory.homologyFunctor C c i)

theorem HomotopyCategory.quasiIso_eq_quasiIso_map_quotient (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : HomotopyCategory.quasiIso C c = (HomologicalComplex.quasiIso C c).map (HomotopyCategory.quotient C c)

class ComplexShape.QFactorsThroughHomotopy {ι : Type u_3} (c : ComplexShape ι) (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : Prop

The condition on a complex shape c saying that homotopic maps become equal in the localized category with respect to quasi-isomorphisms.

• areEqualizedByLocalization : ∀ {K L : HomologicalComplex C c} {f g : K ⟶ L}, Homotopy f g → CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

theorem ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization {ι : Type u_3} {c : ComplexShape ι} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [self : c.QFactorsThroughHomotopy C] {K : HomologicalComplex C c} {L : HomologicalComplex C c} {f : K ⟶ L} {g : K ⟶ L} (h : Homotopy f g) : CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

theorem HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] {K : HomologicalComplex C c} {L : HomologicalComplex C c} {f : K ⟶ L} {g : K ⟶ L} (h : Homotopy f g) : HomologicalComplexUpToQuasiIso.Q.map f = HomologicalComplexUpToQuasiIso.Q.map g

def HomologicalComplexUpToQuasiIso.Qh {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] : CategoryTheory.Functor (HomotopyCategory C c) (HomologicalComplexUpToQuasiIso C c)

The functor HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c from the homotopy category to the localized category with respect to quasi-isomorphisms.

Equations

• HomologicalComplexUpToQuasiIso.Qh = CategoryTheory.Quotient.lift (homotopic C c) HomologicalComplexUpToQuasiIso.Q ⋯

def HomologicalComplexUpToQuasiIso.quotientCompQhIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] : (HomotopyCategory.quotient C c).comp HomologicalComplexUpToQuasiIso.Qh ≅ HomologicalComplexUpToQuasiIso.Q

The canonical isomorphism HomotopyCategory.quotient C c ⋙ Qh ≅ Q.

Equations

• HomologicalComplexUpToQuasiIso.quotientCompQhIso C c = CategoryTheory.Quotient.lift.isLift (homotopic C c) HomologicalComplexUpToQuasiIso.Q ⋯

theorem HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] : (HomotopyCategory.quasiIso C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Qh

instance HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] : ((HomotopyCategory.quotient C c).comp HomologicalComplexUpToQuasiIso.Qh).IsLocalization (HomologicalComplex.quasiIso C c)

Equations

• ⋯ = ⋯

noncomputable def HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] (i : ι) : HomologicalComplexUpToQuasiIso.Qh.comp (HomologicalComplexUpToQuasiIso.homologyFunctor C c i) ≅ HomotopyCategory.homologyFunctor C c i

The homology functor on HomologicalComplexUpToQuasiIso C c is induced by the homology functor on HomotopyCategory C c.

Equations

• One or more equations did not get rendered due to their size.

instance HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] : HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.quasiIso C c)

The category HomologicalComplexUpToQuasiIso C c which was defined as a localization of HomologicalComplex C c with respect to quasi-isomorphisms also identify to a localization of the homotopy category with respect ot quasi-isomorphisms.

Equations

• ⋯ = ⋯

def ComplexShape.strictUniversalPropertyFixedTargetQuotient {ι : Type u_1} (c : ComplexShape ι) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (C : Type u_2) [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) E

The homotopy category satisfies the universal property of the localized category with respect to homotopy equivalences.

Equations

• One or more equations did not get rendered due to their size.

theorem ComplexShape.quotient_isLocalization {ι : Type u_1} (c : ComplexShape ι) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)

theorem ComplexShape.QFactorsThroughHomotopy_of_exists_prev {ι : Type u_1} (c : ComplexShape ι) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] : c.QFactorsThroughHomotopy C

instance instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} [CategoryTheory.Preadditive C] [AddRightCancelSemigroup ι] [One ι] [CategoryTheory.Limits.HasBinaryBiproducts C] : (HomotopyCategory.quotient C (ComplexShape.down ι)).IsLocalization (HomologicalComplex.homotopyEquivalences C (ComplexShape.down ι))

Equations

• ⋯ = ⋯

instance instQFactorsThroughHomotopyDown (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} [CategoryTheory.Preadditive C] [AddRightCancelSemigroup ι] [One ι] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] : (ComplexShape.down ι).QFactorsThroughHomotopy C

Equations

• ⋯ = ⋯

instance instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).IsLocalization (HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ))

Equations

• ⋯ = ⋯

instance instQFactorsThroughHomotopyIntUp (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] : (ComplexShape.up ℤ).QFactorsThroughHomotopy C

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [F.Additive] [F.PreservesHomology] : (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).functor = F.mapHomologicalComplex c

def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [F.Additive] [F.PreservesHomology] : CategoryTheory.LocalizerMorphism (HomologicalComplex.quasiIso C c) (HomologicalComplex.quasiIso D c)

The localizer morphism which expresses that F.mapHomologicalComplex c preserves quasi-isomorphisms.

Equations

• F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c = { functor := F.mapHomologicalComplex c, map := ⋯ }

theorem CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] : (HomologicalComplex.quasiIso C c).IsInvertedBy ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q)

noncomputable def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] : CategoryTheory.Functor (HomologicalComplexUpToQuasiIso C c) (HomologicalComplexUpToQuasiIso D c)

The functor HomologicalComplexUpToQuasiIso C c ⥤ HomologicalComplexUpToQuasiIso D c induced by a functor F : C ⥤ D which preserves homology.

Equations

• F.mapHomologicalComplexUpToQuasiIso c = (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).localizedFunctor HomologicalComplexUpToQuasiIso.Q HomologicalComplexUpToQuasiIso.Q

noncomputable instance CategoryTheory.Functor.instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] : CategoryTheory.Localization.Lifting HomologicalComplexUpToQuasiIso.Q (HomologicalComplex.quasiIso C c) ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q) (F.mapHomologicalComplexUpToQuasiIso c)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactors {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] : HomologicalComplexUpToQuasiIso.Q.comp (F.mapHomologicalComplexUpToQuasiIso c) ≅ (F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q

The functor F.mapHomologicalComplexUpToQuasiIso c is induced by F.mapHomologicalComplex c.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] : HomologicalComplexUpToQuasiIso.Qh.comp (F.mapHomologicalComplexUpToQuasiIso c) ≅ (F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh

The functor F.mapHomologicalComplexUpToQuasiIso c is induced by F.mapHomotopyCategory c.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.Functor.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] : CategoryTheory.Localization.Lifting HomologicalComplexUpToQuasiIso.Qh (HomotopyCategory.quasiIso C c) ((F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh) (F.mapHomologicalComplexUpToQuasiIso c)

Equations

• F.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso c = { iso' := F.mapHomologicalComplexUpToQuasiIsoFactorsh c }

theorem CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] (K : HomologicalComplex C c) {Z : HomologicalComplexUpToQuasiIso D c} (h : HomologicalComplexUpToQuasiIso.Qh.obj ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K)) h = CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K)) (CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K) (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K)) (CategoryTheory.CategoryStruct.comp (HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)) h)))

theorem CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.CategoryWithHomology D] [(HomologicalComplex.quasiIso C c).HasLocalization] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] (K : HomologicalComplex C c) : (F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K) = CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K)) (CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K) (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K)) (HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K))))