# 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 the`n`

th cyclotomic polynomial is irreducible in`K`

, then`IsPrimitiveRoot.autToPow`

is a`MulEquiv`

(for example, in`ℚ`

and certain`𝔽ₚ`

).`galXPowEquivUnitsZMod`

,`galCyclotomicEquivUnitsZMod`

: Repackage`IsCyclotomicExtension.autEquivPow`

in terms of`Polynomial.Gal`

.`IsCyclotomicExtension.Aut.commGroup`

: Cyclotomic extensions are abelian.

## References #

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

Cyclotomic extensions are abelian.

## Equations

- IsCyclotomicExtension.Aut.commGroup K = Function.Injective.commGroup ⇑(IsPrimitiveRoot.autToPow K ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

## Instances For

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`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Maps `μ`

to the `AlgEquiv`

that sends `IsCyclotomicExtension.zeta`

to `μ`

.

## Equations

- IsCyclotomicExtension.fromZetaAut hμ h = (IsCyclotomicExtension.autEquivPow L h).symm (ZMod.unitOfCoprime ⋯.choose ⋯)

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

## Equations

- galCyclotomicEquivUnitsZMod h = (Polynomial.IsSplittingField.algEquiv L (Polynomial.cyclotomic (↑n) K)).autCongr.symm.trans (IsCyclotomicExtension.autEquivPow L h)

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

## Equations

- galXPowEquivUnitsZMod h = (Polynomial.IsSplittingField.algEquiv L (Polynomial.X ^ ↑n - 1)).autCongr.symm.trans (IsCyclotomicExtension.autEquivPow L h)