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 #
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
the condition on the two integers
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)
Instances For
Equations
- CochainComplex.HomComplex.instAddCommGroupCochain F G n = id inferInstance
Equations
- CochainComplex.HomComplex.instModuleCochain F G n = id inferInstance
A practical constructor for cochains.
Equations
- CochainComplex.HomComplex.Cochain.mk v { p := p, q := q, hpq := hpq } = v p q hpq
Instances For
The value of a cochain on a triplet ⟨p, q, hpq⟩
.
Equations
- γ.v p q hpq = γ { p := p, q := q, hpq := 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 : ℤ
.
Equations
- CochainComplex.HomComplex.Cochain.ofHoms ψ = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + 0 = q) => CategoryTheory.CategoryStruct.comp (ψ p) (CategoryTheory.eqToHom ⋯)
Instances For
The 0
-cochain attached to a morphism of cochain complexes.
Equations
- CochainComplex.HomComplex.Cochain.ofHom φ = CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => φ.f p
Instances For
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
Instances For
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 ⋯)
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
.
Equations
- CochainComplex.HomComplex.Cochain.diff K = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) => K.d p q
Instances For
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.
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' := ⋯ }
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
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)
Instances For
Equations
- CochainComplex.HomComplex.instAddCommGroupCocycle F G n = id inferInstance
Equations
- CochainComplex.HomComplex.Cocycle.instCoeCochain = { coe := fun (x : CochainComplex.HomComplex.Cocycle F G n) => ↑x }
Equations
- CochainComplex.HomComplex.Cocycle.instSMul = { smul := fun (r : R) (z : CochainComplex.HomComplex.Cocycle F G n) => ⟨r • ↑z, ⋯⟩ }
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, ⋯⟩
Instances For
The 0
-cocycle associated to a morphism in CochainComplex C ℤ
.
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 1
-cocycle given by the differential on a cochain complex.
Equations
Instances For
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
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)