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 cocycles to a single complex.

source

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.

Instances For

source

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

source

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

source

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

source

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'

source

noncomputable def CochainComplex.HomComplex.Cochain.fromSingleEquiv {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) :

Cochain ((singleFunctor C p).obj X) K n ≃+ (X ⟶ K.X q)

Cochains of degree n from (singleFunctor C p).obj X to K identify to X ⟶ K.X q when p + n = q.

Equations

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

Instances For

source

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleEquiv_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) :

(fromSingleEquiv h) (fromSingleMk f h) = f

source

@[simp]

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

fromSingleMk (f + g) h = fromSingleMk f h + fromSingleMk g h

source

@[simp]

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

fromSingleMk (f - g) h = fromSingleMk f h - fromSingleMk g h

source

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_neg {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 = -fromSingleMk f h

source

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

∃ (f : X ⟶ K.X q), fromSingleMk f h = α

source

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

fromSingleMk (CategoryTheory.CategoryStruct.comp g f) h = (ofHom ((singleFunctor C p).map g)).comp (fromSingleMk f h) ⋯

source

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp {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) {L : CochainComplex C ℤ} (g : K ⟶ L) :

fromSingleMk (CategoryTheory.CategoryStruct.comp f (g.f q)) h = (fromSingleMk f h).comp (ofHom g) ⋯

source

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.

Instances For

source

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

source

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

source

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

source

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'

source

noncomputable def CochainComplex.HomComplex.Cochain.toSingleEquiv {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) :

Cochain K ((singleFunctor C q).obj X) n ≃+ (K.X p ⟶ X)

Cochains of degree n from (singleFunctor C q).obj X to K identify to K.X p ⟶ X when p + n = q.

Equations

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

Instances For

source

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleEquiv_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) :

(toSingleEquiv h) (toSingleMk f h) = f

source

@[simp]

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

toSingleMk (f + g) h = toSingleMk f h + toSingleMk g h

source

@[simp]

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

toSingleMk (f - g) h = toSingleMk f h - toSingleMk g h

source

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleMk_neg {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 = -toSingleMk f h

source

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

∃ (f : K.X p ⟶ X), toSingleMk f h = α

source

theorem CochainComplex.HomComplex.Cochain.toSingleMk_postcomp {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) {X' : C} (g : X ⟶ X') :

toSingleMk (CategoryTheory.CategoryStruct.comp f g) h = (toSingleMk f h).comp (ofHom ((singleFunctor C q).map g)) ⋯

source

theorem CochainComplex.HomComplex.Cochain.toSingleMk_precomp {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) {L : CochainComplex C ℤ} (g : L ⟶ K) :

toSingleMk (CategoryTheory.CategoryStruct.comp (g.f p) f) h = (ofHom g).comp (toSingleMk f h) ⋯

source

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) ⋯ ⋯

Instances For

source

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

source

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {X' : C} (g : X' ⟶ X) {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 (CategoryTheory.CategoryStruct.comp g f) h q' hq' ⋯ = (fromSingleMk f h q' hq' hf).precomp ((singleFunctor C p).map g)

source

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp {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) {L : CochainComplex C ℤ} (g : K ⟶ L) :

fromSingleMk (CategoryTheory.CategoryStruct.comp f (g.f q)) h q' hq' ⋯ = (fromSingleMk f h q' hq' hf).postcomp g

source

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p n : ℤ} (α : Cocycle ((singleFunctor C p).obj X) K n) (q : ℤ) (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') :

∃ (f : X ⟶ K.X q) (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0), fromSingleMk f h q' hq' hf = α

source

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

fromSingleMk (f + g) h q' hq' ⋯ = fromSingleMk f h q' hq' hf + fromSingleMk g h q' hq' hg

source

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

fromSingleMk (f - g) h q' hq' ⋯ = fromSingleMk f h q' hq' hf - fromSingleMk g h q' hq' hg

source

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_neg {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' ⋯ = -fromSingleMk f h q' hq' hf

source

@[simp]

theorem CochainComplex.HomComplex.Cocycle.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) (q' : ℤ) (hq' : q + 1 = q') :

fromSingleMk 0 h q' hq' ⋯ = 0

source

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff {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) (q'' : ℤ) (hq'' : q'' + 1 = q) :

fromSingleMk f h q' hq' hf ∈ coboundaries ((singleFunctor C p).obj X) K n ↔ ∃ (g : X ⟶ K.X q''), CategoryTheory.CategoryStruct.comp g (K.d q'' q) = f

source

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) ⋯ ⋯

Instances For

source

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

source

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp {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) {X' : C} (g : X ⟶ X') :

toSingleMk (CategoryTheory.CategoryStruct.comp f g) h p' hp' ⋯ = (toSingleMk f h p' hp' hf).postcomp ((singleFunctor C q).map g)

source

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_precomp {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) {L : CochainComplex C ℤ} (g : L ⟶ K) :

toSingleMk (CategoryTheory.CategoryStruct.comp (g.f p) f) h p' hp' ⋯ = (toSingleMk f h p' hp' hf).precomp g

source

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {q n : ℤ} (α : Cocycle K ((singleFunctor C q).obj X) n) (p : ℤ) (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) :

∃ (f : K.X p ⟶ X) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0), toSingleMk f h p' hp' hf = α

source

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

toSingleMk (f + g) h p' hp' ⋯ = toSingleMk f h p' hp' hf + toSingleMk g h p' hp' hg

source

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

toSingleMk (f - g) h p' hp' ⋯ = toSingleMk f h p' hp' hf - toSingleMk g h p' hp' hg

source

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_neg {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' ⋯ = -toSingleMk f h p' hp' hf

source

@[simp]

theorem CochainComplex.HomComplex.Cocycle.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) (p' : ℤ) (hp' : p' + 1 = p) :

toSingleMk 0 h p' hp' ⋯ = 0

source

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff {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) (p'' : ℤ) (hp'' : p + 1 = p'') :

toSingleMk f h p' hp' hf ∈ coboundaries K ((singleFunctor C q).obj X) n ↔ ∃ (g : K.X p'' ⟶ X), CategoryTheory.CategoryStruct.comp (K.d p p'') g = f

Documentation

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Cochains from or to single complexes #