Tate's duality maps of a Demushkin group

For a finite discrete 𝔽_p[G]-module M of a pro-p group G, Tate's duality maps αᵢ : Hⁱ(G, M) → Hom(H²⁻ⁱ(G, M'), H²(G, 𝔽_p)), with M' = Hom(M, 𝔽_p), are the cup products with the evaluation pairing (TauCeti.ContCohomology.dualityMap0, dualityMap1, dualityMap2). For an infinite Demushkin group they are isomorphisms for every such M: this is the perfect duality on its finite modules, and the source of cd_p G = 2. This file proves it, following Tate's argument in Serre's exposé, §9.1.

The base case is the trivial module M = 𝔽_p. Under evaluation at 1 the dual module Hom(𝔽_p, 𝔽_p) is 𝔽_p again, and the three maps read as follows. α₁ is the cup square H¹(G, 𝔽_p) → Hom(H¹(G, 𝔽_p), H²(G, 𝔽_p)), bijective because the cup square of a Demushkin group is a perfect pairing (TauCeti.IsDemushkin.cupFp_bijective). α₀ sends c ∈ 𝔽_p = H⁰(G, 𝔽_p) to multiplication by c on H²(G, 𝔽_p), bijective because H²(G, 𝔽_p) is one-dimensional. α₂ sends a class b ∈ H²(G, 𝔽_p) to c ↦ c • b, which is bijective for every group acting trivially (TauCeti.ContCohomology.dualityMap2_zmod_bijective), so no statement about it is specific to Demushkin groups.

The dévissage is the general one for pro-p groups (TauCeti.IsProP.dualityMap0_surjective_dualityMap1_injective and TauCeti.IsProP.dualityMap1_surjective_dualityMap2_injective, with N = 𝔽_p and n = p): every finite 𝔽_p[G]-module of a pro-p group is an iterated extension of trivial modules of order p, and the four lemmas along a short exact sequence carry surjectivity of α₀, bijectivity of α₁ and injectivity of α₂ from the two ends of an extension to its middle; the Baer hypothesis on H²(G, 𝔽_p) holds because it is an 𝔽_p-vector space. Two further arguments, both needing G infinite, complete the duality. Injectivity of α₀ on M is the general TauCeti.IsProP.dualityMap0_injective: it follows from injectivity of α₁ on the kernel of a trace Coind_V^G M → M that vanishes on invariants, which exists because H⁰ is co-effaceable on an infinite pro-p group. Surjectivity of α₂ on M is then the general count TauCeti.ContCohomology.dualityMap2_bijective_of_injective_of_addEquiv_zmod: H²(G, 𝔽_p) is 𝔽_p, and injectivity of α₂ on M and of α₀ on M' together with the double duality M ≅ M'' give |H²(G, M)| = |H⁰(G, M')|.

Main results

• TauCeti.IsDemushkin.dualityMap1_zmod_bijective, TauCeti.IsDemushkin.dualityMap0_zmod_bijective: Tate's duality maps α₁ and α₀ at M = 𝔽_p are bijective.
• TauCeti.IsDemushkin.dualityMap0_surjective, TauCeti.IsDemushkin.dualityMap1_bijective, TauCeti.IsDemushkin.dualityMap2_injective: the dévissage, on every finite 𝔽_p[G]-module M, α₀ is surjective, α₁ is bijective and α₂ is injective.
• TauCeti.IsDemushkin.dualityMap0_bijective, TauCeti.IsDemushkin.dualityMap2_bijective: for an infinite Demushkin group all three duality maps are bijective on every finite 𝔽_p[G]-module, Tate's perfect duality.

References

• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki exp. 252 (1963), §9.1.

theorem TauCeti.IsDemushkin.dualityMap1_zmod_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Function.Bijective ⇑(ContCohomology.dualityMap1 G (ZMod p) (ZMod p))

Tate's duality map α₁ of a Demushkin group is bijective at M = 𝔽_p: for any trivial action of G on ZMod p, H¹(G, 𝔽_p) → Hom(H¹(G, Hom(𝔽_p, 𝔽_p)), H²(G, 𝔽_p)) is a bijection. Under evaluation at 1 it is the cup square, a perfect pairing.

theorem TauCeti.IsDemushkin.dualityMap0_zmod_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Function.Bijective ⇑(ContCohomology.dualityMap0 G (ZMod p) (ZMod p))

Tate's duality map α₀ of a Demushkin group is bijective at M = 𝔽_p: for any trivial action of G on ZMod p, H⁰(G, 𝔽_p) → Hom(H²(G, Hom(𝔽_p, 𝔽_p)), H²(G, 𝔽_p)) is a bijection, since H²(G, 𝔽_p) is one-dimensional.

Dévissage: the duality maps on every finite 𝔽_p[G]-module

theorem TauCeti.IsDemushkin.dualityMap0_surjective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p • x = 0) : Function.Surjective ⇑(ContCohomology.dualityMap0 G M (ZMod p))

Tate's duality map α₀ of a Demushkin group is surjective on every finite discrete G-module M killed by p.

theorem TauCeti.IsDemushkin.dualityMap1_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p • x = 0) : Function.Bijective ⇑(ContCohomology.dualityMap1 G M (ZMod p))

Tate's duality map α₁ of a Demushkin group is bijective on every finite discrete G-module M killed by p: H¹(G, M) × H¹(G, M') → H²(G, 𝔽_p) is a perfect pairing.

theorem TauCeti.IsDemushkin.dualityMap2_injective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p • x = 0) : Function.Injective ⇑(ContCohomology.dualityMap2 G M (ZMod p))

Tate's duality map α₂ of a Demushkin group is injective on every finite discrete G-module M killed by p.

Perfect duality for infinite Demushkin groups

theorem TauCeti.IsDemushkin.dualityMap0_injective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p • x = 0) : Function.Injective ⇑(ContCohomology.dualityMap0 G M (ZMod p))

Tate's duality map α₀ of an infinite Demushkin group is injective on every finite discrete G-module M killed by p: the general TauCeti.IsProP.dualityMap0_injective, whose trace along a deep enough open subgroup vanishes on invariants, with α₁ injective on its kernel by the dévissage.

theorem TauCeti.IsDemushkin.dualityMap0_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p • x = 0) : Function.Bijective ⇑(ContCohomology.dualityMap0 G M (ZMod p))

Tate's duality map α₀ of an infinite Demushkin group is bijective on every finite discrete G-module M killed by p: H⁰(G, M) × H²(G, M') → H²(G, 𝔽_p) is a perfect pairing.

theorem TauCeti.IsDemushkin.natCard_addMonoidHom_H2 {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (V : Type u_1) [AddCommGroup V] (hV : ∀ (v : V), p • v = 0) : Nat.card (V →+ ContCohomology.H2 G (ZMod p)) = Nat.card V

Homomorphisms into H²(G, 𝔽_p) of a Demushkin group are as many as their source: for an abelian group V killed by p, |Hom(V, H²(G, 𝔽_p))| = |V|, since H²(G, 𝔽_p) is one-dimensional over 𝔽_p.

theorem TauCeti.IsDemushkin.dualityMap2_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsDemushkin p G) [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p • x = 0) : Function.Bijective ⇑(ContCohomology.dualityMap2 G M (ZMod p))

Tate's duality map α₂ of an infinite Demushkin group is bijective on every finite discrete G-module M killed by p: H²(G, M) × H⁰(G, M') → H²(G, 𝔽_p) is a perfect pairing, where M' = Hom(M, 𝔽_p). It is injective by the dévissage and bijective by counting (TauCeti.ContCohomology.dualityMap2_bijective_of_injective_of_addEquiv_zmod), since α₀ is injective on M' and H²(G, 𝔽_p) is 𝔽_p.