Homology of complexes in concrete categories #
The homology of short complexes in concrete categories was studied in
Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory. 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.ConcreteCategory 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.ConcreteCategory 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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
(x₃ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₃.homology i)))
(x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.opcycles i)))
(x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.cycles j)))
(h₂ : ((CategoryTheory.forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i)) x₂ = ((CategoryTheory.forget₂ C Ab).map (S.X₃.homologyι i)) x₃)
(h₁ : ((CategoryTheory.forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j)) x₁ = ((CategoryTheory.forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)) x₂)
:
((CategoryTheory.forget₂ C Ab).map (hS.δ i j hij)) x₃ = ((CategoryTheory.forget₂ C Ab).map (S.X₁.homologyπ j)) x₁
theorem
CategoryTheory.ShortComplex.ShortExact.δ_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
(x₃ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₃.X i)))
(hx₃ : ((CategoryTheory.forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0)
(x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.X i)))
(hx₂ : ((CategoryTheory.forget₂ C Ab).map (S.g.f i)) x₂ = x₃)
(x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.X j)))
(hx₁ : ((CategoryTheory.forget₂ C Ab).map (S.f.f j)) x₁ = ((CategoryTheory.forget₂ C Ab).map (S.X₂.d i j)) x₂)
(k : ι)
(hk : c.next j = k)
:
((CategoryTheory.forget₂ C Ab).map (hS.δ i j hij))
(((CategoryTheory.forget₂ C Ab).map (S.X₃.homologyπ i)) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) = ((CategoryTheory.forget₂ C Ab).map (S.X₁.homologyπ j)) (S.X₁.cyclesMk x₁ k hk ⋯)