The cochain complex of homomorphisms between cochain complexes
G are cochain complexes (indexed by
ℤ) in a preadditive category,
there is a cochain complex of abelian groups whose
0-cocycles identify to
F ⟶ G. Informally, in degree
n, this complex shall consist of
cochains of degree
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
q are integers and
hpq : p + n = q.
α : 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].
- Define the differential
Cochain F G n ⟶ Cochain F G m, and develop the API.
- Identify morphisms of complexes to
- Identify homotopies to
-1-cochains satisfying certain relations.
- Behaviour with respect to shifting the cochain complexes
- [Brian Conrad, Grothendieck duality and base change][conrad2000]
A term of type
HomComplex.Triplet n consists of two integers
p + n = q. (This type is introduced so that the instance
AddCommGroup (Cochain F G n) defined below can be found automatically.)
A practical constructor for cochains.
The value of a cochain on a triplet
⟨p, q, hpq⟩.
The cochain of degree
-1 given by an homotopy between two morphism of complexes.
The composition of cochains.
z₁ is a cochain of degree
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
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
p₁ + n₁ is not always the best choice.)
The associativity of the composition of cochains.
The formulation of the associativity of the composition of cochains given by the
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
there are better choices, which provides the following simplification lemmas.
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
The differential on the complex of morphisms between cochain complexes, as an additive homomorphism.
The cochain complex of homomorphisms between two cochain complexes
n : ℤ, it consists of the abelian group
HomComplex.Cochain F G n.
The additive equivalence between morphisms in
CochainComplex C ℤ and