The cochain complex of homomorphisms between cochain complexes

If F and G are cochain complexes (indexed by ℤ) in a preadditive category, there is a cochain complex of abelian groups whose 0-cocycles identify to morphisms F ⟶ G. Informally, in degree n, this complex shall consist of cochains of degree n from F to G, i.e. arbitrary families for morphisms F.X p ⟶ G.X (p + n). This complex shall be denoted HomComplex F G.

In order to avoid type theoretic issues, a cochain of degree n : ℤ (i.e. a term of type of Cochain F G n) shall be defined here as the data of a morphism F.X p ⟶ G.X q for all triplets ⟨p, q, hpq⟩ where p and q are integers and hpq : p + n = q. If α : Cochain F G n, we shall define α.v p q hpq : F.X p ⟶ G.X q.

We follow the signs conventions appearing in the introduction of [Brian Conrad's book Grothendieck duality and base change][conrad2000].

TODO:

• Define the differential Cochain F G n ⟶ Cochain F G m, and develop the API.
• Identify morphisms of complexes to 0-cocycles.
• Identify homotopies to -1-cochains satisfying certain relations.
• Behaviour with respect to shifting the cochain complexes F and G.

References

• [Brian Conrad, Grothendieck duality and base change][conrad2000]

structure CochainComplex.HomComplex.Triplet (n : ℤ) : Type

• p : ℤ

  a first integer

• q : ℤ

  a second integer

• hpq : s.p + n = s.q

  the condition on the two integers

A term of type HomComplex.Triplet n consists of two integers p and q such that p + n = q. (This type is introduced so that the instance AddCommGroup (Cochain F G n) defined below can be found automatically.)

def CochainComplex.HomComplex.Cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) : Type v

A cochain of degree n : ℤ between to cochain complexes F and G consists of a family of morphisms F.X p ⟶ G.X q whenever p + n = q, i.e. for all triplets in HomComplex.Triplet n.

instance CochainComplex.HomComplex.instAddCommGroupCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) : AddCommGroup (CochainComplex.HomComplex.Cochain F G n)

def CochainComplex.HomComplex.Cochain.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (v : (p q : ℤ) → p + n = q → (HomologicalComplex.X F p ⟶ HomologicalComplex.X G q)) : CochainComplex.HomComplex.Cochain F G n

A practical constructor for cochains.

def CochainComplex.HomComplex.Cochain.v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (hpq : p + n = q) : HomologicalComplex.X F p ⟶ HomologicalComplex.X G q

The value of a cochain on a triplet ⟨p, q, hpq⟩.

@[simp]

theorem CochainComplex.HomComplex.Cochain.mk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (v : (p q : ℤ) → p + n = q → (HomologicalComplex.X F p ⟶ HomologicalComplex.X G q)) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (CochainComplex.HomComplex.Cochain.mk v).v p q hpq = v p q hpq

theorem CochainComplex.HomComplex.Cochain.congr_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} {z₁ : CochainComplex.HomComplex.Cochain F G n} {z₂ : CochainComplex.HomComplex.Cochain F G n} (h : z₁ = z₂) (p : ℤ) (q : ℤ) (hpq : p + n = q) : z₁.v p q hpq = z₂.v p q hpq

theorem CochainComplex.HomComplex.Cochain.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) (h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq) : z₁ = z₂

theorem CochainComplex.HomComplex.Cochain.ext₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain F G 0) (h : ∀ (p : ℤ), z₁.v p p (_ : p + 0 = p) = z₂.v p p (_ : p + 0 = p)) : z₁ = z₂

@[simp]

theorem CochainComplex.HomComplex.Cochain.zero_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (p : ℤ) (q : ℤ) (hpq : p + n = q) : 0.v p q hpq = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.add_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (z₁ + z₂).v p q hpq = z₁.v p q hpq + z₂.v p q hpq

@[simp]

theorem CochainComplex.HomComplex.Cochain.sub_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (z₁ - z₂).v p q hpq = z₁.v p q hpq - z₂.v p q hpq

@[simp]

theorem CochainComplex.HomComplex.Cochain.neg_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (-z).v p q hpq = -z.v p q hpq

@[simp]

theorem CochainComplex.HomComplex.Cochain.zsmul_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} {k : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (k • z).v p q hpq = k • z.v p q hpq

def CochainComplex.HomComplex.Cochain.ofHoms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (ψ : (p : ℤ) → HomologicalComplex.X F p ⟶ HomologicalComplex.X G p) : CochainComplex.HomComplex.Cochain F G 0

A cochain of degree 0 from F to G can be constructed from a family of morphisms F.X p ⟶ G.X p for all p : ℤ.

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHoms_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (ψ : (p : ℤ) → HomologicalComplex.X F p ⟶ HomologicalComplex.X G p) (p : ℤ) : (CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p (_ : p + 0 = p) = ψ p

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHoms_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} : (CochainComplex.HomComplex.Cochain.ofHoms fun p => 0) = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (ψ : (p : ℤ) → HomologicalComplex.X F p ⟶ HomologicalComplex.X G p) (p : ℤ) (q : ℤ) (q' : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) (HomologicalComplex.d G q q') = CategoryTheory.CategoryStruct.comp (ψ p) (HomologicalComplex.d G p q')

@[simp]

theorem CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (ψ : (p : ℤ) → HomologicalComplex.X F p ⟶ HomologicalComplex.X G p) (p' : ℤ) (p : ℤ) (q : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d F p' p) ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d F p' q) (ψ q)

def CochainComplex.HomComplex.Cochain.ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) : CochainComplex.HomComplex.Cochain F G 0

The 0-cochain attached to a morphism of cochain complexes.

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) : CochainComplex.HomComplex.Cochain.ofHom 0 = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) (p : ℤ) : (CochainComplex.HomComplex.Cochain.ofHom φ).v p p (_ : p + 0 = p) = HomologicalComplex.Hom.f φ p

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_v_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) (p : ℤ) (q : ℤ) (q' : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) (HomologicalComplex.d G q q') = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f φ p) (HomologicalComplex.d G p q')

@[simp]

theorem CochainComplex.HomComplex.Cochain.d_comp_ofHom_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) (p' : ℤ) (p : ℤ) (q : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d F p' p) ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d F p' q) (HomologicalComplex.Hom.f φ q)

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ₁ : F ⟶ G) (φ₂ : F ⟶ G) : CochainComplex.HomComplex.Cochain.ofHom (φ₁ + φ₂) = CochainComplex.HomComplex.Cochain.ofHom φ₁ + CochainComplex.HomComplex.Cochain.ofHom φ₂

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ₁ : F ⟶ G) (φ₂ : F ⟶ G) : CochainComplex.HomComplex.Cochain.ofHom (φ₁ - φ₂) = CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) : CochainComplex.HomComplex.Cochain.ofHom (-φ) = -CochainComplex.HomComplex.Cochain.ofHom φ

def CochainComplex.HomComplex.Cochain.ofHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {φ₁ : F ⟶ G} {φ₂ : F ⟶ G} (ho : Homotopy φ₁ φ₂) : CochainComplex.HomComplex.Cochain F G (-1)

The cochain of degree -1 given by an homotopy between two morphism of complexes.

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {φ₁ : F ⟶ G} {φ₂ : F ⟶ G} (h : φ₁ = φ₂) : CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.ofEq h) = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHomotopy_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) : CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.refl φ) = 0

theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (q' : ℤ) (hpq : p + n = q) (hq' : q = q') {Z : C} (h : HomologicalComplex.X G q' ⟶ Z) : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').hom h) = CategoryTheory.CategoryStruct.comp (γ.v p q' (_ : p + n = q')) h

theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (q' : ℤ) (hpq : p + n = q) (hq' : q = q') : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' (_ : p + n = q')

theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (q' : ℤ) (hpq : p + n = q) (hq' : q' = q) {Z : C} (h : HomologicalComplex.X G q' ⟶ Z) : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').inv h) = CategoryTheory.CategoryStruct.comp (γ.v p q' (_ : p + n = q')) h

theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (q' : ℤ) (hpq : p + n = q) (hq' : q' = q) : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' (_ : p + n = q')

def CochainComplex.HomComplex.Cochain.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : CochainComplex.HomComplex.Cochain F K n₁₂

The composition of cochains.

If z₁ is a cochain of degree n₁ and z₂ is a cochain of degree n₂, and that we have a relation h : n₁ + n₂ = n₁₂, then z₁.comp z₂ h is a cochain of degree n₁₂. The following lemma comp_v computes the value of this composition z₁.comp z₂ h on a triplet ⟨p₁, p₃, _⟩ (with p₁ + n₁₂ = p₃). In order to use this lemma, we need to provide an intermediate integer p₂ such that p₁ + n₁ = p₂. It is advisable to use a p₂ that has good definitional properties (i.e. p₁ + n₁ is not always the best choice.)

When z₁ or z₂ is a 0-cochain, there is a better choice of p₂, and this leads to the two simplification lemmas comp_zero_cochain_v and zero_cochain_comp_v.

theorem CochainComplex.HomComplex.Cochain.comp_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (p₁ : ℤ) (p₂ : ℤ) (p₃ : ℤ) (h₁ : p₁ + n₁ = p₂) (h₂ : p₂ + n₂ = p₃) : (z₁.comp z₂ h).v p₁ p₃ (_ : p₁ + n₁₂ = p₃) = CategoryTheory.CategoryStruct.comp (z₁.v p₁ p₂ h₁) (z₂.v p₂ p₃ h₂)

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_zero_cochain_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (z₁.comp z₂ (_ : n + 0 = n)).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q (_ : q + 0 = q))

@[simp]

theorem CochainComplex.HomComplex.Cochain.zero_cochain_comp_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n) (p : ℤ) (q : ℤ) (hpq : p + n = q) : (z₁.comp z₂ (_ : 0 + n = n)).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p p (_ : p + 0 = p)) (z₂.v p q hpq)

theorem CochainComplex.HomComplex.Cochain.comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₃ : ℤ} {n₁₂ : ℤ} {n₂₃ : ℤ} {n₁₂₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₁₂ : n₁ + n₂ = n₁₂) (h₂₃ : n₂ + n₃ = n₂₃) (h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃) : (z₁.comp z₂ h₁₂).comp z₃ (_ : n₁₂ + n₃ = n₁₂₃) = z₁.comp (z₂.comp z₃ h₂₃) (_ : n₁ + n₂₃ = n₁₂₃)

The associativity of the composition of cochains.

The formulation of the associativity of the composition of cochains given by the lemma comp_assoc often requires a careful selection of degrees with good definitional properties. In a few cases, like when one of the three cochains is a 0-cochain, there are better choices, which provides the following simplification lemmas.

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n₂ : ℤ} {n₃ : ℤ} {n₂₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₂₃ : n₂ + n₃ = n₂₃) : (z₁.comp z₂ (_ : 0 + n₂ = n₂)).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃) (_ : 0 + n₂₃ = n₂₃)

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n₁ : ℤ} {n₃ : ℤ} {n₁₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₁₃ : n₁ + n₃ = n₁₃) : (z₁.comp z₂ (_ : n₁ + 0 = n₁)).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ (_ : 0 + n₃ = n₃)) h₁₃

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_third_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L 0) (h₁₂ : n₁ + n₂ = n₁₂) : (z₁.comp z₂ h₁₂).comp z₃ (_ : n₁₂ + 0 = n₁₂) = z₁.comp (z₂.comp z₃ (_ : n₂ + 0 = n₂)) h₁₂

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_second_degree_eq_neg_third_degree {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K (-n₂)) (z₃ : CochainComplex.HomComplex.Cochain K L n₂) (h₁₂ : n₁ + -n₂ = n₁₂) : (z₁.comp z₂ h₁₂).comp z₃ (_ : n₁₂ + n₂ = n₁) = z₁.comp (z₂.comp z₃ (_ : -n₂ + n₂ = 0)) (_ : n₁ + 0 = n₁)

@[simp]

theorem CochainComplex.HomComplex.Cochain.zero_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : 0.comp z₂ h = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.add_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₁' : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h

@[simp]

theorem CochainComplex.HomComplex.Cochain.sub_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₁' : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h

@[simp]

theorem CochainComplex.HomComplex.Cochain.neg_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : (-z₁).comp z₂ h = -z₁.comp z₂ h

@[simp]

theorem CochainComplex.HomComplex.Cochain.zsmul_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (k : ℤ) (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : (k • z₁).comp z₂ h = k • z₁.comp z₂ h

@[simp]

theorem CochainComplex.HomComplex.Cochain.id_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₂ : CochainComplex.HomComplex.Cochain F G n) : (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)).comp z₂ (_ : 0 + n = n) = z₂

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (h : n₁ + n₂ = n₁₂) : z₁.comp 0 h = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : z₁.comp (-z₂) h = -z₁.comp z₂ h

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_zsmul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (k : ℤ) (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : z₁.comp (k • z₂) h = k • z₁.comp z₂ h

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) : z₁.comp (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)) (_ : n + 0 = n) = z₁

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHoms_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} (φ : (p : ℤ) → HomologicalComplex.X F p ⟶ HomologicalComplex.X G p) (ψ : (p : ℤ) → HomologicalComplex.X G p ⟶ HomologicalComplex.X K p) : (CochainComplex.HomComplex.Cochain.ofHoms φ).comp (CochainComplex.HomComplex.Cochain.ofHoms ψ) (_ : 0 + 0 = 0) = CochainComplex.HomComplex.Cochain.ofHoms fun p => CategoryTheory.CategoryStruct.comp (φ p) (ψ p)

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} (f : F ⟶ G) (g : G ⟶ K) : CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp f g) = (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.Cochain.ofHom g) (_ : 0 + 0 = 0)

def CochainComplex.HomComplex.Cochain.diff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : CochainComplex.HomComplex.Cochain K K 1

The differential on a cochain complex, as a cochain of degree 1.

@[simp]

theorem CochainComplex.HomComplex.Cochain.diff_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (p : ℤ) (q : ℤ) (hpq : p + 1 = q) : (CochainComplex.HomComplex.Cochain.diff K).v p q hpq = HomologicalComplex.d K p q

def CochainComplex.HomComplex.δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.Cochain F G m

The differential on the complex of morphisms between cochain complexes.

Similarly as for the composition of cochains, if z : Cochain F G n, we usually need to carefully select intermediate indices with good definitional properties in order to obtain a suitable expansion of the morphisms which constitute δ n m z : Cochain F G m (when n + 1 = m, otherwise it shall be zero). The basic equational lemma is δ_v below.

theorem CochainComplex.HomComplex.δ_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) (p : ℤ) (q : ℤ) (hpq : p + m = q) (q₁ : ℤ) (q₂ : ℤ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂) : (CochainComplex.HomComplex.δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ (_ : p + n = q₁)) (HomologicalComplex.d G q₁ q) + (n + 1).negOnePow • CategoryTheory.CategoryStruct.comp (HomologicalComplex.d F p q₂) (z.v q₂ q (_ : q₂ + n = q))

theorem CochainComplex.HomComplex.δ_shape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (hnm : ¬n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.δ n m z = 0

@[simp]

theorem CochainComplex.HomComplex.δ_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) (m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) : ↑(CochainComplex.HomComplex.δ_hom F G n m) z = CochainComplex.HomComplex.δ n m z

def CochainComplex.HomComplex.δ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) (m : ℤ) : CochainComplex.HomComplex.Cochain F G n →+ CochainComplex.HomComplex.Cochain F G m

The differential on the complex of morphisms between cochain complexes, as an additive homomorphism.

@[simp]

theorem CochainComplex.HomComplex.δ_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.δ n m (z₁ + z₂) = CochainComplex.HomComplex.δ n m z₁ + CochainComplex.HomComplex.δ n m z₂

@[simp]

theorem CochainComplex.HomComplex.δ_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.δ n m (z₁ - z₂) = CochainComplex.HomComplex.δ n m z₁ - CochainComplex.HomComplex.δ n m z₂

@[simp]

theorem CochainComplex.HomComplex.δ_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) : CochainComplex.HomComplex.δ n m 0 = 0

@[simp]

theorem CochainComplex.HomComplex.δ_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.δ n m (-z) = -CochainComplex.HomComplex.δ n m z

@[simp]

theorem CochainComplex.HomComplex.δ_zsmul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (k : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z

theorem CochainComplex.HomComplex.δ_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n₀ : ℤ) (n₁ : ℤ) (n₂ : ℤ) (z : CochainComplex.HomComplex.Cochain F G n₀) : CochainComplex.HomComplex.δ n₁ n₂ (CochainComplex.HomComplex.δ n₀ n₁ z) = 0

theorem CochainComplex.HomComplex.δ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} {n₂ : ℤ} {n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (m₁ : ℤ) (m₂ : ℤ) (m₁₂ : ℤ) (h₁₂ : n₁₂ + 1 = m₁₂) (h₁ : n₁ + 1 = m₁) (h₂ : n₂ + 1 = m₂) : CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) (_ : n₁ + m₂ = m₁₂) + n₂.negOnePow • (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ (_ : m₁ + n₂ = m₁₂)

theorem CochainComplex.HomComplex.δ_zero_cochain_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (m₂ : ℤ) (h₂ : n₂ + 1 = m₂) : CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ (_ : 0 + n₂ = n₂)) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) (_ : 0 + m₂ = m₂) + n₂.negOnePow • (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂ (_ : 1 + n₂ = m₂)

theorem CochainComplex.HomComplex.δ_comp_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {K : CochainComplex C ℤ} {n₁ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (m₁ : ℤ) (h₁ : n₁ + 1 = m₁) : CochainComplex.HomComplex.δ n₁ m₁ (z₁.comp z₂ (_ : n₁ + 0 = n₁)) = z₁.comp (CochainComplex.HomComplex.δ 0 1 z₂) h₁ + (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ (_ : m₁ + 0 = m₁)

@[simp]

theorem CochainComplex.HomComplex.δ_zero_cochain_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G 0) (p : ℤ) (q : ℤ) (hpq : p + 1 = q) : (CochainComplex.HomComplex.δ 0 1 z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p p (_ : p + 0 = p)) (HomologicalComplex.d G p q) - CategoryTheory.CategoryStruct.comp (HomologicalComplex.d F p q) (z.v q q (_ : q + 0 = q))

@[simp]

theorem CochainComplex.HomComplex.δ_ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {p : ℤ} (φ : F ⟶ G) : CochainComplex.HomComplex.δ 0 p (CochainComplex.HomComplex.Cochain.ofHom φ) = 0

@[simp]

theorem CochainComplex.HomComplex.δ_ofHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {φ₁ : F ⟶ G} {φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) : CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.HomComplex.Cochain.ofHomotopy h) = CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂

theorem CochainComplex.HomComplex.δ_neg_one_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G (-1)) : CochainComplex.HomComplex.δ (-1) 0 z = CochainComplex.HomComplex.Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij => z.v i j (_ : i + -1 = j))

@[simp]

theorem CochainComplex.HomComplex_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (i : ℤ) : HomologicalComplex.X (CochainComplex.HomComplex F G) i = AddCommGroupCat.of (CochainComplex.HomComplex.Cochain F G i)

@[simp]

theorem CochainComplex.HomComplex_d_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (i : ℤ) (j : ℤ) (z : CochainComplex.HomComplex.Cochain F G i) : ↑(HomologicalComplex.d (CochainComplex.HomComplex F G) i j) z = CochainComplex.HomComplex.δ i j z

def CochainComplex.HomComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) : CochainComplex AddCommGroupCat ℤ

The cochain complex of homomorphisms between two cochain complexes F and G. In degree n : ℤ, it consists of the abelian group HomComplex.Cochain F G n.

def CochainComplex.HomComplex.cocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) : AddSubgroup (CochainComplex.HomComplex.Cochain F G n)

The subgroup of cocycles in Cochain F G n.

def CochainComplex.HomComplex.Cocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) : Type v

The type of n-cocycles, as a subtype of Cochain F G n.

instance CochainComplex.HomComplex.instAddCommGroupCocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) : AddCommGroup (CochainComplex.HomComplex.Cocycle F G n)

instance CochainComplex.HomComplex.Cocycle.instCoeCocycleCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} : Coe (CochainComplex.HomComplex.Cocycle F G n) (CochainComplex.HomComplex.Cochain F G n)

theorem CochainComplex.HomComplex.Cocycle.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cocycle F G n) (z₂ : CochainComplex.HomComplex.Cocycle F G n) (h : ↑z₁ = ↑z₂) : z₁ = z₂

theorem CochainComplex.HomComplex.Cocycle.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cocycle F G n) (z₂ : CochainComplex.HomComplex.Cocycle F G n) : z₁ = z₂ ↔ ↑z₁ = ↑z₂

@[simp]

theorem CochainComplex.HomComplex.Cocycle.coe_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (n : ℤ) : ↑0 = 0

@[simp]

theorem CochainComplex.HomComplex.Cocycle.coe_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cocycle F G n) (z₂ : CochainComplex.HomComplex.Cocycle F G n) : ↑(z₁ + z₂) = ↑z₁ + ↑z₂

@[simp]

theorem CochainComplex.HomComplex.Cocycle.coe_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) : ↑(-z) = -↑z

@[simp]

theorem CochainComplex.HomComplex.Cocycle.coe_zsmul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (x : ℤ) : ↑(x • z) = x • ↑z

@[simp]

theorem CochainComplex.HomComplex.Cocycle.coe_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cocycle F G n) (z₂ : CochainComplex.HomComplex.Cocycle F G n) : ↑(z₁ - z₂) = ↑z₁ - ↑z₂

theorem CochainComplex.HomComplex.Cocycle.mem_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (n : ℤ) (m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) : z ∈ CochainComplex.HomComplex.cocycle F G n ↔ CochainComplex.HomComplex.δ n m z = 0

@[simp]

theorem CochainComplex.HomComplex.Cocycle.mk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (m : ℤ) (hnm : n + 1 = m) (h : CochainComplex.HomComplex.δ n m z = 0) : ↑(CochainComplex.HomComplex.Cocycle.mk z m hnm h) = z

def CochainComplex.HomComplex.Cocycle.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (m : ℤ) (hnm : n + 1 = m) (h : CochainComplex.HomComplex.δ n m z = 0) : CochainComplex.HomComplex.Cocycle F G n

Constructor for Cocycle F G n, taking as inputs z : Cochain F G n, an integer m : ℤ such that n + 1 = m, and the relation δ n m z = 0.

@[simp]

theorem CochainComplex.HomComplex.Cocycle.δ_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (m : ℤ) : CochainComplex.HomComplex.δ n m ↑z = 0

@[simp]

theorem CochainComplex.HomComplex.Cocycle.ofHom_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) : ↑(CochainComplex.HomComplex.Cocycle.ofHom φ) = CochainComplex.HomComplex.Cochain.ofHom φ

def CochainComplex.HomComplex.Cocycle.ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) : CochainComplex.HomComplex.Cocycle F G 0

The 0-cocycle associated to a morphism in CochainComplex C ℤ.

@[simp]

theorem CochainComplex.HomComplex.Cocycle.homOf_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) (i : ℤ) : HomologicalComplex.Hom.f (CochainComplex.HomComplex.Cocycle.homOf z) i = (↑z).v i i (_ : i + 0 = i)

def CochainComplex.HomComplex.Cocycle.homOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) : F ⟶ G

The morphism in CochainComplex C ℤ associated to a 0-cocycle.

@[simp]

theorem CochainComplex.HomComplex.Cocycle.homOf_ofHom_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (φ : F ⟶ G) : CochainComplex.HomComplex.Cocycle.homOf (CochainComplex.HomComplex.Cocycle.ofHom φ) = φ

@[simp]

theorem CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) : CochainComplex.HomComplex.Cocycle.ofHom (CochainComplex.HomComplex.Cocycle.homOf z) = z

@[simp]

theorem CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C ℤ} {G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) : CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.HomComplex.Cocycle.homOf z) = ↑z

@[simp]

theorem CochainComplex.HomComplex.Cocycle.equivHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (φ : F ⟶ G) : ↑(CochainComplex.HomComplex.Cocycle.equivHom F G) φ = CochainComplex.HomComplex.Cocycle.ofHom φ

@[simp]

theorem CochainComplex.HomComplex.Cocycle.equivHom_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) (z : CochainComplex.HomComplex.Cocycle F G 0) : ↑(AddEquiv.symm (CochainComplex.HomComplex.Cocycle.equivHom F G)) z = CochainComplex.HomComplex.Cocycle.homOf z

def CochainComplex.HomComplex.Cocycle.equivHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) (G : CochainComplex C ℤ) : (F ⟶ G) ≃+ CochainComplex.HomComplex.Cocycle F G 0

The additive equivalence between morphisms in CochainComplex C ℤ and 0-cocycles.

@[simp]

theorem CochainComplex.HomComplex.Cocycle.diff_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : ↑(CochainComplex.HomComplex.Cocycle.diff K) = CochainComplex.HomComplex.Cochain.diff K

def CochainComplex.HomComplex.Cocycle.diff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : CochainComplex.HomComplex.Cocycle K K 1

The 1-cocycle given by the differential on a cochain complex.