Connecting a chain complex and a cochain complex

Given a chain complex K: ... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0, a cochain complex L: L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ..., a morphism d₀ : K.X 0 ⟶ L.X 0 satisfying the identifies K.d 1 0 ≫ d₀ = 0 and d₀ ≫ L.d 0 1 = 0, we construct a cochain complex indexed by ℤ of the form ... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ..., where K.X 0 lies in degree -1 and L.X 0 in degree 0.

Main definitions

Say K : ChainComplex C ℕ and L : CochainComplex C ℕ, so ... ⟶ K₂ ⟶ K₁ ⟶ K₀ and L⁰ ⟶ L¹ ⟶ L² ⟶ ....

• ConnectData K L: an auxiliary structure consisting of d₀ : K₀ ⟶ L⁰ "connecting" the complexes and proofs that the induced maps K₁ ⟶ K₀ ⟶ L⁰ and K₀ ⟶ L⁰ ⟶ L¹ are both zero.

Now say h : ConnectData K L.

• CochainComplex.ConnectData.cochainComplex h : the induced ℤ-indexed complex ... ⟶ K₁ ⟶ K₀ ⟶ L⁰ ⟶ L¹ ⟶ ...
• CochainComplex.ConnectData.homologyIsoPos h (n : ℕ) (m : ℤ) : if m = n + 1, the isomorphism h.cochainComplex.homology m ≅ L.homology (n + 1)
• CochainComplex.ConnectData.homologyIsoNeg h (n : ℕ) (m : ℤ) : if m = -(n + 2), the isomorphism h.cochainComplex.homology m ≅ K.homology (n + 1)

TODO

• Computation of h.cochainComplex.homology k when k = 0 or k = -1.

structure CochainComplex.ConnectData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : ChainComplex C ℕ) (L : CochainComplex C ℕ) : Type v

Given K : ChainComplex C ℕ and L : CochainComplex C ℕ, this data allows to connect K and L in order to get a cochain complex indexed by ℤ, see ConnectData.cochainComplex.

• d₀ : K.X 0 ⟶ L.X 0

  the differential which connect K and L

• comp_d₀ : CategoryTheory.CategoryStruct.comp (K.d 1 0) self.d₀ = 0
• d₀_comp : CategoryTheory.CategoryStruct.comp self.d₀ (L.d 0 1) = 0

@[simp]

theorem CochainComplex.ConnectData.comp_d₀_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (self : ConnectData K L) {Z : C} (h : L.X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d 1 0) (CategoryTheory.CategoryStruct.comp self.d₀ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CochainComplex.ConnectData.d₀_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (self : ConnectData K L) {Z : C} (h : L.X 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d₀ (CategoryTheory.CategoryStruct.comp (L.d 0 1) h) = CategoryTheory.CategoryStruct.comp 0 h

def CochainComplex.ConnectData.X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : ChainComplex C ℕ) (L : CochainComplex C ℕ) : ℤ → C

Auxiliary definition for ConnectData.cochainComplex.

@[simp]

theorem CochainComplex.ConnectData.X_ofNat {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (n : ℕ) : X K L ↑n = L.X n

@[simp]

theorem CochainComplex.ConnectData.X_negSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (n : ℕ) : X K L (Int.negSucc n) = K.X n

@[simp]

theorem CochainComplex.ConnectData.X_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} : X K L 0 = L.X 0

@[simp]

theorem CochainComplex.ConnectData.X_negOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} : X K L (-1) = K.X 0

def CochainComplex.ConnectData.d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m : ℤ) : X K L n ⟶ X K L m

Auxiliary definition for ConnectData.cochainComplex.

@[simp]

theorem CochainComplex.ConnectData.d_ofNat {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m : ℕ) : h.d ↑n ↑m = L.d n m

@[simp]

theorem CochainComplex.ConnectData.d_negSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m : ℕ) : h.d (Int.negSucc n) (Int.negSucc m) = K.d n m

@[simp]

theorem CochainComplex.ConnectData.d_sub_one_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : h.d (-1) 0 = h.d₀

@[simp]

theorem CochainComplex.ConnectData.d_zero_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : h.d 0 1 = L.d 0 1

@[simp]

theorem CochainComplex.ConnectData.d_sub_two_sub_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : h.d (-2) (-1) = K.d 1 0

theorem CochainComplex.ConnectData.shape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m : ℤ) (hnm : n + 1 ≠ m) : h.d n m = 0

@[simp]

theorem CochainComplex.ConnectData.d_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m p : ℤ) : CategoryTheory.CategoryStruct.comp (h.d n m) (h.d m p) = 0

@[simp]

theorem CochainComplex.ConnectData.d_comp_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m p : ℤ) {Z : C} (h✝ : X K L p ⟶ Z) : CategoryTheory.CategoryStruct.comp (h.d n m) (CategoryTheory.CategoryStruct.comp (h.d m p) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

def CochainComplex.ConnectData.cochainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : CochainComplex C ℤ

Given h : ConnectData K L where K : ChainComplex C ℕ and L : CochainComplex C ℕ, this is the cochain complex indexed by ℤ obtained by connecting K and L: ... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ....

@[simp]

theorem CochainComplex.ConnectData.cochainComplex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n m : ℤ) : h.cochainComplex.d n m = h.d n m

@[simp]

theorem CochainComplex.ConnectData.cochainComplex_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (a✝ : ℤ) : h.cochainComplex.X a✝ = X K L a✝

def CochainComplex.ConnectData.restrictionGEIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : HomologicalComplex.restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ≅ L

If h : ConnectData K L, then h.cochainComplex identifies to L in degrees ≥ 0.

@[simp]

theorem CochainComplex.ConnectData.restrictionGEIso_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (i : ℕ) : h.restrictionGEIso.hom.f i = (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom

@[simp]

theorem CochainComplex.ConnectData.restrictionGEIso_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (i : ℕ) : h.restrictionGEIso.inv.f i = (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).inv

def CochainComplex.ConnectData.restrictionLEIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : HomologicalComplex.restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ≅ K

If h : ConnectData K L, then h.cochainComplex identifies to K in degrees ≤ -1.

@[simp]

theorem CochainComplex.ConnectData.restrictionLEIso_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (i : ℕ) : h.restrictionLEIso.hom.f i = (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

@[simp]

theorem CochainComplex.ConnectData.restrictionLEIso_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (i : ℕ) : h.restrictionLEIso.inv.f i = (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv

noncomputable def CochainComplex.ConnectData.homologyIsoPos {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n : ℕ) (m : ℤ) [HomologicalComplex.HasHomology h.cochainComplex m] [HomologicalComplex.HasHomology L (n + 1)] (hm : m = ↑(n + 1)) : HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology L (n + 1)

Given h : ConnectData K L and n : ℕ, the homology of h.cochainComplex in degree n + 1 identifies to the homology of L in degree n + 1.

noncomputable def CochainComplex.ConnectData.homologyIsoNeg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) (n : ℕ) (m : ℤ) [HomologicalComplex.HasHomology h.cochainComplex m] [HomologicalComplex.HasHomology K (n + 1)] (hm : m = -↑(n + 2)) : HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology K (n + 1)

Given h : ConnectData K L and n : ℕ, the homology of h.cochainComplex in degree -(n + 2) identifies to the homology of K in degree n + 1.