Local Tate duality for modules with trivial action

Let K be a nonarchimedean local field containing a primitive nth root of unity ζ. This file proves Tate's local duality with values in ℤ/n for every finite module killed by n on which G_K acts trivially. It first treats the trivial module ℤ/n itself, proving that the duality maps αᵢ : Hⁱ(G_K, ℤ/n) → Hom(H²⁻ⁱ(G_K, Hom(ℤ/n, ℤ/n)), H²(G_K, ℤ/n)) in degrees 0 and 1 (TauCeti.ContCohomology.dualityMap0, dualityMap1) are bijective, α₂ (TauCeti.ContCohomology.dualityMap2) being bijective for every group acting trivially. The root ζ identifies the trivial coefficients ℤ/n with μₙ, so this is the duality of μₙ with itself, and it is the base case from which local duality for a general finite module is reached by Shapiro's lemma and the four lemma.

From ℤ/n the duality passes to every finite module A killed by n with trivial action (TauCeti.ClassFieldTheory.dualityMap0_bijective_of_isPrimitiveRoot and its companions in degrees 1 and 2), by the dévissage of TauCeti/RepresentationTheory/Homological/ContCohomology/Cup/Duality/TrivialAction.lean: A embeds into a free ℤ/n-module, along which the four lemma gives injectivity, and the injections are bijections by counting, H¹(G_K, ℤ/n) being finite.

The arithmetic input is in degree (1, 1): the cup square on H¹(G_K, ℤ/n) is a perfect pairing (TauCeti.ClassFieldTheory.cupFp_bijective_of_isPrimitiveRoot). Through ζ it is the cohomological Hilbert pairing along kummerCupPairing ζ hζ (TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_kummerCupPairing_cup), which separates the points of its second variable (TauCeti.ClassFieldTheory.separatingRight_localSymbol). By graded commutativity (TauCeti.cupFp_eq_zero_comm) it separates those of its first variable too, and H¹(G_K, ℤ/n) and its ℤ/n-linear maps to H²(G_K, ℤ/n) ≃ ℤ/n (h2FpEquivZMod) are finite of the same order, so the injection a ↦ (a ⌣ -) is a bijection. In degrees (0, 2) and (2, 0) the duality maps are scalar multiplication on H²(G_K, ℤ/n) ≃ ℤ/n; α₂ is bijective for every group acting trivially (TauCeti.ContCohomology.dualityMap2_zmod_bijective), and α₀ because H²(G_K, ℤ/n) is ℤ/n (TauCeti.ContCohomology.dualityMap0_zmod_bijective_of_addEquiv).

The duality maps are stated for any topological group H isomorphic to G_K, the form in which an open subgroup of the absolute Galois group of a smaller field, fixing a finite extension K, appears in Shapiro's lemma. The actions on ℤ/n and on A are trivial, hence continuous: each theorem takes these continuity instances, needed to state its cohomology groups, as final arguments that default to proofs from triviality, so callers never need to supply them.

Main results

• TauCeti.ClassFieldTheory.cupFp_bijective_of_isPrimitiveRoot: the cup square on H¹(G_K, ℤ/n) is a perfect pairing when K contains a primitive nth root of unity.
• TauCeti.ClassFieldTheory.map₂_cupFp_absoluteGaloisGroup_eq_top_of_isPrimitiveRoot: for a prime p, H²(G_K, 𝔽_p) is spanned by cup products of classes in H¹(G_K, 𝔽_p).
• TauCeti.ClassFieldTheory.dualityMap0_zmod_bijective_of_isPrimitiveRoot, TauCeti.ClassFieldTheory.dualityMap1_zmod_bijective_of_isPrimitiveRoot: Tate's duality maps α₀ and α₁ at the trivial module ℤ/n are bijective, for any topological group isomorphic to G_K.
• TauCeti.ClassFieldTheory.dualityMap0_bijective_of_isPrimitiveRoot, TauCeti.ClassFieldTheory.dualityMap1_bijective_of_isPrimitiveRoot, TauCeti.ClassFieldTheory.dualityMap2_bijective_of_isPrimitiveRoot: Tate's duality maps with values in ℤ/n are bijective on every finite module killed by n with trivial action, for any topological group isomorphic to G_K.

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.2, Theorem 2 and its proof.
• J.-P. Serre, Local Fields, GTM 67, Chapter XIV, §2.

theorem TauCeti.ClassFieldTheory.cupFp_bijective_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) : Function.Bijective ⇑(cupFp n (Field.absoluteGaloisGroup K))

The cup square on H¹(G_K, ℤ/n) is a perfect pairing when the nonarchimedean local field K contains a primitive nth root of unity: a ↦ (b ↦ a ⌣ b) is a bijection from H¹(G_K, ℤ/n) onto the ℤ/n-linear maps H¹(G_K, ℤ/n) → H²(G_K, ℤ/n). Through the chosen-root identification of ℤ/n with μₙ this is the perfectness of the Hilbert pairing.

theorem TauCeti.ClassFieldTheory.map₂_cupFp_absoluteGaloisGroup_eq_top_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) [Fact (Nat.Prime n)] : Submodule.map₂ (cupFp n (Field.absoluteGaloisGroup K)) ⊤ ⊤ = ⊤

H²(G_K, 𝔽_p) is spanned by cup products when the nonarchimedean local field K contains a primitive pth root of unity for a prime p: it is one-dimensional, and the perfect cup square takes a nonzero value on the nontrivial space H¹(G_K, 𝔽_p).

theorem TauCeti.ClassFieldTheory.dualityMap1_zmod_bijective_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) [DistribMulAction H (ZMod n)] (htriv : ∀ (h : H) (m : ZMod n), h • m = m) (x✝ : ContinuousSMul H (ZMod n) := ⋯) : Function.Bijective ⇑(ContCohomology.dualityMap1 H (ZMod n) (ZMod n))

Tate's duality map α₁ at the trivial module ℤ/n is bijective for a topological group H isomorphic to G_K, when the local field K contains a primitive nth root of unity: H¹(H, ℤ/n) → Hom(H¹(H, Hom(ℤ/n, ℤ/n)), H²(H, ℤ/n)) is a bijection. Under evaluation at 1 it is the cup square, a perfect pairing by cupFp_bijective_of_isPrimitiveRoot.

theorem TauCeti.ClassFieldTheory.dualityMap0_zmod_bijective_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) [DistribMulAction H (ZMod n)] (htriv : ∀ (h : H) (m : ZMod n), h • m = m) (x✝ : ContinuousSMul H (ZMod n) := ⋯) : Function.Bijective ⇑(ContCohomology.dualityMap0 H (ZMod n) (ZMod n))

Tate's duality map α₀ at the trivial module ℤ/n is bijective for a topological group H isomorphic to G_K, when the local field K contains a primitive nth root of unity: H⁰(H, ℤ/n) → Hom(H²(H, Hom(ℤ/n, ℤ/n)), H²(H, ℤ/n)) is a bijection, since it is scalar multiplication on H²(H, ℤ/n), which is ℤ/n by the local invariant (h2FpEquivZMod).

theorem TauCeti.ClassFieldTheory.dualityMap0_bijective_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) [DistribMulAction H (ZMod n)] (htriv : ∀ (h : H) (m : ZMod n), h • m = m) (A : Type u_1) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction H A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (h : H) (a : A), h • a = a) (x✝ : ContinuousSMul H (ZMod n) := ⋯) (x✝¹ : ContinuousSMul H A := ⋯) : Function.Bijective ⇑(ContCohomology.dualityMap0 H A (ZMod n))

Tate's duality map α₀ on a finite module with trivial action is bijective for a topological group H isomorphic to G_K, when the local field K contains a primitive nth root of unity: for every finite discrete H-module A killed by n on which H acts trivially, H⁰(H, A) → Hom(H²(H, Hom(A, ℤ/n)), H²(H, ℤ/n)) is a bijection. This is the case A = ℤ/n (dualityMap0_zmod_bijective_of_isPrimitiveRoot and its companions) propagated to every such A by TauCeti.ContCohomology.dualityMap0_bijective_of_smul_eq_self.

theorem TauCeti.ClassFieldTheory.dualityMap1_bijective_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) [DistribMulAction H (ZMod n)] (htriv : ∀ (h : H) (m : ZMod n), h • m = m) (A : Type u_1) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction H A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (h : H) (a : A), h • a = a) (x✝ : ContinuousSMul H (ZMod n) := ⋯) (x✝¹ : ContinuousSMul H A := ⋯) : Function.Bijective ⇑(ContCohomology.dualityMap1 H A (ZMod n))

Tate's duality map α₁ on a finite module with trivial action is bijective for a topological group H isomorphic to G_K, when the local field K contains a primitive nth root of unity: for every finite discrete H-module A killed by n on which H acts trivially, H¹(H, A) → Hom(H¹(H, Hom(A, ℤ/n)), H²(H, ℤ/n)) is a bijection.

theorem TauCeti.ClassFieldTheory.dualityMap2_bijective_of_isPrimitiveRoot {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) [DistribMulAction H (ZMod n)] (htriv : ∀ (h : H) (m : ZMod n), h • m = m) (A : Type u_1) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction H A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (h : H) (a : A), h • a = a) (x✝ : ContinuousSMul H (ZMod n) := ⋯) (x✝¹ : ContinuousSMul H A := ⋯) : Function.Bijective ⇑(ContCohomology.dualityMap2 H A (ZMod n))

Tate's duality map α₂ on a finite module with trivial action is bijective for a topological group H isomorphic to G_K, when the local field K contains a primitive nth root of unity: for every finite discrete H-module A killed by n on which H acts trivially, H²(H, A) → Hom(H⁰(H, Hom(A, ℤ/n)), H²(H, ℤ/n)) is a bijection.