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]
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
{ι : Type u_2}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
{i : ι}
(x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i)))
(j : ι)
(hj : c.next i = j)
(hx : (CategoryTheory.ConcreteCategory.hom ((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.
Instances For
@[simp]
theorem
HomologicalComplex.i_cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
{ι : Type u_2}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
{i : ι}
(x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i)))
(j : ι)
(hj : c.next i = j)
(hx : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.d i j))) x = 0)
:
(CategoryTheory.ConcreteCategory.hom ((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]
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{ι : Type u_2}
{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₂ :
(ConcreteCategory.hom ((forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i))) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyι i))) x₃)
(h₁ :
(ConcreteCategory.hom ((forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.opcyclesToCycles i j))) x₂)
:
theorem
CategoryTheory.ShortComplex.ShortExact.δ_apply
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{ι : Type u_2}
{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₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0)
(x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i)))
(hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃)
(x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j)))
(hx₁ :
(ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂)
(k : ι)
(hk : c.next j = k)
: