Tate's duality maps on modules with trivial action

Let G be a topological group and N a discrete G-module on which G acts trivially, with N ≃+ ZMod n and H²(G, N) ≃+ ZMod n for some n ≠ 0. For a finite discrete G-module A write A' = InternalHom G A N for its dual and αᵢ : Hⁱ(G, A) → Hom(H²⁻ⁱ(G, A'), H²(G, N)), i = 0, 1, 2, for Tate's duality maps (TauCeti.ContCohomology.dualityMap0, dualityMap1, dualityMap2).

This file proves that Tate's duality for the module N itself gives Tate's duality for every finite module killed by n with trivial action (TauCeti.ContCohomology.dualityMap0_bijective_of_smul_eq_self, dualityMap1_bijective_of_smul_eq_self, dualityMap2_bijective_of_smul_eq_self): if α₀, α₁ are bijective and α₂ is injective for A = N, and H¹(G, N) is finite, then the three duality maps are bijective for every such A. Over a local field K containing the n-th roots of unity, with N = ℤ/n ≅ μₙ, this is the passage from the cyclic module ℤ/n to every finite module on which the Galois group acts trivially, the base case of local Tate duality.

A finite module with trivial action need not be a sum of copies of N (ℤ/2 is not a direct summand of ℤ/4), so the argument runs through the free modules Nᵏ = Fin k → N and the injectivity statements, which then upgrade to bijectivity by counting.

• Free modules. Along the split sequence 0 → N → Nᵏ⁺¹ → Nᵏ → 0, the four lemmas (TauCeti.ContCohomology.DiscreteShortExact.dualityMap0_surjective and its companions) carry α₀ surjective, α₁ bijective and α₂ injective from N to every Nᵏ.
• Degree zero. α₀ is injective on every finite A with trivial action killed by n, because the maps A → N separate the points of A (TauCeti.exists_addMonoidHom_zmod_apply_ne_zero) and α₀ is natural in the module (TauCeti.ContCohomology.dualityMap0_explicitCoeff0).
• Degrees one and two. The same maps embed A into a free module Nᵏ, whose cokernel C is again finite with trivial action and killed by n. The four lemmas concluding injectivity on the submodule (TauCeti.ContCohomology.DiscreteShortExact.dualityMap1_injective_left, DiscreteShortExact.dualityMap2_injective_left) along 0 → A → Nᵏ → C → 0 then give α₁ injective on A from α₀ injective on C, and α₂ injective on A from α₁ injective on C.
• Counting. The dual A' is again finite with trivial action and killed by n, and H¹(G, A') is finite, embedding into a power of H¹(G, N) (TauCeti.ContCohomology.finite_H1_of_smul_eq_self); so injectivity of αᵢ on A and of α₂₋ᵢ on A' makes αᵢ bijective on A (TauCeti.ContCohomology.dualityMap0_bijective_of_injective_of_addEquiv_zmod and its companions).

Main results

• TauCeti.ContCohomology.finite_H1_of_smul_eq_self: for trivial actions, H¹(G, A) is finite for every finite A killed by n once H¹(G, N) is.
• TauCeti.ContCohomology.dualityMap0_injective_of_smul_eq_self: α₀ is injective on every finite A with trivial action killed by n once it is injective on N.
• TauCeti.ContCohomology.dualityMap0_bijective_of_smul_eq_self, dualityMap1_bijective_of_smul_eq_self and dualityMap2_bijective_of_smul_eq_self: Tate's duality on every finite module with trivial action killed by n, from Tate's duality on N.

References

• J.-P. Serre, Galois Cohomology, Ch. II, §5.2, proof of Theorem 2.
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, proof of Theorem 2.1.

theorem TauCeti.ContCohomology.finite_H1_of_smul_eq_self {G : Type uG} [Group G] {N : Type uN} [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [NeZero n] (hN : ∀ (g : G) (y : N), g • y = y) (e : N ≃+ ZMod n) {A : Type uA} [AddCommGroup A] [DistribMulAction G A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (g : G) (a : A), g • a = a) [TopologicalSpace G] [TopologicalSpace N] [DiscreteTopology N] [ContinuousSMul G N] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul G A] [Finite A] [Finite (H1 G N)] : Finite (H1 G A)

H¹ of a module with trivial action is finite when H¹(G, N) is: for a finite A killed by n on which G acts trivially, the classes of H¹(G, A) are continuous homomorphisms G → A, and the maps A → N separate them, so H¹(G, A) embeds into a finite power of H¹(G, N).

theorem TauCeti.ContCohomology.dualityMap0_injective_of_smul_eq_self {G : Type uG} [Group G] {N : Type uN} [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [NeZero n] (hN : ∀ (g : G) (y : N), g • y = y) (e : N ≃+ ZMod n) {A : Type uA} [AddCommGroup A] [DistribMulAction G A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (g : G) (a : A), g • a = a) [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace N] [DiscreteTopology N] [ContinuousSMul G N] [TopologicalSpace A] [DiscreteTopology A] [ContinuousSMul G A] [Finite A] (h₀ : Function.Injective ⇑(dualityMap0 G N N)) : Function.Injective ⇑(dualityMap0 G A N)

α₀ is injective on every module with trivial action killed by n once it is injective on N: an invariant a ≠ 0 has a nonzero image under some map f : A → N, and α₀ (f a) = α₀ a ∘ f^* by naturality.

The free modules Nᵏ

Bijectivity, by counting

theorem TauCeti.ContCohomology.dualityMap0_bijective_of_smul_eq_self {G : Type uG} [Group G] {N : Type uN} [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [NeZero n] (hN : ∀ (g : G) (y : N), g • y = y) (e : N ≃+ ZMod n) [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace N] [DiscreteTopology N] [ContinuousSMul G N] (e₂ : H2 G N ≃+ ZMod n) (h₀ : Function.Bijective ⇑(dualityMap0 G N N)) (h₁ : Function.Bijective ⇑(dualityMap1 G N N)) (h₂ : Function.Injective ⇑(dualityMap2 G N N)) (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (g : G) (a : A), g • a = a) : Function.Bijective ⇑(dualityMap0 G A N)

Tate's duality map α₀ on a module with trivial action. Let N be a discrete G-module with trivial action, N ≃+ ZMod n and H²(G, N) ≃+ ZMod n, on which α₀, α₁ are bijective and α₂ is injective. Then α₀ : H⁰(G, A) → Hom(H²(G, A'), H²(G, N)) is bijective for every finite discrete G-module A killed by n on which G acts trivially.

theorem TauCeti.ContCohomology.dualityMap1_bijective_of_smul_eq_self {G : Type uG} [Group G] {N : Type uN} [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [NeZero n] (hN : ∀ (g : G) (y : N), g • y = y) (e : N ≃+ ZMod n) [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace N] [DiscreteTopology N] [ContinuousSMul G N] (e₂ : H2 G N ≃+ ZMod n) (h₀ : Function.Bijective ⇑(dualityMap0 G N N)) (h₁ : Function.Bijective ⇑(dualityMap1 G N N)) (h₂ : Function.Injective ⇑(dualityMap2 G N N)) (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (g : G) (a : A), g • a = a) [Finite (H1 G N)] : Function.Bijective ⇑(dualityMap1 G A N)

Tate's duality map α₁ on a module with trivial action. Under the hypotheses of TauCeti.ContCohomology.dualityMap0_bijective_of_smul_eq_self, if moreover H¹(G, N) is finite, then α₁ : H¹(G, A) → Hom(H¹(G, A'), H²(G, N)) is bijective for every finite discrete G-module A killed by n on which G acts trivially.

theorem TauCeti.ContCohomology.dualityMap2_bijective_of_smul_eq_self {G : Type uG} [Group G] {N : Type uN} [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [NeZero n] (hN : ∀ (g : G) (y : N), g • y = y) (e : N ≃+ ZMod n) [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace N] [DiscreteTopology N] [ContinuousSMul G N] (e₂ : H2 G N ≃+ ZMod n) (h₀ : Function.Bijective ⇑(dualityMap0 G N N)) (h₁ : Function.Bijective ⇑(dualityMap1 G N N)) (h₂ : Function.Injective ⇑(dualityMap2 G N N)) (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAtriv : ∀ (g : G) (a : A), g • a = a) : Function.Bijective ⇑(dualityMap2 G A N)

Tate's duality map α₂ on a module with trivial action. Under the hypotheses of TauCeti.ContCohomology.dualityMap0_bijective_of_smul_eq_self, α₂ : H²(G, A) → Hom(H⁰(G, A'), H²(G, N)) is bijective for every finite discrete G-module A killed by n on which G acts trivially.