Homology of complexes in concrete categories #
The homology of short complexes in concrete categories was studied in
Mathlib.Algebra.Homology.ShortComplex.HasForget. In this file,
we introduce specific definitions and lemmas for the homology
of homological complexes in concrete categories. In particular,
we give a computation of the connecting homomorphism of
the homology sequence in terms of (co)cycles.
noncomputable def
HomologicalComplex.cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.HasForget C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
{ι : Type u_1}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
{i : ι}
(x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i)))
(j : ι)
(hj : c.next i = j)
(hx : ((CategoryTheory.forget₂ C Ab).map (K.d i j)) x = 0)
:
↑((CategoryTheory.forget₂ C Ab).obj (K.cycles i))
Constructor for cycles of a homological complex in a concrete category.
Equations
- K.cyclesMk x j hj hx = (K.sc i).cyclesMk x ⋯
Instances For
@[simp]
theorem
HomologicalComplex.i_cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.HasForget C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
{ι : Type u_1}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
{i : ι}
(x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i)))
(j : ι)
(hj : c.next i = j)
(hx : ((CategoryTheory.forget₂ C Ab).map (K.d i j)) x = 0)
:
((CategoryTheory.forget₂ C Ab).map (K.iCycles i)) (K.cyclesMk x j hj hx) = x
theorem
CategoryTheory.ShortComplex.ShortExact.δ_apply'
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{ι : Type u_1}
{c : ComplexShape ι}
{S : ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
(x₃ : ↑((forget₂ C Ab).obj (S.X₃.homology i)))
(x₂ : ↑((forget₂ C Ab).obj (S.X₂.opcycles i)))
(x₁ : ↑((forget₂ C Ab).obj (S.X₁.cycles j)))
(h₂ : ((forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i)) x₂ = ((forget₂ C Ab).map (S.X₃.homologyι i)) x₃)
(h₁ :
((forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)) x₂)
:
theorem
CategoryTheory.ShortComplex.ShortExact.δ_apply
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{ι : Type u_1}
{c : ComplexShape ι}
{S : ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
(x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i)))
(hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0)
(x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i)))
(hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃)
(x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j)))
(hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂)
(k : ι)
(hk : c.next j = k)
: