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
andG
.
References #
- [Brian Conrad, Grothendieck duality and base change][conrad2000]
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.)
Instances For
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
.
Instances For
A practical constructor for cochains.
Instances For
The value of a cochain on a triplet ⟨p, q, hpq⟩
.
Instances For
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 : ℤ
.
Instances For
The 0
-cochain attached to a morphism of cochain complexes.
Instances For
The cochain of degree -1
given by an homotopy between two morphism of complexes.
Instances For
The composition of cochains.
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
.
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.
The differential on a cochain complex, as a cochain of degree 1
.
Instances For
The differential on the complex of morphisms between cochain complexes.
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.
The differential on the complex of morphisms between cochain complexes, as an additive homomorphism.
Instances For
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
.
Instances For
The subgroup of cocycles in Cochain F G n
.
Instances For
The type of n
-cocycles, as a subtype of Cochain F G n
.
Instances For
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
.
Instances For
The 0
-cocycle associated to a morphism in CochainComplex C ℤ
.
Instances For
The morphism in CochainComplex C ℤ
associated to a 0
-cocycle.
Instances For
The additive equivalence between morphisms in CochainComplex C ℤ
and 0
-cocycles.
Instances For
The 1
-cocycle given by the differential on a cochain complex.