The cyclotomic character of an absolute Galois group

The character localCyclotomicCharacter p K records the action of Field.absoluteGaloisGroup K on roots of unity of p-power order in an algebraic closure. It is Mathlib's cyclotomic character restricted from ring automorphisms to the Galois group. The pointwise equation fixes this choice of character for later arithmetic comparisons. Its bundled form continuousLocalCyclotomicCharacter p K is the continuous homomorphism that the twisted coefficients TauCeti.ZModTwist and the prescription property TauCeti.HasPrescriptionProperty take. It factors through the topological abelianization as abelianizedLocalCyclotomicCharacter p K, which is how it is evaluated on Artin symbols.

noncomputable def TauCeti.localCyclotomicCharacter (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] : Field.absoluteGaloisGroup K →* ℤ_[p]ˣ

The p-adic cyclotomic character on the absolute Galois group of K.

Equations

• TauCeti.localCyclotomicCharacter p K = (cyclotomicCharacter (AlgebraicClosure K) p).comp (MulSemiringAction.toRingAut Gal(AlgebraicClosure K/K) (AlgebraicClosure K))

@[simp]

theorem TauCeti.localCyclotomicCharacter_apply (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (σ : Field.absoluteGaloisGroup K) : (localCyclotomicCharacter p K) σ = (cyclotomicCharacter (AlgebraicClosure K) p) σ.toRingEquiv

The local character is Mathlib's cyclotomic character evaluated on the underlying ring automorphism.

theorem TauCeti.localCyclotomicCharacter_continuous (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] : Continuous ⇑(localCyclotomicCharacter p K)

The cyclotomic character is continuous for the Krull topology on the absolute Galois group and the p-adic topology on the units.

noncomputable def TauCeti.continuousLocalCyclotomicCharacter (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] : Field.absoluteGaloisGroup K →ₜ* ℤ_[p]ˣ

The p-adic cyclotomic character on the absolute Galois group of K, as a continuous homomorphism.

Equations

• TauCeti.continuousLocalCyclotomicCharacter p K = { toMonoidHom := TauCeti.localCyclotomicCharacter p K, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.continuousLocalCyclotomicCharacter_apply (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (σ : Field.absoluteGaloisGroup K) : (continuousLocalCyclotomicCharacter p K) σ = (localCyclotomicCharacter p K) σ

The bundled continuous character takes the values of the cyclotomic character.

noncomputable def TauCeti.abelianizedLocalCyclotomicCharacter (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] : Field.absoluteGaloisGroupAbelianization K →ₜ* ℤ_[p]ˣ

The p-adic cyclotomic character on the topological abelianization of the absolute Galois group of K, through which the cyclotomic character factors since ℤ_[p]ˣ is commutative.

Equations

• TauCeti.abelianizedLocalCyclotomicCharacter p K = TopologicalAbelianization.lift (TauCeti.continuousLocalCyclotomicCharacter p K)

@[simp]

theorem TauCeti.abelianizedLocalCyclotomicCharacter_mk (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (σ : Field.absoluteGaloisGroup K) : (abelianizedLocalCyclotomicCharacter p K) ↑σ = (localCyclotomicCharacter p K) σ

On the class of σ, the abelianized cyclotomic character is the cyclotomic character of σ.