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.
noncomputable instance
HomologicalComplex.instNormalEpiCategory
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
HomologicalComplex.instNormalMonoCategory
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
HomologicalComplex.instAbelian
{C : Type u_1}
{ι : Type u_2}
{c : ComplexShape ι}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
:
Equations
- HomologicalComplex.instAbelian = CategoryTheory.Abelian.mk
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 (HomologicalComplex.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 (HomologicalComplex.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))
:
S.Exact ↔ ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).Exact
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))
:
S.ShortExact ↔ ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).ShortExact