The evaluation pairings and an open subgroup: restriction, corestriction and Shapiro #

Let U be an open subgroup of finite index of a topological group G, let M be a finite discrete G-module and N a discrete G-module. The evaluation pairings ⟨-, -⟩_G : Hⁱ(G, Hom(M, N)) × H²⁻ⁱ(G, M) → H²(G, N) of TauCeti/RepresentationTheory/Homological/ContCohomology/Cup/Duality/Basic.lean are compatible with the change of group to U in three ways.

Restriction preserves them: res ⟨φ, b⟩_G = ⟨res φ, res b⟩_U. The restriction of a class of Hⁱ(G, InternalHom G M N) is a class of Hⁱ(U, InternalHom G M N), the internal hom of the G-modules with the restricted action; TauCeti.InternalHom.restrict identifies that module with the internal hom InternalHom U M N of the U-modules, and on it the U-pairing is the cup along the evaluation pairing of G (explicitDualityPairing02_explicitCoeff0_restrict and its two companions).
Restriction and corestriction are adjoint: cor ⟨res φ, b⟩_U = ⟨φ, cor b⟩_G, the projection formula for the evaluation pairings. A class of U paired against a restricted class of G is detected, after corestriction, by the pairing of G; this is the identity through which the duality of an open subgroup is compared with that of the ambient group.
Shapiro's lemma transports them: for a discrete U-module A and G profinite, the dual of the coinduced module Coind_U^G A is again coinduced, Hom(Coind_U^G A, N) ≅ Coind_U^G Hom(A, N) through TauCeti.DiscreteCoind.toInternalHom (a bijection when the conjugation action of U on Hom(A, N) is continuous, as it is for a finite A), and Shapiro's lemma identifies the cohomology of both coinduced modules with that of U. Under these identifications the (1,1) evaluation pairing of G is the corestriction of the evaluation pairing of U:
```
⟨toInternalHom F, x⟩_G = cor_U^G ⟨sh F, sh x⟩_U.
```
This is the identity through which a duality statement for the finite modules of G is read on the open subgroup U: a class of H¹(U, A) is detected by the pairing of U as soon as its inverse Shapiro image is detected by the pairing of G. The same identity holds in the (0,2) shape, and there it says that injectivity of Tate's duality map α₂ descends from G to U: if α₂ of G is injective on the coinduced module Coind_U^G A, then α₂ of U is injective on A, for every discrete U-module A whose internal hom Hom(A, N) carries a continuous conjugation action.

The first two are the specializations to the evaluation pairing of the general statements for the explicit cup products, compatibility with restriction from TauCeti/RepresentationTheory/Homological/ContCohomology/Cup/Restriction.lean and the projection formula from TauCeti/RepresentationTheory/Homological/ContCohomology/ProjectionFormula.lean, through the naturality of the cup product in the pairing. In the (2,0) shape the restricted class is the degree-two one, so the projection formula used is the one with restriction on the cocycle factor, TauCeti.ContCohomology.explicitCup_projection20_res_left. For the third, the evaluation pairing of G on the coinduced modules is the trace of the pointwise evaluation pairing (TauCeti.DiscreteCoind.toAddMonoidHom_toInternalHom_apply), the cup product is natural in the pairing, and the corestriction of a cup product of U is the trace of the cup product of G along the pointwise pairing of the inverse Shapiro images (TauCeti.ContCohomology.explicitCor2_explicitCup02 in the (0,2) shape and explicitCor2_explicitCup11 in the (1,1) shape).

Main statements #

TauCeti.ContCohomology.explicitDualityPairing02_explicitCoeff0_restrict, explicitDualityPairing11_explicitCoeff1_restrict and explicitDualityPairing20_explicitCoeff2_restrict: on the restricted internal hom, the evaluation pairing of the U-modules is the cup along the evaluation pairing of G.
TauCeti.ContCohomology.explicitRes2_explicitDualityPairing02, explicitRes2_explicitDualityPairing11 and explicitRes2_explicitDualityPairing20: restriction preserves the evaluation pairings.
TauCeti.ContCohomology.explicitDualityPairing02_projection, explicitDualityPairing11_projection and explicitDualityPairing20_projection: the projection formula cor ⟨res φ, b⟩_U = ⟨φ, cor b⟩_G for the evaluation pairings.
TauCeti.ContCohomology.explicitDualityPairing11_explicitCoeff1_toInternalHom and explicitDualityPairing02_explicitCoeff0_toInternalHom and explicitDualityPairing20_explicitCoeff2_toInternalHom: the evaluation pairing of a coinduced module is the corestriction of the corresponding evaluation pairing of U on the Shapiro images.
TauCeti.ContCohomology.dualityMap0_bijective_discreteCoind_of_bijective, dualityMap1_bijective_discreteCoind_of_bijective and dualityMap2_bijective_discreteCoind_of_bijective: perfect duality is transported by Shapiro's lemma from an open subgroup to a coinduced module, when corestriction on the target is bijective.
TauCeti.ContCohomology.dualityMap2_injective_of_injective_discreteCoind: injectivity of Tate's duality map α₂ descends to an open subgroup: if α₂ of G is injective on Coind_U^G A, then α₂ of U is injective on A.

References #

J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9: the duality of an open subgroup of a Demushkin group is compared with that of the group through restriction and corestriction, and §9.2: the cohomology of the open subgroup is read through the coinduced module.
J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.3)(i) and (iv): compatibility of the cup product with restriction, and the projection formula.