Bounded below cochain complexes

In this file, we consider the full subcategory CochainComplex.Plus C of CochainComplex C ℤ consisting of bounded below cocahin complexes in a category C.

def CochainComplex.plus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ObjectProperty (CochainComplex C ℤ)

The property of cochain complexes that are bounded below.

Equations

• CochainComplex.plus C K = ∃ (n : ℤ), K.IsStrictlyGE n

theorem CochainComplex.plus_iff (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) : CochainComplex.plus C K ↔ ∃ (n : ℤ), K.IsStrictlyGE n

instance CochainComplex.instIsClosedUnderIsomorphismsIntPlus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CochainComplex.plus C).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev CochainComplex.Plus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Type (max u_1 v_1)

The full subcategory of CochainComplex C ℤ consisting of bounded below complexes.

Equations

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

@[reducible, inline]

abbrev CochainComplex.Plus.ι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (Plus C) (CochainComplex C ℤ)

The inclusion of the full subcategory of bounded below cochain complexes.

Equations

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

def CochainComplex.Plus.fullyFaithfulι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (ι C).FullyFaithful

The inclusion of the full subcategory of bounded below cochain complexes is fully faithful.

Equations

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

instance CochainComplex.Plus.instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (J : Type u_2) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [CategoryTheory.Limits.HasLimitsOfShape J C] : (CochainComplex.plus C).IsClosedUnderLimitsOfShape J

instance CochainComplex.Plus.instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (J : Type u_2) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [CategoryTheory.Limits.HasColimitsOfShape J C] : (CochainComplex.plus C).IsClosedUnderColimitsOfShape J

instance CochainComplex.Plus.instHasFiniteLimits (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (Plus C)

instance CochainComplex.Plus.instHasFiniteColimits (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (Plus C)

theorem CochainComplex.Plus.mono_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] {X Y : Plus C} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ CategoryTheory.Mono f.hom

def CochainComplex.Plus.quasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : CategoryTheory.MorphismProperty (Plus C)

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

Equations

• CochainComplex.Plus.quasiIso C = (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C)

instance CochainComplex.Plus.instHasTwoOutOfThreePropertyQuasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : (quasiIso C).HasTwoOutOfThreeProperty

instance CochainComplex.Plus.instIsStableUnderRetractsQuasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : (quasiIso C).IsStableUnderRetracts

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

def CategoryTheory.Functor.mapCochainComplexPlus {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] : Functor (CochainComplex.Plus C) (CochainComplex.Plus D)

The functor on categories of bounded below cochain complexes that is induced by a functor (which preserves zero morphisms).

Equations

• F.mapCochainComplexPlus = (CochainComplex.plus D).lift ((CochainComplex.Plus.ι C).comp (F.mapHomologicalComplex (ComplexShape.up ℤ))) ⋯

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_X {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (i : ℤ) : (F.mapCochainComplexPlus.obj X).obj.X i = F.obj (X.obj.X i)

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_d {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (i j : ℤ) : (F.mapCochainComplexPlus.obj X).obj.d i j = F.map (X.obj.d i j)

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] {X✝ Y✝ : CochainComplex.Plus C} (f : X✝ ⟶ Y✝) (i : ℤ) : (F.mapCochainComplexPlus.map f).hom.f i = F.map (f.hom.f i)

def CategoryTheory.Functor.mapCochainComplexPlusCompι {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] : F.mapCochainComplexPlus.comp (CochainComplex.Plus.ι D) ≅ (CochainComplex.Plus.ι C).comp (F.mapHomologicalComplex (ComplexShape.up ℤ))

The isomorphism between F.mapCochainComplexPlus ⋙ CochainComplex.Plus.ι D and CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex _ when F : C ⥤ D is a functor which preserves zero morphisms

Equations

• F.mapCochainComplexPlusCompι = CategoryTheory.Iso.refl (F.mapCochainComplexPlus.comp (CochainComplex.Plus.ι D))

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (x✝ : ℤ) : (F.mapCochainComplexPlusCompι.inv.app X).f x✝ = CategoryStruct.id (F.obj (X.obj.X x✝))

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (x✝ : ℤ) : (F.mapCochainComplexPlusCompι.hom.app X).f x✝ = CategoryStruct.id (F.obj (X.obj.X x✝))