The cyclotomic orientation of the maximal pro-p Galois group

Let K be a field containing a primitive p-th root of unity ζ. Every σ in the absolute Galois group fixes ζ, and the cyclotomic character reduced modulo p records the exponent j with σ ζ = ζ ^ j. Hence every value of localCyclotomicCharacter p K is a principal unit ≡ 1 mod p, and the image of the character is a pro-p subgroup of ℤ_pˣ. A continuous homomorphism to the profinite pro-p group 1 + pℤ_p kills the pro-p kernel of the absolute Galois group, so the character descends to its maximal pro-p quotient G_K(p).

The descended character cyclotomicOrientation p K hmu : G_K(p) →ₜ* ℤ_pˣ is the arithmetic orientation of G_K(p), the character to compare with the canonical character of G_K(p) when it is a Demushkin group. It is a continuous homomorphism, the form taken by the twisted coefficients ZModTwist and the prescription property HasPrescriptionProperty. It takes the roots-of-unity witness hmu as an explicit argument, and no unconditional descent of the full character is provided: for odd p and K = ℚ_p the character reduced modulo p maps the absolute Galois group onto (ℤ/pℤ)ˣ, a nontrivial group of order prime to p, so it does not factor through any pro-p group.

Main definitions

• TauCeti.cyclotomicOrientation p K hmu: the cyclotomic character descended to absoluteGaloisGroupProP p K.

Main results

• TauCeti.isProP_range_localCyclotomicCharacter: if μ_p ⊆ K, the image of the cyclotomic character is pro-p.
• TauCeti.proPKernel_le_ker_localCyclotomicCharacter: if μ_p ⊆ K, the pro-p kernel of the absolute Galois group lies in the kernel of the cyclotomic character.
• TauCeti.cyclotomicOrientation_mk, TauCeti.cyclotomicOrientation_comp_absoluteGaloisGroupProPQuotientMap, TauCeti.cyclotomicOrientation_range: the orientation agrees with the character on classes, pulls back to the continuous character along the quotient map, and has the same image as the character.

theorem TauCeti.isProP_range_localCyclotomicCharacter (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : IsProP p ↥(localCyclotomicCharacter p K).range

If K contains a primitive p-th root of unity, the image of the cyclotomic character of K is a pro-p subgroup of ℤ_pˣ.

theorem TauCeti.proPKernel_le_ker_localCyclotomicCharacter (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : proPKernel p (Field.absoluteGaloisGroup K) ≤ (localCyclotomicCharacter p K).ker

If K contains a primitive p-th root of unity, the pro-p kernel of the absolute Galois group of K lies in the kernel of the cyclotomic character.

noncomputable def TauCeti.cyclotomicOrientation (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : absoluteGaloisGroupProP p K →ₜ* ℤ_[p]ˣ

The cyclotomic orientation of the maximal pro-p Galois group: when K contains a primitive p-th root of unity, the continuous cyclotomic character continuousLocalCyclotomicCharacter p K descends to a continuous homomorphism on absoluteGaloisGroupProP p K.

Equations

• TauCeti.cyclotomicOrientation p K hmu = TauCeti.ContinuousMonoidHom.quotientLift (TauCeti.proPKernel p (Field.absoluteGaloisGroup K)) (TauCeti.continuousLocalCyclotomicCharacter p K) ⋯

@[simp]

theorem TauCeti.cyclotomicOrientation_mk {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) (g : Field.absoluteGaloisGroup K) : (cyclotomicOrientation p K hmu) ↑g = (localCyclotomicCharacter p K) g

The cyclotomic orientation of the class of g is the cyclotomic character of g.

@[simp]

theorem TauCeti.cyclotomicOrientation_comp_absoluteGaloisGroupProPQuotientMap {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : (cyclotomicOrientation p K hmu).comp (absoluteGaloisGroupProPQuotientMap p K) = continuousLocalCyclotomicCharacter p K

The cyclotomic orientation pulls back to the continuous cyclotomic character along the quotient map from the absolute Galois group to its maximal pro-p quotient.

@[simp]

theorem TauCeti.cyclotomicOrientation_range {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : (↑(cyclotomicOrientation p K hmu)).range = (localCyclotomicCharacter p K).range

The cyclotomic orientation and the cyclotomic character have the same image in ℤ_pˣ, because the quotient map onto the maximal pro-p Galois group is surjective.