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]
:
instance
HomologicalComplex.instIsNormalMonoCategory
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
:
@[implicit_reducible]
noncomputable instance
HomologicalComplex.instAbelian
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian 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)
:
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))
:
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))
:
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]
:
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]
:
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]
:
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]
: