Documentation

TauCeti.FieldTheory.GaloisCohomology.KummerCoeffProP

Pro-ℓ subgroups of the absolute Galois group fix the ℓ-th roots of unity #

Let K be a field and ℓ a prime invertible in K. The absolute Galois group G_K = Gal(Kˢ/K) acts on the ℓ-th roots of unity μ_ℓ(Kˢ), a group of order ℓ, through the cyclotomic character G_K → (ℤ/ℓ)ˣ. A pro-ℓ subgroup P of G_K has an ℓ-group as image in the group (ℤ/ℓ)ˣ of order ℓ - 1, so P acts trivially on μ_ℓ (TauCeti.smul_kummerCoeff_eq_self_of_isProP). In particular a Sylow pro-ℓ subgroup of G_K fixes μ_ℓ, so μ_ℓ is a trivial coefficient module of order ℓ for it; this is how the ℓ-cohomological dimension of G_K is computed on μ_ℓ.

Main results #

References #

theorem TauCeti.smul_kummerCoeff_eq_self_of_isProP {K : Type u_1} [Field K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) {P : Subgroup (AbsoluteGaloisGroup K)} (hP : IsProP ℓ ↥P) (g : ↥P) (x : KummerCoeff K ℓ) :
g • x = x

A pro-ℓ subgroup of G_K fixes the ℓ-th roots of unity, for a prime ℓ invertible in K: its image under the cyclotomic character G_K → (ℤ/ℓ)ˣ is an ℓ-group in a group of order ℓ - 1, hence trivial.