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 : ℕ+} (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 ↑(IsPrimitiveRoot.autToPow K hμ)

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

noncomputable def IsCyclotomicExtension.Aut.commGroup {n : ℕ+} (K : Type u_1) [Field K] {L : Type u_2} [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] : CommGroup (L ≃ₐ[K] L)

Cyclotomic extensions are abelian.

@[simp]

theorem IsCyclotomicExtension.autEquivPow_symm_apply {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)ˣ) : ↑(MulEquiv.symm (IsCyclotomicExtension.autEquivPow L h)) t = PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (IsCyclotomicExtension.zeta n K L) ↑n)) (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (IsCyclotomicExtension.zeta n K L ^ ZMod.val ↑t) ↑n)) (_ : minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (IsCyclotomicExtension.zeta n K L) ↑n)).gen = minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (IsCyclotomicExtension.zeta n K L ^ ZMod.val ↑t) ↑n)).gen)

@[simp]

theorem IsCyclotomicExtension.autEquivPow_apply {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)) : ∀ (a : L ≃ₐ[K] L), ↑(IsCyclotomicExtension.autEquivPow L h) a = OneHom.toFun (↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (IsCyclotomicExtension.zeta n K L) ↑n))) a

noncomputable def IsCyclotomicExtension.autEquivPow {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.

noncomputable def IsCyclotomicExtension.fromZetaAut {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 μ.

theorem IsCyclotomicExtension.fromZetaAut_spec {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)) : ↑(IsCyclotomicExtension.fromZetaAut hμ h) (IsCyclotomicExtension.zeta n K L) = μ

noncomputable def galCyclotomicEquivUnitsZMod {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.Gal (Polynomial.cyclotomic (↑n) K) ≃* (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.

noncomputable def galXPowEquivUnitsZMod {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.Gal (Polynomial.X ^ ↑n - 1) ≃* (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.