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

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_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

@[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

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.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

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))

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

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 ℤ))) ⋯

@[implicit_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.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.