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.

Equations

• CochainComplex.ConnectData.X K L (Int.ofNat n) = L.X n
• CochainComplex.ConnectData.X K L (Int.negSucc n) = K.X n

@[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.

Equations

• h.d (Int.ofNat n) (Int.ofNat m) = L.d n m
• h.d (Int.negSucc n) (Int.negSucc m) = K.d n m
• h.d (Int.negSucc 0) (Int.ofNat 0) = h.d₀
• h.d (Int.ofNat a) (Int.negSucc a_1) = 0
• h.d (Int.negSucc a) (Int.ofNat a_1) = 0

@[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 ⟶ ....

Equations

• h.cochainComplex = { X := CochainComplex.ConnectData.X K L, d := h.d, shape := ⋯, d_comp_d' := ⋯ }

@[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.

Equations

• h.restrictionGEIso = HomologicalComplex.Hom.isoOfComponents (fun (n : ℕ) => HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯) ⋯

@[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

@[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

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.

Equations

• h.restrictionLEIso = HomologicalComplex.Hom.isoOfComponents (fun (n : ℕ) => HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯) ⋯

@[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

@[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

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 : ℕ) [NeZero n] (m : ℤ) (hm : m = ↑n) [HomologicalComplex.HasHomology h.cochainComplex m] [HomologicalComplex.HasHomology L n] : HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology L n

Given h : ConnectData K L and n : ℕ non-zero, the homology of h.cochainComplex in degree n identifies to the homology of L in degree n.

Equations

• One or more equations did not get rendered due to their size.

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 : ℕ) [NeZero n] (m : ℤ) (hm : m = -↑(n + 1)) [HomologicalComplex.HasHomology h.cochainComplex m] [HomologicalComplex.HasHomology K n] : HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology K n

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

Equations

• One or more equations did not get rendered due to their size.

def CochainComplex.ConnectData.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : ConnectData K L) (h' : ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L') (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0)) : h.cochainComplex ⟶ h'.cochainComplex

Connecting complexes is functorial.

Equations

• h.map h' fK fL f_comm = { f := fun (x : ℤ) => match x with | Int.ofNat n => fL.f n | Int.negSucc n => fK.f n, comm' := ⋯ }

@[simp]

theorem CochainComplex.ConnectData.map_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : ConnectData K L) (h' : ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L') (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0)) (x✝ : ℤ) : (h.map h' fK fL f_comm).f x✝ = match x✝ with | Int.ofNat n => fL.f n | Int.negSucc n => fK.f n

@[simp]

theorem CochainComplex.ConnectData.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : ConnectData K L) : h.map h (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L) ⋯ = CategoryTheory.CategoryStruct.id h.cochainComplex

theorem CochainComplex.ConnectData.map_comp_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K K' K'' : ChainComplex C ℕ} {L L' L'' : CochainComplex C ℕ} (h : ConnectData K L) (h' : ConnectData K' L') (h'' : ConnectData K'' L'') (fK : K ⟶ K') (fL : L ⟶ L') (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0)) (fK' : K' ⟶ K'') (fL' : L' ⟶ L'') (f_comm' : CategoryTheory.CategoryStruct.comp (fK'.f 0) h''.d₀ = CategoryTheory.CategoryStruct.comp h'.d₀ (fL'.f 0)) : CategoryTheory.CategoryStruct.comp (h.map h' fK fL f_comm) (h'.map h'' fK' fL' f_comm') = h.map h'' (CategoryTheory.CategoryStruct.comp fK fK') (CategoryTheory.CategoryStruct.comp fL fL') ⋯

theorem CochainComplex.ConnectData.homologyMap_map_of_eq_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : ConnectData K L) (h' : ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L') (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0)) (n : ℕ) [NeZero n] (m : ℤ) (hmn : m = ↑n) [HomologicalComplex.HasHomology h.cochainComplex m] [HomologicalComplex.HasHomology L n] [HomologicalComplex.HasHomology h'.cochainComplex m] [HomologicalComplex.HasHomology L' n] : HomologicalComplex.homologyMap (h.map h' fK fL f_comm) m = CategoryTheory.CategoryStruct.comp (h.homologyIsoPos n m hmn).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap fL n) (h'.homologyIsoPos n m hmn).inv)

theorem CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : ConnectData K L) (h' : ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L') (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0)) (n : ℕ) [NeZero n] (m : ℤ) (hmn : m = -↑(n + 1)) [HomologicalComplex.HasHomology h.cochainComplex m] [HomologicalComplex.HasHomology K n] [HomologicalComplex.HasHomology h'.cochainComplex m] [HomologicalComplex.HasHomology K' n] : HomologicalComplex.homologyMap (h.map h' fK fL f_comm) m = CategoryTheory.CategoryStruct.comp (h.homologyIsoNeg n m hmn).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap fK n) (h'.homologyIsoNeg n m hmn).inv)