Galois group of cyclotomic extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

is_primitive_root.aut_to_pow_injective: is_primitive_root.aut_to_pow is injective in the case that it's considered over a cyclotomic field extension.
is_cyclotomic_extension.aut_equiv_pow: If the nth cyclotomic polynomial is irreducible in K, then is_primitive_root.aut_to_pow is a mul_equiv (for example, in ℚ and certain 𝔽ₚ).
gal_X_pow_equiv_units_zmod, gal_cyclotomic_equiv_units_zmod: Repackage is_cyclotomic_extension.aut_equiv_pow in terms of polynomial.gal.
is_cyclotomic_extension.aut.comm_group: 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 power_basis.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.)

source

theorem is_primitive_root.aut_to_pow_injective {n : ℕ+} (K : Type u_1) [field K] {L : Type u_2} {μ : L} [comm_ring L] [is_domain L] (hμ : is_primitive_root μ ↑n) [algebra K L] [is_cyclotomic_extension {n} K L] :

function.injective ⇑(is_primitive_root.aut_to_pow K hμ)

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

source

noncomputable def is_cyclotomic_extension.aut.comm_group {n : ℕ+} (K : Type u_1) [field K] {L : Type u_2} [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] :

comm_group (L ≃ₐ[K] L)

Cyclotomic extensions are abelian.

Equations

is_cyclotomic_extension.aut.comm_group K = function.injective.comm_group ⇑(is_primitive_root.aut_to_pow K _) _ _ _ _ _ _ _

source

@[simp]

theorem is_cyclotomic_extension.aut_equiv_pow_apply {n : ℕ+} {K : Type u_1} [field K] (L : Type u_2) [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) (ᾰ : L ≃ₐ[K] L) :

⇑(is_cyclotomic_extension.aut_equiv_pow L h) ᾰ = (is_primitive_root.aut_to_pow K _).to_fun ᾰ

source

@[simp]

theorem is_cyclotomic_extension.aut_equiv_pow_symm_apply {n : ℕ+} {K : Type u_1} [field K] (L : Type u_2) [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) (t : (zmod ↑n)ˣ) :

⇑((is_cyclotomic_extension.aut_equiv_pow L h).symm) t = (is_primitive_root.power_basis K _).equiv_of_minpoly (is_primitive_root.power_basis K _) _

source

noncomputable def is_cyclotomic_extension.aut_equiv_pow {n : ℕ+} {K : Type u_1} [field K] (L : Type u_2) [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) :

(L ≃ₐ[K] L) ≃* (zmod ↑n)ˣ

The mul_equiv that takes an automorphism f to the element k : (zmod n)ˣ such that f μ = μ ^ k for any root of unity μ. A strengthening of is_primitive_root.aut_to_pow.

Equations

is_cyclotomic_extension.aut_equiv_pow L h = let hζ : is_primitive_root (is_cyclotomic_extension.zeta n K L) ↑n := _, hμ : ∀ (t : (zmod ↑n)ˣ), is_primitive_root (is_cyclotomic_extension.zeta n K L ^ ↑t.val) ↑n := _ in {to_fun := (is_primitive_root.aut_to_pow K _).to_fun, inv_fun := λ (t : (zmod ↑n)ˣ), (is_primitive_root.power_basis K hζ).equiv_of_minpoly (is_primitive_root.power_basis K _) _, left_inv := _, right_inv := _, map_mul' := _}

source

noncomputable def is_cyclotomic_extension.from_zeta_aut {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} {μ : L} [comm_ring L] [is_domain L] (hμ : is_primitive_root μ ↑n) [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) :

L ≃ₐ[K] L

Maps μ to the alg_equiv that sends is_cyclotomic_extension.zeta to μ.

Equations

is_cyclotomic_extension.from_zeta_aut hμ h = let hζ : ∃ (i : ℕ) (H : i < ↑n), is_cyclotomic_extension.zeta n K L ^ i = μ := _ in ⇑((is_cyclotomic_extension.aut_equiv_pow L h).symm) (zmod.unit_of_coprime hζ.some _)

source

theorem is_cyclotomic_extension.from_zeta_aut_spec {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} {μ : L} [comm_ring L] [is_domain L] (hμ : is_primitive_root μ ↑n) [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) :

⇑(is_cyclotomic_extension.from_zeta_aut hμ h) (is_cyclotomic_extension.zeta n K L) = μ

source

noncomputable def gal_cyclotomic_equiv_units_zmod {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} [field L] [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) :

(polynomial.cyclotomic ↑n K).gal ≃* (zmod ↑n)ˣ

is_cyclotomic_extension.aut_equiv_pow 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

gal_cyclotomic_equiv_units_zmod h = (polynomial.is_splitting_field.alg_equiv L (polynomial.cyclotomic ↑n K)).aut_congr.symm.trans (is_cyclotomic_extension.aut_equiv_pow L h)

source

noncomputable def gal_X_pow_equiv_units_zmod {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} [field L] [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic ↑n K)) :

(polynomial.X ^ ↑n - 1).gal ≃* (zmod ↑n)ˣ

is_cyclotomic_extension.aut_equiv_pow 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

gal_X_pow_equiv_units_zmod h = (polynomial.is_splitting_field.alg_equiv L (polynomial.X ^ ↑n - 1)).aut_congr.symm.trans (is_cyclotomic_extension.aut_equiv_pow L h)