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.

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_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✝

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