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_2) [CategoryTheory.Category.{v_2, u_2} 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_2) [CategoryTheory.Category.{v_2, u_2} 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_2) [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Abelian A] : (quasiIso A).IsCompatibleWithShift ℤ

instance HomotopyCategory.Plus.instRespectsIsoQuasiIso (A : Type u_2) [CategoryTheory.Category.{v_2, u_2} 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