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.

Equations

• IsCyclotomicExtension.Aut.commGroup K = Function.Injective.commGroup ⇑(IsPrimitiveRoot.autToPow K ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.powerBasis K ⋯) ⋯

@[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 = (IsPrimitiveRoot.autToPow K ⋯).toFun 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.

Equations

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

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 μ.

Equations

• IsCyclotomicExtension.fromZetaAut hμ h = let hζ := ⋯; (MulEquiv.symm (IsCyclotomicExtension.autEquivPow L h)) (ZMod.unitOfCoprime (Exists.choose hζ) ⋯)

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.

Equations

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

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.

Equations

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