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.Aut.commGroup {n : ℕ} [NeZero 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 ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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.

@[simp]

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)) (a✝ : L ≃ₐ[K] L) : (autEquivPow L h) a✝ = (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun a✝

@[simp]

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)