mathlib3 documentation

number_theory.cyclotomic.gal

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 #

References #

TODO #

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} [comm_ring L] [is_domain L] [algebra K L] [is_cyclotomic_extension {n} K L] :

Cyclotomic extensions are abelian.

Equations
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)) :

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
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)) :

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

Equations
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)) :

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] [algebra K L] [is_cyclotomic_extension {n} K L] (h : irreducible (polynomial.cyclotomic n K)) :

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