Cyclotomic characters in a rational cyclotomic field

Let K be the n-th cyclotomic field over ℚ and let m ∣ n. Mathlib identifies Gal(K/ℚ) with (ZMod n)ˣ through IsCyclotomicExtension.Rat.galEquivZMod, which records the exponent by which an automorphism acts on every n-th root of unity. A primitive m-th root of unity ζ in K carries its own cyclotomic character IsPrimitiveRoot.autToPow, with values in (ZMod m)ˣ; this file shows that it is the reduction of galEquivZMod modulo m.

Main results

• IsPrimitiveRoot.autToPow_eq_unitsMap_galEquivZMod: the cyclotomic character of a primitive m-th root of unity in the n-th cyclotomic field is galEquivZMod reduced modulo m.
• AlgEquiv.galEquivZMod_restrictNormal: an automorphism of a larger field acting on the n-th roots of unity through u restricts to galEquivZMod.symm u.

theorem IsPrimitiveRoot.autToPow_eq_unitsMap_galEquivZMod {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] {m : ℕ} [NeZero m] {ζ : K} (hζ : IsPrimitiveRoot ζ m) (hmn : m ∣ n) (σ : Gal(K/ℚ)) : (autToPow ℚ hζ) σ = (ZMod.unitsMap hmn) ((IsCyclotomicExtension.Rat.galEquivZMod n K) σ)

The cyclotomic character of a primitive m-th root of unity in the n-th cyclotomic field, for m ∣ n, is the reduction modulo m of galEquivZMod.

theorem AlgEquiv.galEquivZMod_restrictNormal {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] {L : Type u_2} [Field L] [Algebra ℚ L] [Algebra K L] [IsScalarTower ℚ K L] [Normal ℚ K] (τ : Gal(L/ℚ)) (u : (ZMod n)ˣ) (hτ : ∀ (z : L), z ^ n = 1 → τ z = z ^ (↑u).val) : (IsCyclotomicExtension.Rat.galEquivZMod n K) (τ.restrictNormal K) = u

Restricting to the n-th cyclotomic field. If an automorphism τ of an extension L of K raises every n-th root of unity of L to the power u, then galEquivZMod sends its restriction to K to u.