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 n
th cyclotomic polynomial is irreducible, they are isomorphic.
Main results #
IsPrimitiveRoot.autToPow_injective
:IsPrimitiveRoot.autToPow
is injective in the case that it's considered over a cyclotomic field extension.IsCyclotomicExtension.autEquivPow
: If then
th cyclotomic polynomial is irreducible inK
, thenIsPrimitiveRoot.autToPow
is aMulEquiv
(for example, inβ
and certainπ½β
).galXPowEquivUnitsZMod
,galCyclotomicEquivUnitsZMod
: RepackageIsCyclotomicExtension.autEquivPow
in terms ofPolynomial.Gal
.IsCyclotomicExtension.Aut.commGroup
: 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
PowerBasis.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.)
IsPrimitiveRoot.autToPow
is injective in the case that it's considered over a cyclotomic
field extension.
The MulEquiv
that takes an automorphism f
to the element k : (ZMod n)Λ£
such that
f ΞΌ = ΞΌ ^ k
for any root of unity ΞΌ
. A strengthening of IsPrimitiveRoot.autToPow
.
Instances For
Maps ΞΌ
to the AlgEquiv
that sends IsCyclotomicExtension.zeta
to ΞΌ
.
Instances For
IsCyclotomicExtension.autEquivPow
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.
Instances For
IsCyclotomicExtension.autEquivPow
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.