The triangulated subcategory of bounded below cochain complexes up to homotopy

In this file, we introduce the triangulated full subcategory HomotopyCategory.Plus C of HomotopyCategory C (.up ℤ) consisting of bounded below cochain complexes.

theorem CochainComplex.plus_cylinder {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : CochainComplex C ℤ) (hK : CochainComplex.plus C K) : CochainComplex.plus C (HomologicalComplex.cylinder K)

theorem CochainComplex.plus_pathObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : CochainComplex C ℤ) (hK : CochainComplex.plus C K) : CochainComplex.plus C (HomologicalComplex.pathObject K)

theorem CochainComplex.isStrictlyGE_mappingCone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n₁ n₂ n : ℤ) [K.IsStrictlyGE n₁] [L.IsStrictlyGE n₂] (hn₁ : n < n₁ := by lia) (hn₂ : n ≤ n₂ := by lia) : (mappingCone f).IsStrictlyGE n

@[reducible, inline]

noncomputable abbrev CochainComplex.Plus.precylinder {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : Plus C) : HomotopicalAlgebra.Precylinder K

The pre-cylinder object attached to K : Plus C.

Equations

• K.precylinder = (HomologicalComplex.precylinder K.obj).toFullSubcategory ⋯

@[reducible, inline]

noncomputable abbrev CochainComplex.Plus.prepathObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : Plus C) : HomotopicalAlgebra.PrepathObject K

The pre-path object attached to K : Plus C.

Equations

• K.prepathObject = (HomologicalComplex.prepathObject K.obj).toFullSubcategory ⋯

def HomotopyCategory.plus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))

The property of objects in HomotopyCategory C (.up ℤ) whose underlying cochain complex is bounded below. (Note: this property of objects is not closed under isomorphisms.)

Equations

• HomotopyCategory.plus C = (CochainComplex.plus C).strictMap (HomotopyCategory.quotient C (ComplexShape.up ℤ))

@[simp]

theorem HomotopyCategory.plus_quotient_obj_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : plus C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ CochainComplex.plus C K

instance HomotopyCategory.instContainsZeroIntUpPlusOfHasZeroObject (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : (plus C).ContainsZero

instance HomotopyCategory.instIsStableUnderShiftIntUpPlus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (plus C).IsStableUnderShift ℤ

instance HomotopyCategory.instIsTriangulatedClosed₃IntUpPlus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (plus C).IsTriangulatedClosed₃

instance HomotopyCategory.instIsTriangulatedIntUpPlus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (plus C).IsTriangulated

@[reducible, inline]

abbrev HomotopyCategory.Plus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : Type (max u_1 v_1)

The homotopy category of bounded below cochain complexes.

Equations

• HomotopyCategory.Plus C = (HomotopyCategory.plus C).FullSubcategory

@[reducible, inline]

abbrev HomotopyCategory.Plus.ι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (Plus C) (HomotopyCategory C (ComplexShape.up ℤ))

The inclusion of the homotopy category of bounded below cochain complexes in the homotopy category category of all cochain complexes.

Equations

• HomotopyCategory.Plus.ι C = (HomotopyCategory.plus C).ι

@[reducible, inline]

abbrev HomotopyCategory.Plus.fullyFaithfulι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (ι C).FullyFaithful

The inclusion functor HomotopyCategory.ι C : HomotopyCategory.Plus C ⥤ HomotopyCategory C (.up ℤ) is fully faithful.

Equations

• HomotopyCategory.Plus.fullyFaithfulι C = (HomotopyCategory.plus C).fullyFaithfulι

def HomotopyCategory.Plus.quasiIso (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Abelian A] : CategoryTheory.MorphismProperty (Plus A)

The class of quasi-isomorphisms in the homotopy category of bounded below cochain complexes.

Equations

• HomotopyCategory.Plus.quasiIso A = (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)).inverseImage (HomotopyCategory.Plus.ι A)

instance HomotopyCategory.Plus.instIsMultiplicativeQuasiIso (A : Type u_2) [CategoryTheory.Category.{u_1, u_2} A] [CategoryTheory.Abelian A] : (quasiIso A).IsMultiplicative

theorem HomotopyCategory.Plus.quasiIso_iff (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Abelian A] {K L : Plus A} (f : K ⟶ L) : quasiIso A f ↔ HomotopyCategory.quasiIso A (ComplexShape.up ℤ) f.hom

instance HomotopyCategory.Plus.instIsCompatibleWithShiftQuasiIsoInt (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Abelian A] : (quasiIso A).IsCompatibleWithShift ℤ

instance HomotopyCategory.Plus.instRespectsIsoQuasiIso (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Abelian A] : (quasiIso A).RespectsIso

@[implicit_reducible]

def HomotopyCategory.Plus.quotient (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (CochainComplex.Plus C) (Plus C)

The full and essentially surjective functor CochainComplex.Plus C ⥤ HomotopyCategory.Plus C.

Equations

• HomotopyCategory.Plus.quotient C = (HomotopyCategory.plus C).lift ((CochainComplex.Plus.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))) ⋯

@[simp]

theorem HomotopyCategory.Plus.quotient_obj_obj_as (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CochainComplex.Plus C) : ((quotient C).obj X).obj.as = X.obj

@[simp]

theorem HomotopyCategory.Plus.quotient_map_hom (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X✝ Y✝ : CochainComplex.Plus C} (f : X✝ ⟶ Y✝) : ((quotient C).map f).hom = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f.hom

def HomotopyCategory.Plus.quotientCompιIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (quotient C).comp (ι C) ≅ (CochainComplex.Plus.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))

The functor HomotopyCategory.Plus.quotient C : CochainComplex.Plus C ⥤ HomotopyCategory.Plus C is induced by the functor HomotopyCategory.quotient C (.up ℤ) from CochainComplex C ℤ to HomotopyCategory C (.up ℤ).

Equations

• HomotopyCategory.Plus.quotientCompιIso C = (HomotopyCategory.plus C).liftCompιIso ((CochainComplex.Plus.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))) ⋯

theorem HomotopyCategory.Plus.quotientCompιIso_inv_app (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CochainComplex.Plus C) : (quotientCompιIso C).inv.app X = CategoryTheory.CategoryStruct.id ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X.obj)

theorem HomotopyCategory.Plus.quotientCompιIso_hom_app (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CochainComplex.Plus C) : (quotientCompιIso C).hom.app X = CategoryTheory.CategoryStruct.id ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X.obj)

@[instance_reducible]

noncomputable instance HomotopyCategory.Plus.instCommShiftPlusQuotientInt (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (quotient C).CommShift ℤ

Equations

• HomotopyCategory.Plus.instCommShiftPlusQuotientInt C = (HomotopyCategory.plus C).commShiftLift ((CochainComplex.Plus.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))) ⋯

instance HomotopyCategory.Plus.instCommShiftPlusIntUpHomFunctorQuotientCompιIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.NatTrans.CommShift (quotientCompιIso C).hom ℤ

theorem HomotopyCategory.Plus.quotient_obj_surjective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : Function.Surjective (quotient C).obj

instance HomotopyCategory.Plus.instEssSurjPlusQuotient (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (quotient C).EssSurj

instance HomotopyCategory.Plus.instFullPlusQuotient (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (quotient C).Full

theorem HomotopyCategory.Plus.quasiIso_map_quotient_eq_quasiIso (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Abelian A] : (CochainComplex.Plus.quasiIso A).map (quotient A) = quasiIso A

instance HomotopyCategory.Plus.instIsLocalizationPlusQuotientInverseImageHomologicalComplexIntUpHomotopyEquivalencesι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (quotient C).IsLocalization ((HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C))

instance HomotopyCategory.Plus.instIsLocalizationPlusCompQuotientQuasiIsoOfQuasiIso (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Abelian A] {H : Type u_4} [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor (Plus A) H) [L.IsLocalization (quasiIso A)] : ((quotient A).comp L).IsLocalization (CochainComplex.Plus.quasiIso A)

noncomputable def HomotopyCategory.Plus.singleFunctors (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.SingleFunctors C (Plus C) ℤ

The collection of all single functors C ⥤ HomotopyCategory.Plus C for n : ℤ along with their compatibilities with shifts.

Equations

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

@[reducible, inline]

noncomputable abbrev HomotopyCategory.Plus.singleFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : CategoryTheory.Functor C (Plus C)

The single functor C ⥤ HomotopyCategory.Plus C.

Equations

• HomotopyCategory.Plus.singleFunctor C n = (HomotopyCategory.Plus.singleFunctors C).functor n

noncomputable def HomotopyCategory.Plus.singleFunctorCompιIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : (singleFunctor C n).comp (ι C) ≅ HomotopyCategory.singleFunctor C n

The single functor C ⥤ HomotopyCategory.Plus C is induced by HomotopyCategory.singleFunctor C n : C ⥤ HomotopyCategory C (.up ℤ).

Equations

• HomotopyCategory.Plus.singleFunctorCompιIso C n = CategoryTheory.Iso.refl ((HomotopyCategory.Plus.singleFunctor C n).comp (HomotopyCategory.Plus.ι C))

instance HomotopyCategory.Plus.instAdditiveSingleFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : (singleFunctor C n).Additive

@[implicit_reducible]

def CategoryTheory.Functor.mapHomotopyCategoryPlus {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : Functor (HomotopyCategory.Plus C) (HomotopyCategory.Plus D)

The functor between bounded below homotopy categories that is induced by an additive functor.

Equations

• F.mapHomotopyCategoryPlus = (HomotopyCategory.plus D).lift ((HomotopyCategory.Plus.ι C).comp (F.mapHomotopyCategory (ComplexShape.up ℤ))) ⋯

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instCommShiftPlusMapHomotopyCategoryPlusInt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : F.mapHomotopyCategoryPlus.CommShift ℤ

Equations

• F.instCommShiftPlusMapHomotopyCategoryPlusInt = { commShiftIso := CategoryTheory.Functor.instCommShiftPlusMapHomotopyCategoryPlusInt._aux_1 F, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

instance CategoryTheory.Functor.instIsTriangulatedPlusMapHomotopyCategoryPlus {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [Limits.HasZeroObject C] [Limits.HasBinaryBiproducts C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts D] : F.mapHomotopyCategoryPlus.IsTriangulated

instance CategoryTheory.Functor.instFullPlusMapHomotopyCategoryPlusOfFaithful {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [F.Full] [F.Faithful] : F.mapHomotopyCategoryPlus.Full

instance CategoryTheory.Functor.instFaithfulPlusMapHomotopyCategoryPlusOfFull {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [F.Full] [F.Faithful] : F.mapHomotopyCategoryPlus.Faithful

def CategoryTheory.Functor.mapHomotopyCategoryPlusCompι {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : F.mapHomotopyCategoryPlus.comp (HomotopyCategory.Plus.ι D) ≅ (HomotopyCategory.Plus.ι C).comp (F.mapHomotopyCategory (ComplexShape.up ℤ))

The functor F.mapHomotopyCategoryPlus : HomotopyCategory.Plus C ⥤ HomotopyCategory.Plus D is induced by F.mapHomotopyCategory (.up ℤ).

Equations

• F.mapHomotopyCategoryPlusCompι = CategoryTheory.Iso.refl (F.mapHomotopyCategoryPlus.comp (HomotopyCategory.Plus.ι D))

theorem CategoryTheory.Functor.mapHomotopyCategoryPlusCompι_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] (X : HomotopyCategory.Plus C) : F.mapHomotopyCategoryPlusCompι.hom.app X = CategoryStruct.id (F.mapHomotopyCategoryPlus.obj X).obj

theorem CategoryTheory.Functor.mapHomotopyCategoryPlusCompι_inv_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] (X : HomotopyCategory.Plus C) : F.mapHomotopyCategoryPlusCompι.inv.app X = CategoryStruct.id (F.mapHomotopyCategoryPlus.obj X).obj

instance CategoryTheory.Functor.instCommShiftPlusHomotopyCategoryIntUpHomMapHomotopyCategoryPlusCompι {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : NatTrans.CommShift F.mapHomotopyCategoryPlusCompι.hom ℤ

def CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : (HomotopyCategory.Plus.quotient C).comp F.mapHomotopyCategoryPlus ≅ F.mapCochainComplexPlus.comp (HomotopyCategory.Plus.quotient D)

The functor F.mapHomotopyCategoryPlus : HomotopyCategory.Plus C ⥤ HomotopyCategory.Plus D is induced by F.mapCochainComplexPlus.

Equations

• F.quotientCompMapHomotopyCategoryPlusIso = CategoryTheory.Iso.refl ((HomotopyCategory.Plus.quotient C).comp F.mapHomotopyCategoryPlus)

theorem CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIso_inv_app_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] (X : CochainComplex.Plus C) : (F.quotientCompMapHomotopyCategoryPlusIso.inv.app X).hom = CategoryStruct.id (F.mapHomotopyCategoryPlus.obj ((HomotopyCategory.Plus.quotient C).obj X)).obj

theorem CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIso_hom_app_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] (X : CochainComplex.Plus C) : (F.quotientCompMapHomotopyCategoryPlusIso.hom.app X).hom = CategoryStruct.id (F.mapHomotopyCategoryPlus.obj ((HomotopyCategory.Plus.quotient C).obj X)).obj

theorem CategoryTheory.Functor.whiskerRight_quotientCompMapHomotopyCategoryPlusIso_hom_ι {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : whiskerRight F.quotientCompMapHomotopyCategoryPlusIso.hom (HomotopyCategory.Plus.ι D) = CategoryStruct.comp ((HomotopyCategory.Plus.quotient C).associator F.mapHomotopyCategoryPlus (HomotopyCategory.Plus.ι D)).hom (CategoryStruct.comp ((HomotopyCategory.Plus.quotient C).whiskerLeft F.mapHomotopyCategoryPlusCompι.hom) (CategoryStruct.comp ((HomotopyCategory.Plus.quotient C).associator (HomotopyCategory.Plus.ι C) (F.mapHomotopyCategory (ComplexShape.up ℤ))).inv (CategoryStruct.comp (whiskerRight (HomotopyCategory.Plus.quotientCompιIso C).hom (F.mapHomotopyCategory (ComplexShape.up ℤ))) (CategoryStruct.comp ((CochainComplex.Plus.ι C).associator (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (F.mapHomotopyCategory (ComplexShape.up ℤ))).hom (CategoryStruct.comp ((CochainComplex.Plus.ι C).whiskerLeft (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom) (CategoryStruct.comp ((CochainComplex.Plus.ι C).associator (F.mapHomologicalComplex (ComplexShape.up ℤ)) (HomotopyCategory.quotient D (ComplexShape.up ℤ))).inv (CategoryStruct.comp (whiskerRight F.mapCochainComplexPlusCompι.inv (HomotopyCategory.quotient D (ComplexShape.up ℤ))) (CategoryStruct.comp (F.mapCochainComplexPlus.associator (CochainComplex.Plus.ι D) (HomotopyCategory.quotient D (ComplexShape.up ℤ))).hom (CategoryStruct.comp (F.mapCochainComplexPlus.whiskerLeft (HomotopyCategory.Plus.quotientCompιIso D).inv) (F.mapCochainComplexPlus.associator (HomotopyCategory.Plus.quotient D) (HomotopyCategory.Plus.ι D)).inv)))))))))

theorem CategoryTheory.Functor.whiskerRight_quotientCompMapHomotopyCategoryPlusIso_hom_ι_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {Z : Functor (CochainComplex.Plus C) (HomotopyCategory D (ComplexShape.up ℤ))} (h : (F.mapCochainComplexPlus.comp (HomotopyCategory.Plus.quotient D)).comp (HomotopyCategory.Plus.ι D) ⟶ Z) : CategoryStruct.comp (whiskerRight F.quotientCompMapHomotopyCategoryPlusIso.hom (HomotopyCategory.Plus.ι D)) h = CategoryStruct.comp ((HomotopyCategory.Plus.quotient C).associator F.mapHomotopyCategoryPlus (HomotopyCategory.Plus.ι D)).hom (CategoryStruct.comp ((HomotopyCategory.Plus.quotient C).whiskerLeft F.mapHomotopyCategoryPlusCompι.hom) (CategoryStruct.comp ((HomotopyCategory.Plus.quotient C).associator (HomotopyCategory.Plus.ι C) (F.mapHomotopyCategory (ComplexShape.up ℤ))).inv (CategoryStruct.comp (whiskerRight (HomotopyCategory.Plus.quotientCompιIso C).hom (F.mapHomotopyCategory (ComplexShape.up ℤ))) (CategoryStruct.comp ((CochainComplex.Plus.ι C).associator (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (F.mapHomotopyCategory (ComplexShape.up ℤ))).hom (CategoryStruct.comp ((CochainComplex.Plus.ι C).whiskerLeft (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom) (CategoryStruct.comp ((CochainComplex.Plus.ι C).associator (F.mapHomologicalComplex (ComplexShape.up ℤ)) (HomotopyCategory.quotient D (ComplexShape.up ℤ))).inv (CategoryStruct.comp (whiskerRight F.mapCochainComplexPlusCompι.inv (HomotopyCategory.quotient D (ComplexShape.up ℤ))) (CategoryStruct.comp (F.mapCochainComplexPlus.associator (CochainComplex.Plus.ι D) (HomotopyCategory.quotient D (ComplexShape.up ℤ))).hom (CategoryStruct.comp (F.mapCochainComplexPlus.whiskerLeft (HomotopyCategory.Plus.quotientCompιIso D).inv) (CategoryStruct.comp (F.mapCochainComplexPlus.associator (HomotopyCategory.Plus.quotient D) (HomotopyCategory.Plus.ι D)).inv h))))))))))

instance CategoryTheory.Functor.instCommShiftPlusPlusHomQuotientCompMapHomotopyCategoryPlusIsoInt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : NatTrans.CommShift F.quotientCompMapHomotopyCategoryPlusIso.hom ℤ

def CategoryTheory.Functor.mapHomotopyCategoryPlusCompIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {E : Type u_4} [Category.{v_4, u_4} E] [Preadditive E] {F : Functor C D} {G : Functor D E} {H : Functor C E} (e : F.comp G ≅ H) [F.Additive] [G.Additive] [H.Additive] : F.mapHomotopyCategoryPlus.comp G.mapHomotopyCategoryPlus ≅ H.mapHomotopyCategoryPlus

Given additive functors that are related by an isomorphism F ⋙ G ≅ H, this is the corresponding isomorphism on the corresponding functor between the bounded below homotopy categories.

Equations

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