Kummer Extensions #
Main result #
isCyclic_tfae
: SupposeL/K
is a finite extension of dimensionn
, andK
contains alln
-th roots of unity. ThenL/K
is cyclic iffL
is a splitting field of some irreducible polynomial of the formXⁿ - a : K[X]
iffL = K[α]
for someαⁿ ∈ K
.autEquivRootsOfUnity
: Given an instanceIsSplittingField K L (X ^ n - C a)
(perhaps viaisSplittingField_X_pow_sub_C_of_root_adjoin_eq_top
), then the galois group is isomorphic torootsOfUnity n K
, by sendingσ ↦ σ α / α
forα ^ n = a
, and the inverse is given byμ ↦ (α ↦ μ • α)
.autEquivZmod
: Furthermore, given an explicit choiceζ
of a primitiven
-th root of unity, the galois group is then isomorphic toMultiplicative (ZMod n)
whose inverse is given byi ↦ (α ↦ ζⁱ • α)
.
Other results #
Criteria for X ^ n - C a
to be irreducible is given:
X_pow_sub_C_irreducible_iff_of_prime
: Forn = p
a prime,X ^ n - C a
is irreducible iffa
is not ap
-power.X_pow_sub_C_irreducible_iff_of_prime_pow
: Forn = p ^ k
an odd prime power,X ^ n - C a
is irreducible iffa
is not ap
-power.X_pow_sub_C_irreducible_iff_forall_prime_of_odd
: Forn
odd,X ^ n - C a
is irreducible iffa
is not ap
-power for all primep ∣ n
.X_pow_sub_C_irreducible_iff_of_odd
: Forn
odd,X ^ n - C a
is irreducible iffa
is not ad
-power ford ∣ n
andd ≠ 1
.
TODO: criteria for even n
. See [Lan02] VI,§9.
Galois Group of K[n√a]
#
We first develop the theory for a specific K[n√a] := AdjoinRoot (X ^ n - C a)
.
The main result is the description of the galois group: autAdjoinRootXPowSubCEquiv
.
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural embedding of the roots of unity of K
into Gal(K[ⁿ√a]/K)
, by sending
η ↦ (ⁿ√a ↦ η • ⁿ√a)
. Also see autAdjoinRootXPowSubC
for the AlgEquiv
version.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural embedding of the roots of unity of K
into Gal(K[ⁿ√a]/K)
, by sending
η ↦ (ⁿ√a ↦ η • ⁿ√a)
. This is an isomorphism when K
contains a primitive root of unity.
See autAdjoinRootXPowSubCEquiv
.
Equations
- autAdjoinRootXPowSubC hn a = (AlgEquiv.algHomUnitsEquiv K (AdjoinRoot (Polynomial.X ^ n - Polynomial.C a))).toMonoidHom.comp (autAdjoinRootXPowSubCHom hn a).toHomUnits
Instances For
The inverse function of autAdjoinRootXPowSubC
if K
has all roots of unity.
See autAdjoinRootXPowSubCEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between the roots of unity of K
and Gal(K[ⁿ√a]/K)
.
Equations
- autAdjoinRootXPowSubCEquiv hζ hn H = { toFun := (↑(autAdjoinRootXPowSubC hn a)).toFun, invFun := AdjoinRootXPowSubCEquivToRootsOfUnity hζ hn H, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
Galois Group of IsSplittingField K L (X ^ n - C a)
#
Suppose L/K
is the splitting field of Xⁿ - a
, then a choice of ⁿ√a
gives an equivalence of
L
with K[n√a]
.
Equations
- adjoinRootXPowSubCEquiv hζ H hα = AlgEquiv.ofBijective (AdjoinRoot.liftHom (Polynomial.X ^ n - Polynomial.C a) α ⋯) ⋯
Instances For
An arbitrary choice of ⁿ√a
in the splitting field of Xⁿ - a
.
Equations
- rootOfSplitsXPowSubC hn a L = Polynomial.rootOfSplits (algebraMap K L) ⋯ ⋯
Instances For
Suppose L/K
is the splitting field of Xⁿ - a
, then Gal(L/K)
is isomorphic to the
roots of unity in K
if K
contains all of them.
Note that this does not depend on a choice of ⁿ√a
.
Equations
- autEquivRootsOfUnity hζ hn H L = (adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ hn H).symm
Instances For
Suppose L/K
is the splitting field of Xⁿ - a
, and ζ
is a n
-th primitive root of unity
in K
, then Gal(L/K)
is isomorphic to ZMod n
.
Equations
- autEquivZmod H L hζ = (autEquivRootsOfUnity ⋯ ⋯ H L).trans ((MulEquiv.subgroupCongr ⋯).trans (AddEquiv.toMultiplicative' ⋯.zmodEquivZPowers.symm))
Instances For
Cyclic extensions of order n
when K
has all n
-th roots of unity. #
If L/K
is a cyclic extension of degree n
, and K
contains all n
-th roots of unity,
then L = K[α]
for some α ^ n ∈ K
.
Suppose L/K
is a finite extension of dimension n
, and K
contains all n
-th roots of unity.
Then L/K
is cyclic iff
L
is a splitting field of some irreducible polynomial of the form Xⁿ - a : K[X]
iff
L = K[α]
for some αⁿ ∈ K
.