Cochains from or to single complexes

We introduce constructors Cochain.fromSingleMk and Cocycle.fromSingleMk for cochains and cocycles from a single complex. We also introduce similar definitions for cochains and cocyles to a single complex.

noncomputable def CochainComplex.HomComplex.Cochain.fromSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} : p + n = q → Cochain ((singleFunctor C p).obj X) K n

Constructor for cochains from a single complex.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) (p q n : ℤ) (h : p + n = q) : fromSingleMk 0 h = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) : (fromSingleMk f h).v p q h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom f

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) : (fromSingleMk f h).v p' q' hpq' = 0

theorem CochainComplex.HomComplex.Cochain.δ_fromSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (n' q' : ℤ) (h' : p + n' = q') : δ n n' (fromSingleMk f h) = fromSingleMk (CategoryTheory.CategoryStruct.comp f (K.d q q')) h'

noncomputable def CochainComplex.HomComplex.Cochain.toSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} : p + n = q → Cochain K ((singleFunctor C q).obj X) n

Constructor for cochains to a single complex.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleMk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) (p q n : ℤ) (h : p + n = q) : toSingleMk 0 h = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleMk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) : (toSingleMk f h).v p q h = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv

theorem CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) : (toSingleMk f h).v p' q' hpq' = 0

theorem CochainComplex.HomComplex.Cochain.δ_toSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (n' p' : ℤ) (h' : p' + n' = q) : δ n n' (toSingleMk f h) = n'.negOnePow • toSingleMk (CategoryTheory.CategoryStruct.comp (K.d p' p) f) h'

noncomputable def CochainComplex.HomComplex.Cocycle.fromSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) : Cocycle ((singleFunctor C p).obj X) K n

Constructor for cocycles from a single complex.

Equations

• CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.fromSingleMk f h) (n + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) : ↑(fromSingleMk f h q' hq' hf) = Cochain.fromSingleMk f h

noncomputable def CochainComplex.HomComplex.Cocycle.toSingleMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) : Cocycle K ((singleFunctor C q).obj X) n

Constructor for cocycles to a single complex.

Equations

• CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.toSingleMk f h) (n + 1) ⋯ ⋯

@[simp]

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) : ↑(toSingleMk f h p' hp' hf) = Cochain.toSingleMk f h