Documentation

TauCeti.FieldTheory.Galois.AbsoluteGaloisGroup.Cyclotomic.Prescription

The prescription property of the cyclotomic character #

Let K be a field in which the prime p is invertible and χ = χ_cyc the p-adic cyclotomic character of its absolute Galois group G_K. This file proves that χ has Labute's prescription property: every reduction H¹(G_K, I(χ)/pⁱ) → H¹(G_K, I(χ)/p) of the twisted coefficients is surjective. When K contains a primitive p-th root of unity, the same holds for the cyclotomic orientation of the maximal pro-p Galois group G_K(p), the character through which χ factors. The proof is Kummer theory, with no input from local duality or reciprocity.

A primitive pʲ-th root of unity ζ of the separable closure identifies I(χ)/pʲ with the roots of unity μ_{pʲ}, by x ↦ ζ ^ x. This is equivariant because G_K acts on μ_{pʲ} through χ modulo pʲ (TauCeti.smul_kummerCoeff_eq_nsmul_localCyclotomicCharacter), which is how χ is defined. If the root used at level j ≤ i is the p ^ (i - j)-th power of the root used at level i, the reduction I(χ)/pⁱ → I(χ)/pʲ becomes the power map μ_{pⁱ} → μ_{pʲ}. On Kummer classes that power map only changes the level, so it is surjective on H¹ because every class at level pʲ is a Kummer class (TauCeti.explicitCoeff1_kummerCoeffPow_surjective).

The prescription property is the hypothesis under which a character of a Demushkin group is its canonical character. It descends from G_K to the maximal pro-p quotient G_K(p) (TauCeti.hasPrescriptionProperty_comp_quotientMk_proPKernel_iff), because twisted inflation along G_K → G_K(p) is bijective and compatible with the reductions. The cyclotomic orientation pulls back to χ along this map, so it has the property as well.

Main definitions #

Main results #

References #

source
theorem TauCeti.smul_kummerCoeff_eq_nsmul_localCyclotomicCharacter {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NeZero ↑p] {j : ℕ} (τ : AbsoluteGaloisGroup K) (x : KummerCoeff K (p ^ j)) :
τ • x = ((PadicInt.toZModPow j) ↑((localCyclotomicCharacter p K) ((absoluteGaloisGroupRestrictEquiv K).symm τ))).val • x

The Galois action on μ_{pʲ} is the cyclotomic character modulo pʲ: an element τ of Gal(Kˢ/K) raises every pʲ-th root of unity of Kˢ to the power χ(τ) mod pʲ, where χ is read on τ through the comparison with Field.absoluteGaloisGroup K.

source
noncomputable def TauCeti.zModTwistEquivKummerCoeff (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] {j : ℕ} {ζ : (SeparableClosure K)ˣ} (hζ : IsPrimitiveRoot ζ (p ^ j)) :
ZModTwist (continuousLocalCyclotomicCharacter p K) j ≃+ KummerCoeff K (p ^ j)

The identification I(χ_cyc)/pʲ ≃ μ_{pʲ} of a primitive pʲ-th root of unity ζ of Kˢ: the residue class of x goes to ζ ^ x. It is equivariant for the comparison of Field.absoluteGaloisGroup K with Gal(Kˢ/K) (TauCeti.zModTwistEquivKummerCoeff_smul).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.coe_toMul_zModTwistEquivKummerCoeff {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] {j : ℕ} {ζ : (SeparableClosure K)ˣ} (hζ : IsPrimitiveRoot ζ (p ^ j)) (x : ZModTwist (continuousLocalCyclotomicCharacter p K) j) :
    ↑(Additive.toMul ((zModTwistEquivKummerCoeff p K hζ) x)) = ζ ^ x.val.val

    The identification I(χ_cyc)/pʲ ≃ μ_{pʲ} sends the residue class of x to ζ ^ x.

    source
    @[simp]
    theorem TauCeti.zModTwistEquivKummerCoeff_smul {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NeZero ↑p] {j : ℕ} {ζ : (SeparableClosure K)ˣ} (hζ : IsPrimitiveRoot ζ (p ^ j)) (τ : AbsoluteGaloisGroup K) (x : ZModTwist (continuousLocalCyclotomicCharacter p K) j) :
    (zModTwistEquivKummerCoeff p K hζ) ((absoluteGaloisGroupRestrictEquiv K).symm τ • x) = τ • (zModTwistEquivKummerCoeff p K hζ) x

    The identification I(χ_cyc)/pʲ ≃ μ_{pʲ} is equivariant: the action of σ on the twisted module, multiplication by χ(σ) mod pʲ, corresponds to the action of the restriction of σ to Kˢ on the roots of unity.

    source
    theorem TauCeti.kummerCoeffPow_zModTwistEquivKummerCoeff {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] {i j : ℕ} (h : j ≤ i) {ζ : (SeparableClosure K)ˣ} (hζ : IsPrimitiveRoot ζ (p ^ i)) (x : ZModTwist (continuousLocalCyclotomicCharacter p K) i) :
    (kummerCoeffPow K ⋯) ((zModTwistEquivKummerCoeff p K hζ) x) = (zModTwistEquivKummerCoeff p K ⋯) ((ZModTwist.reduce (continuousLocalCyclotomicCharacter p K) h) x)

    The identifications turn reductions into power maps: if the root used at level j ≤ i is the pⁱ / pʲ-th power of the root ζ used at level i, the reduction I(χ_cyc)/pⁱ → I(χ_cyc)/pʲ corresponds to the power map μ_{pⁱ} → μ_{pʲ}.

    source
    theorem TauCeti.continuousLocalCyclotomicCharacter_hasPrescriptionProperty (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NeZero ↑p] :
    HasPrescriptionProperty (continuousLocalCyclotomicCharacter p K)

    The cyclotomic character has the prescription property: for a field K in which p is invertible, every reduction H¹(G_K, I(χ_cyc)/pⁱ) → H¹(G_K, I(χ_cyc)/p) is surjective. Through a compatible choice of primitive roots of unity the reduction is the power map H¹(G_K, μ_{pⁱ}) → H¹(G_K, μ_p), which is onto because every class at level p is the Kummer class of a unit of K, and so the image of the Kummer class of that unit at level pⁱ.

    source
    theorem TauCeti.cyclotomicOrientation_hasPrescriptionProperty (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) :
    HasPrescriptionProperty (cyclotomicOrientation p K hmu)

    The cyclotomic orientation has the prescription property: if K contains a primitive p-th root of unity, then for the cyclotomic orientation χ of the maximal pro-p Galois group G_K(p), every reduction H¹(G_K(p), I(χ)/pⁱ) → H¹(G_K(p), I(χ)/p) is surjective. The orientation pulls back to the cyclotomic character of G_K, which has the property, and the property descends along G_K → G_K(p).