Galois group of cyclotomic extensions #
In this file, we show the relationship between the Galois group ofK(ζₙ) and (zmod n)ˣ;
it is always a subgroup, and if the nth cyclotomic polynomial is irreducible, they are isomorphic.
Main results #
is_cyclotomic_extension.aut_to_pow_injective:is_primitive_root.aut_to_powis injective in the case that it's considered over a cyclotomic field extension, wherendoes not divide the characteristic of K.is_cyclotomic_extension.aut_equiv_pow: If, additionally, thenth cyclotomic polynomial is irreducible in K, thenaut_to_powis amul_equiv(for example, in ℚ and certain 𝔽ₚ).gal_X_pow_equiv_units_zmod,gal_cyclotomic_equiv_units_zmod: Repackageaut_equiv_powin terms ofpolynomial.gal.is_cyclotomic_extension.aut.comm_group: Cyclotomic extensions are abelian.
References #
TODO #
zeta_pow_power_basisis not sufficiently general; the correct solution is somepower_basis.map_conjugate, but figuring out the exact correct assumptions + proof for this is mathematically nontrivial. (Current thoughts: the ideal of polynomials with α as a root is equal to the ideal of polynomials with β as a root, which, in an integrally closed domain, reduces to the usual condition that they are the roots of each others' minimal polynomials.)
theorem
is_primitive_root.aut_to_pow_injective
{n : ℕ+}
(K : Type u_1)
[field K]
{L : Type u_2}
[field L]
{μ : L}
(hμ : is_primitive_root μ ↑n)
[algebra K L]
[is_cyclotomic_extension {n} K L] :
is_primitive_root.aut_to_pow is injective in the case that it's considered over a cyclotomic
field extension, where n does not divide the characteristic of K.
noncomputable
def
is_cyclotomic_extension.aut.comm_group
{n : ℕ+}
(K : Type u_1)
[field K]
{L : Type u_2}
[field L]
[algebra K L]
[is_cyclotomic_extension {n} K L]
[ne_zero ↑↑n] :
comm_group (L ≃ₐ[K] L)
Cyclotomic extensions are abelian.
Equations
- is_cyclotomic_extension.aut.comm_group K = is_cyclotomic_extension.aut.comm_group._match_1 K _
- is_cyclotomic_extension.aut.comm_group._match_1 K _x = function.injective.comm_group ⇑(is_primitive_root.aut_to_pow K _) _ _ _ _ _
@[simp]
theorem
is_cyclotomic_extension.aut_equiv_pow_apply
{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))
[ne_zero ↑↑n]
(ᾰ : L ≃ₐ[K] L) :
⇑(is_cyclotomic_extension.aut_equiv_pow L h) ᾰ = (is_primitive_root.aut_to_pow K _).to_fun ᾰ
@[simp]
theorem
is_cyclotomic_extension.aut_equiv_pow_symm_apply
{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))
[ne_zero ↑↑n]
(t : (zmod ↑n)ˣ) :
noncomputable
def
is_cyclotomic_extension.aut_equiv_pow
{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))
[ne_zero ↑↑n] :
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
- is_cyclotomic_extension.aut_equiv_pow L h = let hn : ne_zero ↑↑n := _, 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' := _}
noncomputable
def
is_cyclotomic_extension.from_zeta_aut
{n : ℕ+}
{K : Type u_1}
[field K]
{L : Type u_2}
[field L]
{μ : L}
(hμ : is_primitive_root μ ↑n)
[algebra K L]
[is_cyclotomic_extension {n} K L]
(h : irreducible (polynomial.cyclotomic ↑n K))
[ne_zero ↑↑n] :
Maps μ to the alg_equiv that sends is_cyclotomic_extension.zeta to μ.
Equations
- is_cyclotomic_extension.from_zeta_aut hμ h = have this : ne_zero ↑↑n, from is_cyclotomic_extension.from_zeta_aut._proof_3, 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 _)
theorem
is_cyclotomic_extension.from_zeta_aut_spec
{n : ℕ+}
{K : Type u_1}
[field K]
{L : Type u_2}
[field L]
{μ : L}
(hμ : is_primitive_root μ ↑n)
[algebra K L]
[is_cyclotomic_extension {n} K L]
(h : irreducible (polynomial.cyclotomic ↑n K))
[ne_zero ↑↑n] :
⇑(is_cyclotomic_extension.from_zeta_aut hμ h) (is_cyclotomic_extension.zeta n K L) = μ
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))
[ne_zero ↑↑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 n does not divide the
characteristic of K, and cyclotomic n K is irreducible in the base field.
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))
[ne_zero ↑↑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 n does not divide the characteristic
of K, and cyclotomic n K is irreducible in the base field.