# Documentation

## Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

## References #

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

Instances For
theorem CochainComplex.HomComplex.Triplet.hpq {n : } (self : ) :
self.p + n = self.q

the condition on the two integers

def CochainComplex.HomComplex.Cochain {C : Type u} (F : ) (G : ) (n : ) :

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
• = ((T : ) → F.X T.p G.X T.q)
Instances For
instance CochainComplex.HomComplex.instAddCommGroupCochain {C : Type u} (F : ) (G : ) (n : ) :
Equations
• = id inferInstance
instance CochainComplex.HomComplex.instModuleCochain {C : Type u} {R : Type u_1} [Ring R] [] (F : ) (G : ) (n : ) :
Equations
• = id inferInstance
def CochainComplex.HomComplex.Cochain.mk {C : Type u} {F : } {G : } {n : } (v : (p q : ) → p + n = q(F.X p G.X q)) :

A practical constructor for cochains.

Equations
• = match x with | { p := p, q := q, hpq := hpq } => v p q hpq
Instances For
def CochainComplex.HomComplex.Cochain.v {C : Type u} {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 }
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.mk_v {C : Type u} {F : } {G : } {n : } (v : (p q : ) → p + n = q(F.X p G.X q)) (p : ) (q : ) (hpq : p + n = q) :
p q hpq = v p q hpq
theorem CochainComplex.HomComplex.Cochain.congr_v {C : Type u} {F : } {G : } {n : } {z₁ : } {z₂ : } (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} {F : } {G : } {n : } (z₁ : ) (z₂ : ) (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} {F : } {G : } (z₁ : ) (z₂ : ) (h : ∀ (p : ), z₁.v p p = z₂.v p p ) :
z₁ = z₂
@[simp]
theorem CochainComplex.HomComplex.Cochain.zero_v {C : Type u} {F : } {G : } {n : } (p : ) (q : ) (hpq : p + n = q) :
= 0
@[simp]
theorem CochainComplex.HomComplex.Cochain.add_v {C : Type u} {F : } {G : } {n : } (z₁ : ) (z₂ : ) (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} {F : } {G : } {n : } (z₁ : ) (z₂ : ) (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} {F : } {G : } {n : } (z : ) (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} {R : Type u_1} [Ring R] [] {F : } {G : } {n : } (k : R) (z : ) (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} {R : Type u_1} [Ring R] [] {F : } {G : } {n : } (k : Rˣ) (z : ) (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} {F : } {G : } (ψ : (p : ) → F.X p G.X p) :

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
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHoms_v {C : Type u} {F : } {G : } (ψ : (p : ) → F.X p G.X p) (p : ) :
= ψ p
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d {C : Type u} {F : } {G : } (ψ : (p : ) → F.X p G.X p) (p : ) (q : ) (q' : ) (hpq : p + 0 = q) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v {C : Type u} {F : } {G : } (ψ : (p : ) → F.X p G.X p) (p' : ) (p : ) (q : ) (hpq : p + 0 = q) :
def CochainComplex.HomComplex.Cochain.ofHom {C : Type u} {F : } {G : } (φ : F G) :

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

Equations
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_zero {C : Type u} (F : ) (G : ) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_v {C : Type u} {F : } {G : } (φ : F G) (p : ) :
= φ.f p
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_v_comp_d {C : Type u} {F : } {G : } (φ : F G) (p : ) (q : ) (q' : ) (hpq : p + 0 = q) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.d_comp_ofHom_v {C : Type u} {F : } {G : } (φ : F G) (p' : ) (p : ) (q : ) (hpq : p + 0 = q) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_add {C : Type u} {F : } {G : } (φ₁ : F G) (φ₂ : F G) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_sub {C : Type u} {F : } {G : } (φ₁ : F G) (φ₂ : F G) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_neg {C : Type u} {F : } {G : } (φ : F G) :
def CochainComplex.HomComplex.Cochain.ofHomotopy {C : Type u} {F : } {G : } {φ₁ : F G} {φ₂ : F G} (ho : Homotopy φ₁ φ₂) :

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

Equations
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq {C : Type u} {F : } {G : } {φ₁ : F G} {φ₂ : F G} (h : φ₁ = φ₂) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHomotopy_refl {C : Type u} {F : } {G : } (φ : F G) :
theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc {C : Type u} {F : } {G : } {n : } (γ : ) (p : ) (q : ) (q' : ) (hpq : p + n = q) (hq' : q = q') {Z : C} (h : G.X q' Z) :
theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom {C : Type u} {F : } {G : } {n : } (γ : ) (p : ) (q : ) (q' : ) (hpq : p + n = q) (hq' : q = q') :
CategoryTheory.CategoryStruct.comp (γ.v p q hpq) ().hom = γ.v p q'
theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc {C : Type u} {F : } {G : } {n : } (γ : ) (p : ) (q : ) (q' : ) (hpq : p + n = q) (hq' : q' = q) {Z : C} (h : G.X q' Z) :
theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv {C : Type u} {F : } {G : } {n : } (γ : ) (p : ) (q : ) (q' : ) (hpq : p + n = q) (hq' : q' = q) :
CategoryTheory.CategoryStruct.comp (γ.v p q hpq) ().inv = γ.v p q'
def CochainComplex.HomComplex.Cochain.comp {C : Type u} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (h : n₁ + n₂ = n₁₂) :

The composition of cochains.

Equations
Instances For

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} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (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} {F : } {G : } {K : } {n : } (z₁ : ) (z₂ : ) (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} {F : } {G : } {K : } {n : } (z₁ : ) (z₂ : ) (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} {F : } {G : } {K : } {L : } {n₁ : } {n₂ : } {n₃ : } {n₁₂ : } {n₂₃ : } {n₁₂₃ : } (z₁ : ) (z₂ : ) (z₃ : ) (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} {F : } {G : } {K : } {L : } {n₂ : } {n₃ : } {n₂₃ : } (z₁ : ) (z₂ : ) (z₃ : ) (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} {F : } {G : } {K : } {L : } {n₁ : } {n₃ : } {n₁₃ : } (z₁ : ) (z₂ : ) (z₃ : ) (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} {F : } {G : } {K : } {L : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (z₃ : ) (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} {F : } {G : } {K : } {L : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (z₃ : ) (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} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₂ : ) (h : n₁ + n₂ = n₁₂) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.add_comp {C : Type u} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₁' : ) (z₂ : ) (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} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₁' : ) (z₂ : ) (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} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (h : n₁ + n₂ = n₁₂) :
(-z₁).comp z₂ h = -z₁.comp z₂ h
@[simp]
theorem CochainComplex.HomComplex.Cochain.smul_comp {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (k : R) (z₁ : ) (z₂ : ) (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} {R : Type u_1} [Ring R] [] {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (k : Rˣ) (z₁ : ) (z₂ : ) (h : n₁ + n₂ = n₁₂) :
(k z₁).comp z₂ h = k z₁.comp z₂ h
@[simp]
theorem CochainComplex.HomComplex.Cochain.id_comp {C : Type u} {F : } {G : } {n : } (z₂ : ) :
= z₂
@[simp]
theorem CochainComplex.HomComplex.Cochain.comp_zero {C : Type u} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (h : n₁ + n₂ = n₁₂) :
z₁.comp 0 h = 0
@[simp]
theorem CochainComplex.HomComplex.Cochain.comp_add {C : Type u} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (z₂' : ) (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} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (z₂' : ) (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} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (h : n₁ + n₂ = n₁₂) :
z₁.comp (-z₂) h = -z₁.comp z₂ h
@[simp]
theorem CochainComplex.HomComplex.Cochain.comp_smul {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (k : R) (z₂ : ) (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} {R : Type u_1} [Ring R] [] {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (k : Rˣ) (z₂ : ) (h : n₁ + n₂ = n₁₂) :
z₁.comp (k z₂) h = k z₁.comp z₂ h
@[simp]
theorem CochainComplex.HomComplex.Cochain.comp_id {C : Type u} {F : } {G : } {n : } (z₁ : ) :
= z₁
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHoms_comp {C : Type u} {F : } {G : } {K : } (φ : (p : ) → F.X p G.X p) (ψ : (p : ) → G.X p K.X p) :
@[simp]
theorem CochainComplex.HomComplex.Cochain.ofHom_comp {C : Type u} {F : } {G : } {K : } (f : F G) (g : G K) :

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

Equations
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.diff_v {C : Type u} (K : ) (p : ) (q : ) (hpq : p + 1 = q) :
p q hpq = K.d p q
def CochainComplex.HomComplex.δ {C : Type u} {F : } {G : } (n : ) (m : ) (z : ) :

The differential on the complex of morphisms between cochain complexes.

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

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} {F : } {G : } (n : ) (m : ) (hnm : n + 1 = m) (z : ) (p : ) (q : ) (hpq : p + m = q) (q₁ : ) (q₂ : ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂) :
().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} {F : } {G : } (n : ) (m : ) (hnm : ¬n + 1 = m) (z : ) :
= 0
@[simp]
theorem CochainComplex.HomComplex.δ_hom_apply {C : Type u} (R : Type u_1) [Ring R] [] (F : ) (G : ) (n : ) (m : ) (z : ) :
() z =
def CochainComplex.HomComplex.δ_hom {C : Type u} (R : Type u_1) [Ring R] [] (F : ) (G : ) (n : ) (m : ) :

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

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem CochainComplex.HomComplex.δ_add {C : Type u} {F : } {G : } (n : ) (m : ) (z₁ : ) (z₂ : ) :
@[simp]
theorem CochainComplex.HomComplex.δ_sub {C : Type u} {F : } {G : } (n : ) (m : ) (z₁ : ) (z₂ : ) :
@[simp]
theorem CochainComplex.HomComplex.δ_zero {C : Type u} {F : } {G : } (n : ) (m : ) :
= 0
@[simp]
theorem CochainComplex.HomComplex.δ_neg {C : Type u} {F : } {G : } (n : ) (m : ) (z : ) :
@[simp]
theorem CochainComplex.HomComplex.δ_smul {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } (n : ) (m : ) (k : R) (z : ) :
@[simp]
theorem CochainComplex.HomComplex.δ_units_smul {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } (n : ) (m : ) (k : Rˣ) (z : ) :
theorem CochainComplex.HomComplex.δ_δ {C : Type u} {F : } {G : } (n₀ : ) (n₁ : ) (n₂ : ) (z : ) :
theorem CochainComplex.HomComplex.δ_comp {C : Type u} {F : } {G : } {K : } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (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 () + n₂.negOnePow ().comp z₂
theorem CochainComplex.HomComplex.δ_zero_cochain_comp {C : Type u} {F : } {G : } {K : } {n₂ : } (z₁ : ) (z₂ : ) (m₂ : ) (h₂ : n₂ + 1 = m₂) :
CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ) = z₁.comp () + n₂.negOnePow ().comp z₂
theorem CochainComplex.HomComplex.δ_comp_zero_cochain {C : Type u} {F : } {G : } {K : } {n₁ : } (z₁ : ) (z₂ : ) (m₁ : ) (h₁ : n₁ + 1 = m₁) :
CochainComplex.HomComplex.δ n₁ m₁ (z₁.comp z₂ ) = z₁.comp () h₁ + ().comp z₂
@[simp]
theorem CochainComplex.HomComplex.δ_zero_cochain_v {C : Type u} {F : } {G : } (z : ) (p : ) (q : ) (hpq : p + 1 = q) :
().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} {F : } {G : } {p : } (φ : F G) :
@[simp]
theorem CochainComplex.HomComplex.δ_ofHomotopy {C : Type u} {F : } {G : } {φ₁ : F G} {φ₂ : F G} (h : Homotopy φ₁ φ₂) :
theorem CochainComplex.HomComplex.δ_neg_one_cochain {C : Type u} {F : } {G : } (z : ) :
= CochainComplex.HomComplex.Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ) (hij : .Rel j i) => z.v i j )
@[simp]
theorem CochainComplex.HomComplex_X {C : Type u} (F : ) (G : ) (i : ) :
(F.HomComplex G).X i =
def CochainComplex.HomComplex {C : Type u} (F : ) (G : ) :

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.
Instances For
def CochainComplex.HomComplex.cocycle {C : Type u} (F : ) (G : ) (n : ) :

The subgroup of cocycles in Cochain F G n.

Equations
Instances For
def CochainComplex.HomComplex.Cocycle {C : Type u} (F : ) (G : ) (n : ) :

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

Equations
Instances For
instance CochainComplex.HomComplex.instAddCommGroupCocycle {C : Type u} (F : ) (G : ) (n : ) :
Equations
• = id inferInstance
theorem CochainComplex.HomComplex.Cocycle.mem_iff {C : Type u} {F : } {G : } (n : ) (m : ) (hnm : n + 1 = m) (z : ) :
= 0
instance CochainComplex.HomComplex.Cocycle.instCoeCochain {C : Type u} {F : } {G : } {n : } :
Equations
• CochainComplex.HomComplex.Cocycle.instCoeCochain = { coe := fun (x : ) => x }
theorem CochainComplex.HomComplex.Cocycle.ext {C : Type u} {F : } {G : } {n : } (z₁ : ) (z₂ : ) (h : z₁ = z₂) :
z₁ = z₂
theorem CochainComplex.HomComplex.Cocycle.ext_iff {C : Type u} {F : } {G : } {n : } (z₁ : ) (z₂ : ) :
z₁ = z₂ z₁ = z₂
instance CochainComplex.HomComplex.Cocycle.instSMul {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } {n : } :
Equations
• CochainComplex.HomComplex.Cocycle.instSMul = { smul := fun (r : R) (z : ) => r z, }
@[simp]
theorem CochainComplex.HomComplex.Cocycle.coe_zero {C : Type u} (F : ) (G : ) (n : ) :
0 = 0
@[simp]
theorem CochainComplex.HomComplex.Cocycle.coe_add {C : Type u} {F : } {G : } {n : } (z₁ : ) (z₂ : ) :
(z₁ + z₂) = z₁ + z₂
@[simp]
theorem CochainComplex.HomComplex.Cocycle.coe_neg {C : Type u} {F : } {G : } {n : } (z : ) :
(-z) = -z
@[simp]
theorem CochainComplex.HomComplex.Cocycle.coe_smul {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } {n : } (z : ) (x : R) :
(x z) = x z
@[simp]
theorem CochainComplex.HomComplex.Cocycle.coe_units_smul {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } {n : } (z : ) (x : Rˣ) :
(x z) = x z
@[simp]
theorem CochainComplex.HomComplex.Cocycle.coe_sub {C : Type u} {F : } {G : } {n : } (z₁ : ) (z₂ : ) :
(z₁ - z₂) = z₁ - z₂
instance CochainComplex.HomComplex.Cocycle.instModule {C : Type u} {R : Type u_1} [Ring R] [] {F : } {G : } {n : } :
Equations
• CochainComplex.HomComplex.Cocycle.instModule =
@[simp]
theorem CochainComplex.HomComplex.Cocycle.mk_coe {C : Type u} {F : } {G : } {n : } (z : ) (m : ) (hnm : n + 1 = m) (h : = 0) :
() = z
def CochainComplex.HomComplex.Cocycle.mk {C : Type u} {F : } {G : } {n : } (z : ) (m : ) (hnm : n + 1 = m) (h : = 0) :

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
• = z,
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cocycle.δ_eq_zero {C : Type u} {F : } {G : } {n : } (z : ) (m : ) :
= 0
@[simp]
theorem CochainComplex.HomComplex.Cocycle.ofHom_coe {C : Type u} {F : } {G : } (φ : F G) :
def CochainComplex.HomComplex.Cocycle.ofHom {C : Type u} {F : } {G : } (φ : F G) :

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

Equations
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cocycle.homOf_f {C : Type u} {F : } {G : } (z : ) (i : ) :
z.homOf.f i = (z).v i i
def CochainComplex.HomComplex.Cocycle.homOf {C : Type u} {F : } {G : } (z : ) :
F G

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

Equations
• z.homOf = { f := fun (i : ) => (z).v i i , comm' := }
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cocycle.homOf_ofHom_eq_self {C : Type u} {F : } {G : } (φ : F G) :
.homOf = φ
@[simp]
theorem CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self {C : Type u} {F : } {G : } (z : ) :
@[simp]
theorem CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe {C : Type u} {F : } {G : } (z : ) :
= z
@[simp]
theorem CochainComplex.HomComplex.Cocycle.equivHom_apply {C : Type u} (F : ) (G : ) (φ : F G) :
@[simp]
theorem CochainComplex.HomComplex.Cocycle.equivHom_symm_apply {C : Type u} (F : ) (G : ) (z : ) :
.symm z = z.homOf
def CochainComplex.HomComplex.Cocycle.equivHom {C : Type u} (F : ) (G : ) :
(F G) ≃+

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]

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

Equations
Instances For
@[simp]
theorem CochainComplex.HomComplex.δ_comp_zero_cocycle {C : Type u} {F : } {G : } {K : } {n : } (z₁ : ) (z₂ : ) (m : ) :
CochainComplex.HomComplex.δ n m (z₁.comp z₂ ) = ().comp z₂
@[simp]
theorem CochainComplex.HomComplex.δ_comp_ofHom {C : Type u} {F : } {G : } {K : } {n : } (z₁ : ) (f : G K) (m : ) :
CochainComplex.HomComplex.δ n m (z₁.comp ) = ().comp
@[simp]
theorem CochainComplex.HomComplex.δ_zero_cocycle_comp {C : Type u} {F : } {G : } {K : } {n : } (z₁ : ) (z₂ : ) (m : ) :
CochainComplex.HomComplex.δ n m ((z₁).comp z₂ ) = (z₁).comp ()
@[simp]
theorem CochainComplex.HomComplex.δ_ofHom_comp {C : Type u} {F : } {G : } {K : } {n : } (f : F G) (z : ) (m : ) :
CochainComplex.HomComplex.δ n m ( z ) = ()
@[simp]
theorem CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom {C : Type u} {F : } {G : } (φ₁ : F G) (φ₂ : F G) (z : { z : // }) (i : ) (j : ) :
(.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_coe {C : Type u} {F : } {G : } (φ₁ : F G) (φ₂ : F G) (ho : Homotopy φ₁ φ₂) :
def CochainComplex.HomComplex.Cochain.equivHomotopy {C : Type u} {F : } {G : } (φ₁ : F G) (φ₂ : F G) :
Homotopy φ₁ φ₂ { z : // }

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.
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq {C : Type u} {F : } {G : } {φ₁ : F G} {φ₂ : F G} (h : φ₁ = φ₂) :
() = 0
theorem CochainComplex.HomComplex.Cochain.ofHom_injective {C : Type u} {F : } {G : } {f₁ : F G} {f₂ : F G} :
f₁ = f₂
def CochainComplex.HomComplex.Cochain.map {C : Type u} {K : } {L : } {n : } {D : Type u_2} [] (z : ) (Φ : ) [Φ.Additive] :
CochainComplex.HomComplex.Cochain ((Φ.mapHomologicalComplex ).obj K) ((Φ.mapHomologicalComplex ).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
Instances For
@[simp]
theorem CochainComplex.HomComplex.Cochain.map_v {C : Type u} {K : } {L : } {n : } {D : Type u_2} [] (z : ) (Φ : ) [Φ.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} {K : } {L : } {n : } {D : Type u_2} [] (z : ) (z' : ) (Φ : ) [Φ.Additive] :
(z + z').map Φ = z.map Φ + z'.map Φ
@[simp]
theorem CochainComplex.HomComplex.Cochain.map_neg {C : Type u} {K : } {L : } {n : } {D : Type u_2} [] (z : ) (Φ : ) [Φ.Additive] :
(-z).map Φ = -z.map Φ
@[simp]
theorem CochainComplex.HomComplex.Cochain.map_sub {C : Type u} {K : } {L : } {n : } {D : Type u_2} [] (z : ) (z' : ) (Φ : ) [Φ.Additive] :
(z - z').map Φ = z.map Φ - z'.map Φ
@[simp]
theorem CochainComplex.HomComplex.Cochain.map_zero {C : Type u} (K : ) (L : ) (n : ) {D : Type u_2} [] (Φ : ) [Φ.Additive] :
@[simp]
theorem CochainComplex.HomComplex.Cochain.map_comp {C : Type u} {F : } {G : } (K : ) {D : Type u_2} [] {n₁ : } {n₂ : } {n₁₂ : } (z₁ : ) (z₂ : ) (h : n₁ + n₂ = n₁₂) (Φ : ) [Φ.Additive] :
(z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h
@[simp]
theorem CochainComplex.HomComplex.Cochain.map_ofHom {C : Type u} (K : ) (L : ) {D : Type u_2} [] (f : K L) (Φ : ) [Φ.Additive] :
= CochainComplex.HomComplex.Cochain.ofHom ((Φ.mapHomologicalComplex ).map f)
@[simp]
theorem CochainComplex.HomComplex.δ_map {C : Type u} {K : } {L : } (n : ) (m : ) {D : Type u_2} [] (z : ) (Φ : ) [Φ.Additive] :
CochainComplex.HomComplex.δ n m (z.map Φ) = ().map Φ