# mathlibdocumentation

number_theory.cyclotomic.gal

# 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 #

• 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 aut_to_pow is a mul_equiv (for example, in ℚ and certain 𝔽ₚ).
• gal_X_pow_equiv_units_zmod, gal_cyclotomic_equiv_units_zmod: Repackage aut_equiv_pow in terms of polynomial.gal.
• is_cyclotomic_extension.aut.comm_group: Cyclotomic extensions are abelian.

## 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.)
theorem is_primitive_root.aut_to_pow_injective {n : ℕ+} (K : Type u_1) [field K] {L : Type u_2} [field L] {μ : L} (hμ : n) [ L] [ L] :

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

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

Cyclotomic extensions are abelian.

Equations
@[simp]
theorem is_cyclotomic_extension.aut_equiv_pow_apply {n : ℕ+} {K : Type u_1} [field K] (L : Type u_2) [field L] [ L] [ L] (h : irreducible ) (ᾰ : L ≃ₐ[K] L) :
@[simp]
theorem is_cyclotomic_extension.aut_equiv_pow_symm_apply {n : ℕ+} {K : Type u_1} [field K] (L : Type u_2) [field L] [ L] [ L] (h : irreducible ) (t : (zmod n)ˣ) :
noncomputable def is_cyclotomic_extension.aut_equiv_pow {n : ℕ+} {K : Type u_1} [field K] (L : Type u_2) [field L] [ L] [ L] (h : irreducible ) :

The mul_equiv that takes an automorphism f to the element k : (zmod n)ˣ such that f μ = μ ^ k. A stronger version of is_primitive_root.aut_to_pow.

Equations
noncomputable def is_cyclotomic_extension.from_zeta_aut {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} [field L] {μ : L} (hμ : n) [ L] [ L] (h : irreducible ) :

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

Equations
• = let hζ : ∃ (i : ) (H : i < n), = μ := _ in _)
theorem is_cyclotomic_extension.from_zeta_aut_spec {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} [field L] {μ : L} (hμ : n) [ L] [ L] (h : irreducible ) :
= μ
noncomputable def gal_cyclotomic_equiv_units_zmod {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} [field L] [ L] [ L] (h : irreducible ) :

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
noncomputable def gal_X_pow_equiv_units_zmod {n : ℕ+} {K : Type u_1} [field K] {L : Type u_2} [field L] [ L] [ L] (h : irreducible ) :

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