Homology of complexes in concrete categories #
The homology of short complexes in concrete categories was studied in
Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean. 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.d_eq_zero_of_f_eq_d_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 : ι)
(x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i)))
(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 : ι)
:
In the short exact sequence of complexes
0 0 0
| | |
v v v
...-> X_1,i -----> X_1,j --d--> X_1,k ->...
| | |
| f | |
v v v
...-> X_2,i --d--> X_2,j -----> X_2,k ->...
| | |
v v v
...-> X_3,i -----> X_3,j -----> X_3,k ->...
| | |
v v v
0 0 0
if x₁ ∈ X_1,j and x₂ ∈ X_2,i and if f(x₁) = d(x₂) then d(x₁) = 0.
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)
: