μₙ as a finite discrete G_ℚ₂-module

The literature axioms B6 (local Tate duality) and B7 (local Euler characteristic) are stated for finite discrete G_ℚ₂-modules, and B6 uses μₙ (the group of n-th roots of unity, as the dualizing object). This file makes μₙ ⊆ ℚ̄₂ such a module, i.e. a legal coefficient for GQ2.ContCoh over AbsGalQ2 = Field.absoluteGaloisGroup ℚ_[2].

What is built

Mathlib has rootsOfUnity n L : Subgroup Lˣ and the tautological Galois action on Lˣ (via AlgEquiv.smul_units_def), but not the induced action on rootsOfUnity, nor its additive/discrete/continuous packaging (the cyclotomic-character development works pointwise, via g (ζ : Lˣ) = ζ ^ m). We supply, for any field extension L / K:

• GQ2.galRootsOfUnity : MulDistribMulAction (L ≃ₐ[K] L) (rootsOfUnity n L) — the Galois action, by restriction of the units action (μₙ is stable since (g • ζ)ⁿ = g • ζⁿ = g • 1 = 1);
• GQ2.galRootsOfUnityAdd : DistribMulAction (L ≃ₐ[K] L) (Additive (rootsOfUnity n L)) — the same action written additively, the project's discrete-G-module convention;

and then, over ℚ₂:

• GQ2.MuN n := Additive (rootsOfUnity n ℚ̄₂), which carries the finite discrete topology it inherits as a subspace of the valued field ℚ̄₂ (Finite.instDiscreteTopology: a finite subset of a T₁ space is discrete), with DistribMulAction AbsGalQ2 (MuN n) and ContinuousSMul AbsGalQ2 (MuN n) — the latter from the Krull-open stabilizers (continuousSMul_iff_stabilizer_isOpen + stabilizer_isOpen_of_isIntegral).

Conventions / citations

• The additive convention matches GQ2/DiscreteModule.lean (the discrete-module conventions) and GQ2/Cohomology.lean (the continuous-cohomology API): a discrete G-module is [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M]. μₙ is naturally multiplicative, so we transport it through Additive.
• Continuity of the Galois action on μₙ is the classical fact that each ζ ∈ μₙ lies in a finite (cyclotomic) subextension, hence has open stabilizer in the Krull topology. Cf. Neukirch–Schmidt– Wingberg, Cohomology of Number Fields, and Serre, Galois Cohomology I §1–2 (discrete modules).

The stress tests at the bottom confirm the result: H⁰/H¹/H²(G_ℚ₂, μₙ) all typecheck — μₙ is a legal ContCoh coefficient — and μₙ is finite. #print axioms of every proof = the standard three.

The Galois action on μₙ (pure algebra, any field extension)

@[implicit_reducible]

instance GQ2.galRootsOfUnity {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (n : ℕ) : MulDistribMulAction Gal(L/K) ↥(rootsOfUnity n L)

The Galois action on μₙ(L) = rootsOfUnity n L. Gal(L/K) acts by restricting its tautological action on Lˣ; μₙ is a stable subgroup because a field automorphism preserves ζⁿ = 1 ((g • ζ)ⁿ = g • ζⁿ = g • 1 = 1).

Equations

• GQ2.galRootsOfUnity n = { smul := fun (g : Gal(L/K)) (ζ : ↥(rootsOfUnity n L)) => ⟨g • ↑ζ, ⋯⟩, mul_smul := ⋯, one_smul := ⋯, smul_one := ⋯, smul_mul := ⋯ }

@[implicit_reducible]

instance GQ2.galRootsOfUnityAdd {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (n : ℕ) : DistribMulAction Gal(L/K) (Additive ↥(rootsOfUnity n L))

μₙ as an additive Gal(L/K)-module. The project's cohomology takes additive modules; Additive turns the multiplicative Galois action into a DistribMulAction. All laws reduce definitionally to the multiplicative ones (Additive's +/0 are μₙ's */1).

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.val_smul_units {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (g : Gal(L/K)) (u : Lˣ) : ↑(g • u) = g • ↑u

The units action and the field action agree under the coercion Lˣ → L.

theorem GQ2.stabilizer_additive_eq_field {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (n : ℕ) (x : Additive ↥(rootsOfUnity n L)) : MulAction.stabilizer Gal(L/K) x = MulAction.stabilizer Gal(L/K) ↑↑(Additive.toMul x)

The stabilizer bridge. The stabilizer of x : Additive (μₙ) in Gal(L/K) coincides with the stabilizer of the underlying field element ↑↑x.toMul : L — the reduction that lets us reuse the Krull-topology openness lemma stabilizer_isOpen_of_isIntegral.

μₙ(ℚ̄₂) as a finite discrete G_ℚ₂-module

@[reducible, inline]

abbrev GQ2.MuN (n : ℕ) : Type

μₙ over ℚ₂, the group of n-th roots of unity in a fixed algebraic closure of ℚ₂, written additively: a finite discrete G_ℚ₂-module. It carries the subspace topology from the valued field ℚ̄₂, which is discrete because μₙ is finite and ℚ̄₂ is T₁.

Equations

• GQ2.MuN n = Additive ↥(rootsOfUnity n (AlgebraicClosure ℚ_[2]))

@[implicit_reducible]

noncomputable instance GQ2.instMulDistribMulActionAbsGalQ2SubtypeUnitsAlgebraicClosurePadicOfNatNatMemSubgroupRootsOfUnity (n : ℕ) : MulDistribMulAction AbsGalQ2 ↥(rootsOfUnity n (AlgebraicClosure ℚ_[2]))

The Galois action of G_ℚ₂ on μₙ, transported along AbsGalQ2 = (ℚ̄₂ ≃ₐ[ℚ₂] ℚ̄₂) (definitional).

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance GQ2.instDistribMulActionAbsGalQ2MuN (n : ℕ) : DistribMulAction AbsGalQ2 (MuN n)

The additive Galois action of G_ℚ₂ on μₙ.

Equations

• GQ2.instDistribMulActionAbsGalQ2MuN n = { smul := GQ2.instDistribMulActionAbsGalQ2MuN._aux_1 n, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance GQ2.continuousSMul_gal (n : ℕ) [NeZero n] : ContinuousSMul Gal(AlgebraicClosure ℚ_[2]/ℚ_[2]) (MuN n)

Continuity of the Galois action on μₙ (Krull topology): the stabilizer of each x : μₙ is the stabilizer of an algebraic (hence open-stabilized) field element.

instance GQ2.instContinuousSMulAbsGalQ2MuN (n : ℕ) [NeZero n] : ContinuousSMul AbsGalQ2 (MuN n)

ContinuousSMul over G_ℚ₂, transported.

Stress tests (acceptance)