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.

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

theorem CochainComplex.HomComplex.Cochain.fromSingleEquiv_symm_apply {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) (f : X ⟶ K.X q) : (fromSingleEquiv h).symm f = fromSingleMk f h

theorem CochainComplex.HomComplex.Cochain.fromSingleEquiv_apply {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) : (fromSingleEquiv h) α = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv (α.v p q h)

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_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) (f : Cochain ((singleFunctor C p).obj X) K n) : fromSingleMk ((fromSingleEquiv h) f) h = f

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

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

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleEquiv_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (r : R) {p q n : ℤ} (h : p + n = q) (f : Cochain ((singleFunctor C p).obj X) K n) : (fromSingleEquiv h) (r • f) = r • (fromSingleEquiv h) f

theorem CochainComplex.HomComplex.Cochain.fromSingleMk_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (r : R) {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) : fromSingleMk (r • f) h = r • fromSingleMk f h

noncomputable def CochainComplex.HomComplex.Cochain.fromSingleLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {p q n : ℤ} (h : p + n = q) : Cochain ((singleFunctor C p).obj X) K n ≃ₗ[R] 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.

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {p q n : ℤ} (h : p + n = q) (a✝ : X ⟶ K.X q) : (fromSingleLinearEquiv h).symm a✝ = (fromSingleEquiv h).invFun a✝

@[simp]

theorem CochainComplex.HomComplex.Cochain.fromSingleLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {p q n : ℤ} (h : p + n = q) (a✝ : Cochain ((singleFunctor C p).obj X) K n) : (fromSingleLinearEquiv h) a✝ = (fromSingleEquiv h).toFun a✝

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 = α

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

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

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

theorem CochainComplex.HomComplex.Cochain.toSingleEquiv_symm_apply {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) (f : K.X p ⟶ X) : (toSingleEquiv h).symm f = toSingleMk f h

theorem CochainComplex.HomComplex.Cochain.toSingleEquiv_apply {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) : (toSingleEquiv h) α = CategoryTheory.CategoryStruct.comp (α.v p q h) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleMk_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) (f : Cochain K ((singleFunctor C q).obj X) n) : toSingleMk ((toSingleEquiv h) f) h = f

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

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

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleEquiv_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (r : R) {p q n : ℤ} (h : p + n = q) (f : Cochain K ((singleFunctor C q).obj X) n) : (toSingleEquiv h) (r • f) = r • (toSingleEquiv h) f

theorem CochainComplex.HomComplex.Cochain.toSingleMk_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (r : R) {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) : toSingleMk (r • f) h = r • toSingleMk f h

noncomputable def CochainComplex.HomComplex.Cochain.toSingleLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {p q n : ℤ} (h : p + n = q) : Cochain K ((singleFunctor C q).obj X) n ≃ₗ[R] 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.

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {p q n : ℤ} (h : p + n = q) (a✝ : Cochain K ((singleFunctor C q).obj X) n) : (toSingleLinearEquiv h) a✝ = (toSingleEquiv h).toFun a✝

@[simp]

theorem CochainComplex.HomComplex.Cochain.toSingleLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {p q n : ℤ} (h : p + n = q) (a✝ : K.X p ⟶ X) : (toSingleLinearEquiv h).symm a✝ = (toSingleEquiv h).invFun a✝

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 = α

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

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

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

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)

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

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 = α

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

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

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

theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (r : R) {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 (r • f) h q' hq' ⋯ = r • fromSingleMk f h q' hq' hf

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

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

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

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)

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

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 = α

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

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

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

theorem CochainComplex.HomComplex.Cocycle.toSingleMk_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (r : R) {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 (r • f) h p' hp' ⋯ = r • toSingleMk f h p' hp' hf

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

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