Evaluation cups for finite discrete modules #
For a finite discrete G-module M and a discrete module N, evaluation is an equivariant
biadditive pairing from InternalHom G M N and M to N. The three low-degree cup shapes of
total degree two give pairings from Hⁱ(G, InternalHom G M N) and H²⁻ⁱ(G, M) to H²(G, N).
These are the underlying cohomological pairings used in duality statements.
The cochain formulas below fix the order of the two inputs: the internal hom is always the first
factor, so in degree (1,1) the evaluation is a(g) (g • b(h)).
The three pairings are compatible with the maps of coefficients in two ways (Serre, exposé 252,
§9.1, following Tate). First, they are natural in the module: a G-map f : M →+[G] M' and
its dual InternalHom.precomp G f are adjoint, ⟨φ, f_* b⟩ = ⟨f^* φ, b⟩ in each of the three
shapes. Second, they are compatible with the connecting maps of a short exact sequence
0 → A → B → C → 0 and of its dual sequence 0 → C' → B' → A' → 0, whenever the latter exists
(DiscreteShortExact.dual, for instance for modules killed by a prime): in the two shapes of
total degree two that involve a connecting map, the connecting map of the dual sequence, paired
against a class of the original one, is the connecting map of the original sequence paired against
the dual class, with the Leibniz sign (-1)^(p+1) of the degree p of the dual class. These are
the low-degree identities needed to compare the duality maps
Hⁱ(G, M) → Hom(H²⁻ⁱ(G, M'), H²(G, N)), i = 0, 1, 2, along the segment
H⁰(G, A) → H⁰(G, B) → H⁰(G, C) → H¹(G, A) → H¹(G, B) → H¹(G, C) → H²(G, A) → H²(G, B) → H²(G, C)
of the long exact sequence of a short exact sequence and the corresponding segment for its dual.
Read with the module first, the same cups give Tate's duality maps
αᵢ : Hⁱ(G, M) → Hom(H²⁻ⁱ(G, InternalHom G M N), H²(G, N)), x ↦ ⟨x, -⟩, for i = 0, 1, 2
(Serre, Structure de certains pro-p-groupes, §9.1): TauCeti.ContCohomology.dualityMap0,
dualityMap1 and dualityMap2. They are the explicit cups along the opposite evaluation pairing
(m, φ) ↦ φ m, so graded commutativity relates them to the evaluation cups: α₀ and α₂ are the
(2,0) and (0,2) evaluation cups with their arguments swapped, and α₁ is the negative of the
swapped (1,1) evaluation cup. For a trivial action on ZMod n the internal hom is ZMod n again,
by evaluation at 1, and the duality maps are scalar multiplication on H²(G, ZMod n) in degrees
0 and 2 and the cup product of multiplication in degree 1. In that setting α₂ is always
bijective, and α₀ is bijective as soon as H²(G, ZMod p) is one-dimensional.
Read through the duality maps, naturality in the module says αᵢ (f_* x) b = αᵢ x (f^* b), so for a
bijective f the square formed by αᵢ on M, αᵢ on M', f_* on cohomology and f^* on the
targets commutes, and bijectivity of each αᵢ transports from M' to M. This is how a base case
stated for ZMod p applies to every trivial module of order p.
Finally, when N ≃+ ZMod n and H²(G, N) ≃+ ZMod n, injectivity of αᵢ on a finite module M
killed by n upgrades to bijectivity by counting
(TauCeti.ContCohomology.dualityMap0_bijective_of_injective_of_addEquiv_zmod and its companions in
degrees 1 and 2), once α₂₋ᵢ is known to be injective on the dual M' = InternalHom G M N,
and, in degree 1, H¹(G, M') is known to be finite:
Hom(-, H²(G, N)) preserves the order of a finite group killed by n, and M is its own double
dual with values in N (TauCeti.InternalHom.eval_bijective_of_addEquiv_zmod), so the two
injections Hⁱ(G, M) ↪ Hom(H²⁻ⁱ(G, M'), H²(G, N)) and H²⁻ⁱ(G, M') ↪ Hom(Hⁱ(G, M''), H²(G, N))
force |Hⁱ(G, M)| = |H²⁻ⁱ(G, M')|. This is the last step of Tate's duality for the coefficient
systems 𝔽_p and ℤ/pⁱ of a Demushkin group.
Main statements #
TauCeti.ContCohomology.explicitDualityPairing02,explicitDualityPairing11andexplicitDualityPairing20, with their cochain formulasexplicitDualityPairing02_mk,explicitDualityPairing11_mkandexplicitDualityPairing20_mk.TauCeti.ContCohomology.explicitDualityPairing02_explicitCoeff2,explicitDualityPairing11_explicitCoeff1andexplicitDualityPairing20_explicitCoeff0: naturality in the module,⟨φ, f_* b⟩ = ⟨f^* φ, b⟩, one identity per shape.explicitDualityPairing11_explicitDelta0_dual_eq_neg_explicitDualityPairing02_explicitDelta1andexplicitDualityPairing20_explicitDelta1_dual_eq_explicitDualityPairing11_explicitDelta0: compatibility with the connecting maps of a short exact sequence and of its dual sequence,⟨δ x, y⟩ = (-1)^(p+1) ⟨x, δ y⟩, in the two shapes of total degree two that involve a connecting map.TauCeti.ContCohomology.dualityMap0,dualityMap1anddualityMap2: Tate's duality maps, with their cochain formulasdualityMap0_mk,dualityMap1_mk,dualityMap2_mkand their comparison with the evaluation cupsdualityMap0_eq_explicitDualityPairing20,dualityMap1_eq_neg_explicitDualityPairing11anddualityMap2_eq_explicitDualityPairing02.TauCeti.ContCohomology.dualityMap0_explicitCoeff0,dualityMap1_explicitCoeff1anddualityMap2_explicitCoeff2: naturality of the duality maps in the module,αᵢ (f_* x) b = αᵢ x (f^* b);explicitCoeff2_injective_of_dualityMap2_injective: whenα₂is injective onMandf^*is surjective on the invariants,f_*is injective onH²; anddualityMap0_injective_of_injective: injectivity ofα₀descends along an injection of modules.TauCeti.ContCohomology.dualityMap0_bijective_of_bijective,dualityMap1_bijective_of_bijectiveanddualityMap2_bijective_of_bijective: bijectivity of each duality map transports along an isomorphism of modules.TauCeti.ContCohomology.explicitCoeff2_dualityMap0,explicitCoeff2_dualityMap1andexplicitCoeff2_dualityMap2: naturality of the duality maps in the coefficients,f_* (αᵢ x b) = αᵢ x ((f ∘ -)_* b)for aG-mapf : N →+[G] N'.TauCeti.ContCohomology.dualityMap0_bijective_of_injective_of_forall_nsmul_eq_zero,dualityMap1_bijective_of_injective_of_forall_nsmul_eq_zeroanddualityMap2_bijective_of_injective_of_forall_nsmul_eq_zero: on a module killed byn, bijectivity of each duality map transports along an injection of coefficientsN →+[G] N'whose range is then-torsion, on the modules and onH².TauCeti.ContCohomology.dualityMap0_injective_iff_of_bijective,dualityMap0_surjective_iff_of_bijective,dualityMap0_bijective_iff_of_bijectiveand their analogues in degrees1and2: injectivity, surjectivity and bijectivity of each duality map transport along an isomorphism of coefficientsN →+[G] N'.TauCeti.ContCohomology.dualityMap0_bijective_of_injective_of_addEquiv_zmod,dualityMap1_bijective_of_injective_of_addEquiv_zmodanddualityMap2_bijective_of_injective_of_addEquiv_zmod: forN ≃+ ZMod nandH²(G, N) ≃+ ZMod n, ifαᵢis injective onMandα₂₋ᵢis injective on its dualM'(and, fori = 1,H¹(G, M')is finite), thenαᵢis bijective onM, by counting.TauCeti.ContCohomology.dualityMap2_zmod_bijective:α₂is bijective for a trivial action onZMod n.TauCeti.ContCohomology.dualityMap0_zmod_bijective_of_addEquiv: for a trivial action onZMod n,α₀is bijective whenH²(G, ZMod n) ≃+ ZMod n; anddualityMap0_zmod_bijective_of_finrank_eq_one: the same fornprime whenH²(G, ZMod n)hasℤ/n-dimension1.TauCeti.ContCohomology.dualityMap1_zmod_bijective_iff: for a trivial action onZMod n,α₁is bijective exactly when the cup product of multiplication onH¹(G, ZMod n)is a perfect pairing.
References #
- J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9.1: Tate's duality argument, in which the evaluation pairings are compared along the long exact sequences of a finite module and of its dual.
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.4.2), (1.4.3) and (1.4.5): naturality of the cup product in the coefficients and its compatibility with the connecting homomorphisms.
- J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I §0, the cup-product properties (0.1.1)-(0.1.6).
Evaluation on H⁰(G, InternalHom G M N) × H²(G, M).
Instances For
The (0,2) evaluation pairing is the explicit (0,2) cup along the evaluation pairing.
On cocycles, the (0,2) evaluation cup evaluates the invariant homomorphism pointwise.
Evaluation on H¹(G, InternalHom G M N) × H¹(G, M).
Instances For
The (1,1) evaluation pairing is the explicit (1,1) cup along the evaluation pairing.
Evaluation on H²(G, InternalHom G M N) × H⁰(G, M).
Instances For
The (2,0) evaluation pairing is the explicit (2,0) cup along the evaluation pairing.
On cocycles, the (1,1) evaluation cup applies the first cocycle to the translate of the
second.
On cocycles, the (2,0) evaluation cup evaluates at an invariant element of M.
Naturality in the module #
For a G-map f : M →+[G] M' the dual map is precomposition,
f^* = InternalHom.precomp G f : InternalHom G M' N →+[G] InternalHom G M N, and the evaluation
pairings of M and of M' are intertwined by (f^* φ) m = φ (f m). On cohomology this is the
adjunction ⟨φ, f_* b⟩ = ⟨f^* φ, b⟩, one identity for each of the three shapes (0, 2), (1, 1)
and (2, 0). Each follows from the naturality of the cup product in the pairing, applied twice:
once from the mixed pairing (φ, m) ↦ φ (f m) of InternalHom G M' N with M to the evaluation
pairing of M', along (id, f), and once from the mixed pairing to the evaluation pairing of M,
along (f^*, id).
Naturality of the (0,2) evaluation pairing in the module. For a G-map f : M →+[G] M',
an invariant φ of InternalHom G M' N and a class b ∈ H²(G, M), pairing φ with f_* b
is pairing the precomposed invariant f^* φ with b.
Naturality of the (1,1) evaluation pairing in the module. For a G-map f : M →+[G] M'
and classes φ ∈ H¹(G, InternalHom G M' N) and b ∈ H¹(G, M), pairing φ with f_* b is
pairing the precomposed class f^* φ with b.
Naturality of the (2,0) evaluation pairing in the module. For a G-map f : M →+[G] M',
a class φ ∈ H²(G, InternalHom G M' N) and an invariant b of M, pairing φ with f b is
pairing the precomposed class f^* φ with b.
Compatibility with the connecting maps of a short exact sequence and of its dual #
Let 0 → A → B → C → 0 be a short exact sequence of finite discrete G-modules and let
0 → C' → B' → A' → 0 be its dual sequence DiscreteShortExact.dual, where
X' = InternalHom G X N; the dual sequence exists whenever homomorphisms A →+ N extend to
B, for instance when B is killed by a prime. The sub-object C' of the dual sequence pairs
with the quotient C of the original one, and the quotient A' pairs with the sub-object A, so
the two sequences are a compatibly paired pair in the sense of
TauCeti/RepresentationTheory/Homological/ContCohomology/Cup/ConnectingMap/Basic.lean, and the
adjointness identities there specialize to the evaluation pairings.
The connecting maps δ⁰ of the dual sequence and δ¹ of the original sequence are
anti-adjoint under the evaluation pairings. For an invariant x of A' = InternalHom G A N and
a class y ∈ H¹(G, C), the (1,1) pairing of δ⁰ x ∈ H¹(G, C') with y is the negative of the
(0,2) pairing of x with δ¹ y ∈ H²(G, A).
The connecting maps δ¹ of the dual sequence and δ⁰ of the original sequence are adjoint
under the evaluation pairings. For a class x ∈ H¹(G, A'), A' = InternalHom G A N, and an
invariant y of C, the (2,0) pairing of δ¹ x ∈ H²(G, C') with y is the (1,1) pairing of
x with δ⁰ y ∈ H¹(G, A); the Leibniz sign is 1 because x has degree one.
Tate's duality maps #
The evaluation cups with the module in the first slot.
Tate's duality map in degree 0,
α₀ : H⁰(G, M) → Hom(H²(G, InternalHom G M N), H²(G, N)): the (0,2) cup along the opposite
evaluation pairing, α₀ m b = ⟨m, b⟩, the class of the cocycle (g, h) ↦ b (g, h) m.
Instances For
Tate's duality map in degree 1,
α₁ : H¹(G, M) → Hom(H¹(G, InternalHom G M N), H²(G, N)): the (1,1) cup along the opposite
evaluation pairing, α₁ a b = ⟨a, b⟩, the class of the cocycle (g, h) ↦ (g • b h) (a g).
Instances For
Tate's degree-one duality map is the explicit cup along the opposite evaluation pairing.
On cocycles, α₀ evaluates the cocycle at the invariant element.
On cocycles, α₁ applies the translate of the second cocycle to the first.
α₀ is the (2,0) evaluation cup with its arguments swapped: graded commutativity in
bidegree (0,2), where the sign is 1 (explicitCup02_eq_cup20_flip along the opposite
evaluation pairing).
α₁ is the negative of the (1,1) evaluation cup with its arguments swapped: graded
commutativity in bidegree (1,1), where the sign is -1 (explicitCup11_eq_neg_flip along the
opposite evaluation pairing).
In degree 2 the internal hom sits in the degree-zero slot of the cup, whose continuity is
never used, so α₂ needs neither continuous inversion on G nor finiteness of M.
Tate's duality map in degree 2,
α₂ : H²(G, M) → Hom(H⁰(G, InternalHom G M N), H²(G, N)): the (2,0) cup along the opposite
evaluation pairing, α₂ b φ = ⟨b, φ⟩, the class of the cocycle (g, h) ↦ φ (b (g, h)) for an
invariant φ.
Instances For
On cocycles, α₂ applies the translate of the invariant homomorphism to the cocycle.
α₂ is the (0,2) evaluation cup with its arguments swapped: graded commutativity in
bidegree (2,0), where the sign is 1 (explicitCup02_eq_cup20_flip along the evaluation
pairing, read backwards).
Naturality of the duality maps in the module #
Through the comparison with the evaluation cups, the adjunction ⟨φ, f_* b⟩ = ⟨f^* φ, b⟩ reads
αᵢ (f_* x) b = αᵢ x (f^* b) for each of the three duality maps. As for the evaluation cups, these
are not simp lemmas: neither side is a normal form.
Naturality of α₀ in the module: α₀ (f_* x) b = α₀ x (f^* b).
Naturality of α₁ in the module: α₁ (f_* x) b = α₁ x (f^* b).
Injectivity of α₀ descends along an injection of modules: if f : M →+[G] M' is injective
and α₀ is injective at M', then α₀ is injective at M. An invariant x with α₀ x = 0 has
α₀ (f_* x) = α₀ x ∘ f^* = 0, so f x = 0.
Naturality of α₂ in the module: α₂ (f_* x) b = α₂ x (f^* b).
Injectivity of f_* on H² from injectivity of α₂. If α₂ is injective at M and every
invariant homomorphism M → N is the restriction along f : M →+[G] M' of an invariant
homomorphism M' → N, then f_* : H²(G, M) → H²(G, M') is injective: a class x with f_* x = 0
pairs to zero with every f^* b, hence with every invariant of Hom(M, N), so α₂ x = 0.
Transport along an isomorphism of modules #
A bijective equivariant homomorphism f : M →+[G] M' induces bijections on cohomology and, through
its dual f^*, on the targets of the duality maps; the naturality squares then carry bijectivity
of each duality map from M' to M.
Bijectivity of α₂ transports along an isomorphism of modules.
Bijectivity of α₀ transports along an isomorphism of modules.
Bijectivity of α₁ transports along an isomorphism of modules.
Naturality of the duality maps in the coefficients #
An equivariant homomorphism f : N →+[G] N' of coefficient modules induces f_* on H²(G, -) and,
through postcomposition f ∘ - on the internal hom, maps between the sources of the targets of the
duality maps, and the three duality maps are natural in the coefficients:
f_* (αᵢ x b) = αᵢ x ((f ∘ -)_* b). When f is injective with range the n-torsion of N', both
on the modules and on H², and M is killed by n, bijectivity of each αᵢ transports from N
to N': the groups H²⁻ⁱ(G, InternalHom G M N) are killed by n, so postcomposition with f_*
is a bijection onto the homomorphisms into H²(G, N'). This is how the duality at 𝔽_p
coefficients is read at the coefficients ℤ/pⁱ, on a module killed by p.
Naturality of α₂ in the coefficients: f_* (α₂ x b) = α₂ x ((f ∘ -)_* b).
Bijectivity of α₂ transports along an injection of coefficients onto the n-torsion, on
a module M killed by n: if f : N →+[G] N' is injective with range the n-torsion of N', and
f_* is injective on H² with range the n-torsion of H²(G, N'), then α₂ at the coefficients
N' is bijective as soon as it is at the coefficients N.
Naturality of α₀ in the coefficients: f_* (α₀ x b) = α₀ x ((f ∘ -)_* b).
Naturality of α₁ in the coefficients: f_* (α₁ x b) = α₁ x ((f ∘ -)_* b).
Bijectivity of α₀ transports along an injection of coefficients onto the n-torsion, on
a finite module M killed by n; the hypotheses are those of
dualityMap2_bijective_of_injective_of_forall_nsmul_eq_zero.
Bijectivity of α₁ transports along an injection of coefficients onto the n-torsion, on
a finite module M killed by n; the hypotheses are those of
dualityMap2_bijective_of_injective_of_forall_nsmul_eq_zero.
Transport of the duality maps along an isomorphism of the coefficients #
For a bijective f : N →+[G] N', naturality in the coefficients makes the square formed by αᵢ at
the coefficients N and N', postcomposition with f_* on H²(G, -) and precomposition with
(f ∘ -)_* on the sources commute, and the two latter maps are bijections. Hence αᵢ is injective,
surjective or bijective at N exactly when it is at N'. This is how a duality statement for a
G-module N, read on a subgroup U ≤ G through the restricted action, is carried to the
U-module canonically attached to U: for a character χ of G, from the twisted coefficients
I(χ)/pⁱ restricted to U to the twisted coefficients I(χ|_U)/pⁱ of the restricted character.
The transport square of α₂: postcomposing α₂ at the coefficients N with f_* is
precomposing α₂ at the coefficients N' with (f ∘ -)_*, the function form of
explicitCoeff2_dualityMap2.
Injectivity of α₂ transports along an isomorphism of coefficients.
Surjectivity of α₂ transports along an isomorphism of coefficients.
Bijectivity of α₂ transports along an isomorphism of coefficients.
The transport square of α₀: postcomposing α₀ at the coefficients N with f_* is
precomposing α₀ at the coefficients N' with (f ∘ -)_*, the function form of
explicitCoeff2_dualityMap0.
The transport square of α₁: postcomposing α₁ at the coefficients N with f_* is
precomposing α₁ at the coefficients N' with (f ∘ -)_*, the function form of
explicitCoeff2_dualityMap1.
Injectivity of α₀ transports along an isomorphism of coefficients.
Surjectivity of α₀ transports along an isomorphism of coefficients.
Bijectivity of α₀ transports along an isomorphism of coefficients.
Injectivity of α₁ transports along an isomorphism of coefficients.
Surjectivity of α₁ transports along an isomorphism of coefficients.
Bijectivity of α₁ transports along an isomorphism of coefficients.
Bijectivity of α₀ by counting. Let N ≃+ ZMod n and H²(G, N) ≃+ ZMod n, and let M be
a finite discrete G-module killed by n, with dual M' = InternalHom G M N. If α₀ is injective
on M and α₂ is injective on M', then α₀ : H⁰(G, M) → Hom(H²(G, M'), H²(G, N)) is bijective:
its target has the order of H²(G, M'), which α₂ embeds into Hom(H⁰(G, M''), H²(G, N)), of the
order of H⁰(G, M''), and M'' ≅ M by double duality.
Bijectivity of α₁ by counting. Let N ≃+ ZMod n and H²(G, N) ≃+ ZMod n, and let M be
a finite discrete G-module killed by n whose dual M' = InternalHom G M N has finite
H¹(G, M'). If α₁ is injective on M and on M', then
α₁ : H¹(G, M) → Hom(H¹(G, M'), H²(G, N)) is bijective: its target has the order of H¹(G, M'),
which α₁ embeds into Hom(H¹(G, M''), H²(G, N)), of the order of H¹(G, M''), and M'' ≅ M by
double duality.
Bijectivity of α₂ by counting. Let N ≃+ ZMod n and H²(G, N) ≃+ ZMod n, and let M be
a finite discrete G-module killed by n, with dual M' = InternalHom G M N. If α₂ is injective
on M and α₀ is injective on M', then α₂ : H²(G, M) → Hom(H⁰(G, M'), H²(G, N)) is bijective:
its target has the order of H⁰(G, M'), which α₀ embeds into Hom(H²(G, M''), H²(G, N)), of the
order of H²(G, M''), and M'' ≅ M by double duality. The hypothesis H²(G, N) ≃+ ZMod n is what
makes Hom(-, H²(G, N)) preserve the order of every finite group killed by n.
Trivial ZMod n coefficients #
For a trivial action of G on ZMod n the conjugation action on the internal hom
InternalHom G (ZMod n) (ZMod n) is trivial too
(TauCeti.InternalHom.smul_eq_self_of_smul_eq_self), and evaluation at 1 identifies the internal
hom with ZMod n as G-modules (TauCeti.InternalHom.zmodEquiv_smul). Under that identification
α₀ and α₂ are scalar multiplication on H²(G, ZMod n), and α₁ is the cup product of
multiplication in ZMod n.
The two statements about α₂ need only continuous multiplication on G.
α₂ at trivial ZMod n coefficients is scalar multiplication: α₂ b φ = φ 1 • b.
α₂ at trivial ZMod n coefficients is bijective, for every group G with continuous
multiplication acting trivially on ZMod n: under evaluation at 1 it sends b to c ↦ c • b,
and a homomorphism out of ZMod n into a group killed by n is determined by its value at 1.
The statements below involve the internal hom InternalHom G (ZMod n) (ZMod n) as a
topological G-module, or the duality maps α₀ and α₁, all of which need finite coefficients:
ZMod n is finite exactly when n ≠ 0.
For a trivial action on ZMod n, the first cohomology of InternalHom G (ZMod n) (ZMod n) is
that of ZMod n, along evaluation at 1.
Instances For
For a trivial action on ZMod n, the second cohomology of InternalHom G (ZMod n) (ZMod n) is
that of ZMod n, along evaluation at 1.
Instances For
On cocycle classes, H1InternalHomZModEquiv evaluates the cocycle at 1 pointwise: it is the
cocycle pushforward along TauCeti.InternalHom.zmodEquiv, whose values are given by
cocyclesMap1_apply.
On cocycle classes, H2InternalHomZModEquiv evaluates the cocycle at 1 pointwise: it is the
cocycle pushforward along TauCeti.InternalHom.zmodEquiv, whose values are given by
cocyclesMap2_apply.
α₀ at trivial ZMod n coefficients is scalar multiplication: α₀ m b = m • b, reading
b in H²(G, ZMod n) through evaluation at 1.
α₁ at trivial ZMod n coefficients is the cup product of multiplication:
α₁ a b = a ⌣ b, reading b in H¹(G, ZMod n) through evaluation at 1.
α₁ at trivial ZMod n coefficients is bijective exactly when the cup product of
multiplication is a perfect pairing on H¹(G, ZMod n): by dualityMap1_zmod, α₁ is
a ↦ a ⌣ -, read on H¹(G, Hom(ZMod n, ZMod n)) through evaluation at 1.
α₀ at trivial ZMod n coefficients is bijective when H²(G, ZMod n) is ZMod n:
under evaluation at 1 it sends c to multiplication by c, and every additive endomorphism of
ZMod n is a multiplication.
α₀ at trivial 𝔽_p coefficients is bijective when H²(G, 𝔽_p) is one-dimensional,
being then isomorphic to 𝔽_p (dualityMap0_zmod_bijective_of_addEquiv).