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.{u_3, u_1} C]
[CategoryTheory.Abelian C]
:
instance
HomologicalComplex.instIsNormalMonoCategory
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
:
noncomputable instance
HomologicalComplex.instAbelian
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
:
theorem
HomologicalComplex.exact_of_degreewise_exact
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{u_3, 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.{u_3, 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.{u_3, 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.{u_3, u_1} C]
[CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex (HomologicalComplex C c))
: