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.

References

• Brian Conrad, Grothendieck duality and base change

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

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

• p : ℤ

  a first integer

• q : ℤ

  a second integer

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

  the condition on the two integers

def CochainComplex.HomComplex.Cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F 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.

Equations

• CochainComplex.HomComplex.Cochain F G n = ((T : CochainComplex.HomComplex.Triplet n) → F.X T.p ⟶ G.X T.q)

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

Equations

• CochainComplex.HomComplex.instAddCommGroupCochain F G n = id inferInstance

instance CochainComplex.HomComplex.instModuleCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n : ℤ) : Module R (Cochain F G n)

Equations

• CochainComplex.HomComplex.instModuleCochain F G n = id inferInstance

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

A practical constructor for cochains.

Equations

• CochainComplex.HomComplex.Cochain.mk v { p := p, q := q, hpq := hpq } = v p q hpq

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

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

Equations

• γ.v p q hpq = γ { p := p, q := q, hpq := hpq }

@[simp]

theorem CochainComplex.HomComplex.Cochain.mk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)) (p q : ℤ) (hpq : p + n = q) : (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 G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : 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_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : Cochain F G n} : 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 G : CochainComplex C ℤ} (z₁ z₂ : Cochain F G 0) (h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯) : z₁ = z₂

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

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.add_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} (z : 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.smul_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (k : R) (z : Cochain F G n) (p q : ℤ) (hpq : p + n = q) : (k • z).v p q hpq = k • z.v p q hpq

@[simp]

theorem CochainComplex.HomComplex.Cochain.units_smul_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (k : Rˣ) (z : 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 G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) : 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 : ℤ.

Equations

• CochainComplex.HomComplex.Cochain.ofHoms ψ = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + 0 = q) => CategoryTheory.CategoryStruct.comp (ψ p) (CategoryTheory.eqToHom ⋯)

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHoms_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} : (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 G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p q q' : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp ((ofHoms ψ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (ψ p) (G.d p q')

@[simp]

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

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

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

Equations

• CochainComplex.HomComplex.Cochain.ofHom φ = CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => φ.f p

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CochainComplex.HomComplex.Cochain.ofHomotopy ho = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (x : p + -1 = q) => ho.hom p q

@[simp]

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

@[simp]

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

theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : 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' ⋯

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

theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : 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' ⋯

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

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

The composition of cochains.

Equations

• z₁.comp z₂ h = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + n₁₂ = q) => CategoryTheory.CategoryStruct.comp (z₁.v p (p + n₁) ⋯) (z₂.v (p + n₁) q ⋯)

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 G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : 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₃ ⋯ = 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 G K : CochainComplex C ℤ} {n : ℤ} (z₁ : Cochain F G n) (z₂ : Cochain G K 0) (p q : ℤ) (hpq : p + n = q) : (z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q ⋯)

@[simp]

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

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

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 G K L : CochainComplex C ℤ} {n₂ n₃ n₂₃ : ℤ} (z₁ : Cochain F G 0) (z₂ : Cochain G K n₂) (z₃ : Cochain K L n₃) (h₂₃ : n₂ + n₃ = n₂₃) : (z₁.comp z₂ ⋯).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃) ⋯

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K L : CochainComplex C ℤ} {n₁ n₃ n₁₃ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K 0) (z₃ : Cochain K L n₃) (h₁₃ : n₁ + n₃ = n₁₃) : (z₁.comp z₂ ⋯).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ ⋯) 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 G K L : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (z₃ : Cochain K L 0) (h₁₂ : n₁ + n₂ = n₁₂) : (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) 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 G K L : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K (-n₂)) (z₃ : Cochain K L n₂) (h₁₂ : n₁ + -n₂ = n₁₂) : (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.units_smul_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (k : Rˣ) (z₁ : Cochain F G n₁) (z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} (z₂ : Cochain F G n) : (ofHom (CategoryTheory.CategoryStruct.id F)).comp z₂ ⋯ = z₂

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : 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 G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ z₂' : 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 G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ z₂' : 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 G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : z₁.comp (-z₂) h = -z₁.comp z₂ h

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.comp_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (k : Rˣ) (z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} (z₁ : Cochain F G n) : z₁.comp (ofHom (CategoryTheory.CategoryStruct.id G)) ⋯ = z₁

@[simp]

theorem CochainComplex.HomComplex.Cochain.ofHoms_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} (φ : (p : ℤ) → F.X p ⟶ G.X p) (ψ : (p : ℤ) → G.X p ⟶ K.X p) : (ofHoms φ).comp (ofHoms ψ) ⋯ = 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 G K : CochainComplex C ℤ} (f : F ⟶ G) (g : G ⟶ K) : ofHom (CategoryTheory.CategoryStruct.comp f g) = (ofHom f).comp (ofHom g) ⋯

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

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

Equations

• CochainComplex.HomComplex.Cochain.diff K = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) => K.d p q

@[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) : (diff K).v p q hpq = K.d p q

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

The differential on the complex of morphisms between cochain complexes.

Equations

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

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 G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : Cochain F G n) (p q : ℤ) (hpq : p + m = q) (q₁ q₂ : ℤ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂) : (δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ ⋯) (G.d q₁ q) + m.negOnePow • CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q ⋯)

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

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

The differential on the complex of morphisms between cochain complexes, as a linear map.

Equations

• CochainComplex.HomComplex.δ_hom R F G n m = { toFun := CochainComplex.HomComplex.δ n m, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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.

Equations

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

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex_d_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (i j : ℤ) (a✝ : HomComplex.Cochain F G i) : (AddCommGrp.Hom.hom ((F.HomComplex G).d i j)) a✝ = HomComplex.δ i j a✝

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

The subgroup of cocycles in Cochain F G n.

Equations

• CochainComplex.HomComplex.cocycle F G n = (CochainComplex.HomComplex.δ_hom ℤ F G n (n + 1)).toAddMonoidHom.ker

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

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

Equations

• CochainComplex.HomComplex.Cocycle F G n = ↥(CochainComplex.HomComplex.cocycle F G n)

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

Equations

• CochainComplex.HomComplex.instAddCommGroupCocycle F G n = id inferInstance

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

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

Equations

• CochainComplex.HomComplex.Cocycle.instCoeCochain = { coe := fun (x : CochainComplex.HomComplex.Cocycle F G n) => ↑x }

theorem CochainComplex.HomComplex.Cocycle.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : Cocycle F G n} : z₁ = z₂ ↔ ↑z₁ = ↑z₂

instance CochainComplex.HomComplex.Cocycle.instSMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} : SMul R (Cocycle F G n)

Equations

• CochainComplex.HomComplex.Cocycle.instSMul = { smul := fun (r : R) (z : CochainComplex.HomComplex.Cocycle F G n) => ⟨r • ↑z, ⋯⟩ }

@[simp]

theorem CochainComplex.HomComplex.Cocycle.coe_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F 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 G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : 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 G : CochainComplex C ℤ} {n : ℤ} (z : Cocycle F G n) : ↑(-z) = -↑z

@[simp]

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

@[simp]

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

@[simp]

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

instance CochainComplex.HomComplex.Cocycle.instModule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} : Module R (Cocycle F G n)

Equations

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

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

Equations

• CochainComplex.HomComplex.Cocycle.mk z m hnm h = ⟨z, ⋯⟩

@[simp]

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

@[simp]

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

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

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

Equations

• CochainComplex.HomComplex.Cocycle.ofHom φ = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.ofHom φ) 1 CochainComplex.HomComplex.Cocycle.ofHom._proof_21 ⋯

@[simp]

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

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

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

Equations

• z.homOf = { f := fun (i : ℤ) => (↑z).v i i ⋯, comm' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• CochainComplex.HomComplex.Cocycle.diff K = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.diff K) 2 CochainComplex.HomComplex.Cocycle.diff._proof_27 ⋯

@[simp]

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

@[simp]

theorem CochainComplex.HomComplex.δ_comp_zero_cocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : Cochain F G n) (z₂ : Cocycle G K 0) (m : ℤ) : δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

@[simp]

theorem CochainComplex.HomComplex.δ_comp_ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : Cochain F G n) (f : G ⟶ K) (m : ℤ) : δ n m (z₁.comp (Cochain.ofHom f) ⋯) = (δ n m z₁).comp (Cochain.ofHom f) ⋯

@[simp]

theorem CochainComplex.HomComplex.δ_zero_cocycle_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : Cocycle F G 0) (z₂ : Cochain G K n) (m : ℤ) : δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

@[simp]

theorem CochainComplex.HomComplex.δ_ofHom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (f : F ⟶ G) (z : Cochain G K n) (m : ℤ) : δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯

def CochainComplex.HomComplex.Cochain.equivHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) : Homotopy φ₁ φ₂ ≃ { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }

Given two morphisms of complexes φ₁ φ₂ : F ⟶ G, the datum of an homotopy between φ₁ and φ₂ is equivalent to the datum of a 1-cochain z such that δ (-1) 0 z is the difference of the zero cochains associated to φ₂ and φ₁.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) (ho : Homotopy φ₁ φ₂) : ↑((equivHomotopy φ₁ φ₂) ho) = ofHomotopy ho

@[simp]

theorem CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) (i j : ℤ) : ((equivHomotopy φ₁ φ₂).symm z).hom i j = if hij : i + -1 = j then (↑z).v i j hij else 0

@[simp]

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

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

def CochainComplex.HomComplex.Cochain.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z : Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : Cochain ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) n

If Φ : C ⥤ D is an additive functor, a cochain z : Cochain K L n between cochain complexes in C can be mapped to a cochain between the cochain complexes in D obtained by applying the functor Φ.mapHomologicalComplex _ : CochainComplex C ℤ ⥤ CochainComplex D ℤ.

Equations

• z.map Φ = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + n = q) => Φ.map (z.v p q hpq)

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z : Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] (p q : ℤ) (hpq : p + n = q) : (z.map Φ).v p q hpq = Φ.map (z.v p q hpq)

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z z' : Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : (z + z').map Φ = z.map Φ + z'.map Φ

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z : Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : (-z).map Φ = -z.map Φ

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z z' : Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : (z - z').map Φ = z.map Φ - z'.map Φ

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (Φ : CategoryTheory.Functor C D) [Φ.Additive] : map 0 Φ = 0

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (K : CochainComplex C ℤ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : (z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h

@[simp]

theorem CochainComplex.HomComplex.Cochain.map_ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (f : K ⟶ L) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : (ofHom f).map Φ = ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)

@[simp]

theorem CochainComplex.HomComplex.δ_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (n m : ℤ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z : Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] : δ n m (z.map Φ) = (δ n m z).map Φ