THe category of homological complexes is abelian

If C is an abelian category, then HomologicalComplex C c is an abelian category for any complex shape c : ComplexShape ι.

We also obtain that a short complex in HomologicalComplex C c is exact (resp. short exact) iff degreewise it is so.

instance HomologicalComplex.instIsNormalEpiCategory {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.IsNormalEpiCategory (HomologicalComplex C c)

instance HomologicalComplex.instIsNormalMonoCategory {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.IsNormalMonoCategory (HomologicalComplex C c)

@[instance_reducible]

noncomputable instance HomologicalComplex.instAbelian {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian (HomologicalComplex C c)

Equations

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

theorem HomologicalComplex.exact_of_degreewise_exact {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : ∀ (i : ι), (S.map (eval C c i)).Exact) : S.Exact

theorem HomologicalComplex.shortExact_of_degreewise_shortExact {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : ∀ (i : ι), (S.map (eval C c i)).ShortExact) : S.ShortExact

theorem HomologicalComplex.exact_iff_degreewise_exact {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) : S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact

theorem HomologicalComplex.shortExact_iff_degreewise_shortExact {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) : S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact

instance HomologicalComplex.instInjectiveXObjSingle {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i j : ι) (I : C) [CategoryTheory.Injective I] : CategoryTheory.Injective (((single C c i).obj I).X j)

instance HomologicalComplex.instProjectiveXObjSingle {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i j : ι) (P : C) [CategoryTheory.Projective P] : CategoryTheory.Projective (((single C c i).obj P).X j)

instance CategoryTheory.instPreservesLimitsOfShapeHomologicalComplexMapHomologicalComplexOfHasLimitsOfShape {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [F.PreservesZeroMorphisms] {J : Type u_4} [Category.{v_3, u_4} J] [Limits.HasLimitsOfShape J C] [Limits.PreservesLimitsOfShape J F] : Limits.PreservesLimitsOfShape J (F.mapHomologicalComplex c)

instance CategoryTheory.instPreservesColimitsOfShapeHomologicalComplexMapHomologicalComplexOfHasColimitsOfShape {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [F.PreservesZeroMorphisms] {J : Type u_4} [Category.{v_3, u_4} J] [Limits.HasColimitsOfShape J C] [Limits.PreservesColimitsOfShape J F] : Limits.PreservesColimitsOfShape J (F.mapHomologicalComplex c)

instance CategoryTheory.instPreservesFiniteLimitsHomologicalComplexMapHomologicalComplexOfHasFiniteLimits {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Limits.HasFiniteLimits C] [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] : Limits.PreservesFiniteLimits (F.mapHomologicalComplex c)

instance CategoryTheory.instPreservesFiniteColimitsHomologicalComplexMapHomologicalComplexOfHasFiniteColimits {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Limits.HasFiniteColimits C] [F.PreservesZeroMorphisms] [Limits.PreservesFiniteColimits F] : Limits.PreservesFiniteColimits (F.mapHomologicalComplex c)