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.

Equations

• K.cyclesMk x j hj hx = (K.sc i).cyclesMk x ⋯

@[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₂) : (ConcreteCategory.hom ((forget₂ C Ab).map (hS.δ i j hij))) x₃ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.homologyπ 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 : ι) : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.d j k))) x₁ = 0

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) : (ConcreteCategory.hom ((forget₂ C Ab).map (hS.δ i j hij))) ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyπ i))) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.homologyπ j))) (S.X₁.cyclesMk x₁ k hk ⋯)