Documentation

Mathlib.NumberTheory.Cyclotomic.Gal

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 nth cyclotomic polynomial is irreducible, they are isomorphic.

Main results #

References #

TODO #

theorem IsPrimitiveRoot.autToPow_injective {n : ℕ+} (K : Type u_1) [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] :

IsPrimitiveRoot.autToPow is injective in the case that it's considered over a cyclotomic field extension.

noncomputable def IsCyclotomicExtension.Aut.commGroup {n : ℕ+} (K : Type u_1) [Field K] {L : Type u_2} [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] :

Cyclotomic extensions are abelian.

Equations
Instances For
    @[simp]
    theorem IsCyclotomicExtension.autEquivPow_apply {n : ℕ+} {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic (↑n) K)) :
    ∀ (a : L ≃ₐ[K] L), (IsCyclotomicExtension.autEquivPow L h) a = (↑(IsPrimitiveRoot.autToPow K )).toFun a
    @[simp]
    theorem IsCyclotomicExtension.autEquivPow_symm_apply {n : ℕ+} {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic (↑n) K)) (t : (ZMod n)ˣ) :
    noncomputable def IsCyclotomicExtension.autEquivPow {n : ℕ+} {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic (↑n) K)) :
    (L ≃ₐ[K] L) ≃* (ZMod n)ˣ

    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
      noncomputable def IsCyclotomicExtension.fromZetaAut {n : ℕ+} {K : Type u_1} [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic (↑n) K)) :

      Maps μ to the AlgEquiv that sends IsCyclotomicExtension.zeta to μ.

      Equations
      Instances For
        noncomputable def galCyclotomicEquivUnitsZMod {n : ℕ+} {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic (↑n) K)) :
        (Polynomial.cyclotomic (↑n) K).Gal ≃* (ZMod n)ˣ

        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
        Instances For
          noncomputable def galXPowEquivUnitsZMod {n : ℕ+} {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic (↑n) K)) :
          (Polynomial.X ^ n - 1).Gal ≃* (ZMod n)ˣ

          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
          Instances For