Galois group of cyclotomic extensions

In this file, we show the relationship between the Galois group of K(ζₙ) and (ZMod n)ˣ; it is always a subgroup, and if the nth cyclotomic polynomial is irreducible, they are isomorphic.

Main results

• IsPrimitiveRoot.autToPow_injective: IsPrimitiveRoot.autToPow is injective in the case that it's considered over a cyclotomic field extension.
• IsCyclotomicExtension.autEquivPow: If the nth cyclotomic polynomial is irreducible in K, then IsPrimitiveRoot.autToPow is a MulEquiv (for example, in ℚ and certain 𝔽ₚ).
• galXPowEquivUnitsZMod, galCyclotomicEquivUnitsZMod: Repackage IsCyclotomicExtension.autEquivPow in terms of Polynomial.Gal.
• IsCyclotomicExtension.Aut.commGroup: Cyclotomic extensions are abelian.

References

• https://kconrad.math.uconn.edu/blurbs/galoistheory/cyclotomic.pdf

TODO

• We currently can get away with the fact that the power of a primitive root is a primitive root, but the correct long-term solution for computing other explicit Galois groups is creating PowerBasis.map_conjugate; but figuring out the exact correct assumptions + proof for this is mathematically nontrivial. (Current thoughts: the correct condition is that the annihilating ideal of both elements is equal. This may not hold in an ID, and definitely holds in an ICD.)

theorem IsPrimitiveRoot.autToPow_injective {n : ℕ} [NeZero n] (K : Type u_1) [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] : Function.Injective ⇑(autToPow K hμ)

IsPrimitiveRoot.autToPow is injective in the case that it's considered over a cyclotomic field extension.

noncomputable def IsCyclotomicExtension.autEquivPow {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (L ≃ₐ[K] L) ≃* (ZMod n)ˣ

The MulEquiv that takes an automorphism f to the element k : (ZMod n)ˣ such that f μ = μ ^ k for any root of unity μ. A strengthening of IsPrimitiveRoot.autToPow.

Equations

• One or more equations did not get rendered due to their size.

theorem IsCyclotomicExtension.autEquivPow_apply {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (f : L ≃ₐ[K] L) : (autEquivPow L h) f = (IsPrimitiveRoot.autToPow K ⋯) f

theorem IsCyclotomicExtension.autEquivPow_spec {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (f : L ≃ₐ[K] L) : f (zeta n K L) = zeta n K L ^ (↑((autEquivPow L h) f)).val

theorem IsCyclotomicExtension.autEquivPow_apply_of_pow_eq_one {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (f : L ≃ₐ[K] L) {x : L} (hx : x ^ n = 1) : f x = x ^ (↑((autEquivPow L h) f)).val

theorem IsCyclotomicExtension.autEquivPow_symm_apply_zeta {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (t : (ZMod n)ˣ) : ((autEquivPow L h).symm t) (zeta n K L) = zeta n K L ^ (↑t).val

@[deprecated IsCyclotomicExtension.autEquivPow_symm_apply_zeta (since := "2026-10-19")]

theorem IsCyclotomicExtension.autEquivPow_symm_apply {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (t : (ZMod n)ˣ) : (autEquivPow L h).symm t = (IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯

noncomputable def IsCyclotomicExtension.fromZetaAut {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : L ≃ₐ[K] L

Maps μ to the AlgEquiv that sends IsCyclotomicExtension.zeta to μ.

Equations

• IsCyclotomicExtension.fromZetaAut hμ h = (IsCyclotomicExtension.autEquivPow L h).symm (ZMod.unitOfCoprime ⋯.choose ⋯)

theorem IsCyclotomicExtension.fromZetaAut_spec {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (fromZetaAut hμ h) (zeta n K L) = μ

noncomputable def galCyclotomicEquivUnitsZMod {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (Polynomial.cyclotomic n K).Gal ≃* (ZMod n)ˣ

IsCyclotomicExtension.autEquivPow repackaged in terms of Gal. Asserts that the Galois group of cyclotomic n K is equivalent to (ZMod n)ˣ if cyclotomic n K is irreducible in the base field.

Equations

• galCyclotomicEquivUnitsZMod h = (Polynomial.IsSplittingField.algEquiv L (Polynomial.cyclotomic n K)).autCongr.symm.trans (IsCyclotomicExtension.autEquivPow L h)

noncomputable def galXPowEquivUnitsZMod {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (Polynomial.X ^ n - 1).Gal ≃* (ZMod n)ˣ

IsCyclotomicExtension.autEquivPow repackaged in terms of Gal. Asserts that the Galois group of X ^ n - 1 is equivalent to (ZMod n)ˣ if cyclotomic n K is irreducible in the base field.

Equations

• galXPowEquivUnitsZMod h = (Polynomial.IsSplittingField.algEquiv L (Polynomial.X ^ n - 1)).autCongr.symm.trans (IsCyclotomicExtension.autEquivPow L h)