Documentation

Mathlib.FieldTheory.KummerExtension

Kummer Extensions #

Main result #

Other results #

Criteria for X ^ n - C a to be irreducible is given:

TODO: criteria for even n. See [Lan02] VI,§9.

theorem X_pow_sub_C_eq_prod {R : Type u_1} [CommRing R] [IsDomain R] {n : Nat} {ζ : R} ( : IsPrimitiveRoot ζ n) {α a : R} (hn : LT.lt 0 n) (e : Eq (HPow.hPow α n) a) :
theorem X_pow_sub_C_irreducible_of_odd {K : Type u} [Field K] {n : Nat} (hn : Odd n) {a : K} (ha : ∀ (p : Nat), Nat.Prime pDvd.dvd p n∀ (b : K), Ne (HPow.hPow b p) a) :
theorem X_pow_sub_C_irreducible_iff_forall_prime_of_odd {K : Type u} [Field K] {n : Nat} (hn : Odd n) {a : K} :
Iff (Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (∀ (p : Nat), Nat.Prime pDvd.dvd p n∀ (b : K), Ne (HPow.hPow b p) a)
theorem X_pow_sub_C_irreducible_iff_of_odd {K : Type u} [Field K] {n : Nat} (hn : Odd n) {a : K} :
Iff (Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (∀ (d : Nat), Dvd.dvd d nNe d 1∀ (b : K), Ne (HPow.hPow b d) a)
theorem X_pow_sub_C_irreducible_of_prime_pow {K : Type u} [Field K] {p : Nat} (hp : Nat.Prime p) (hp' : Ne p 2) (n : Nat) {a : K} (ha : ∀ (b : K), Ne (HPow.hPow b p) a) :
theorem X_pow_sub_C_irreducible_iff_of_prime_pow {K : Type u} [Field K] {p : Nat} (hp : Nat.Prime p) (hp' : Ne p 2) {n : Nat} (hn : Ne n 0) {a : K} :

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
        • One or more equations did not get rendered due to their size.
        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
            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
              Instances For
                @[reducible, inline]
                noncomputable abbrev rootOfSplitsXPowSubC {K : Type u} [Field K] {n : Nat} (hn : LT.lt 0 n) (a : K) (L : Type u_2) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))] :
                L

                An arbitrary choice of ⁿ√a in the splitting field of Xⁿ - a.

                Equations
                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
                  Instances For
                    noncomputable def autEquivZmod {K : Type u} [Field K] {n : Nat} {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))] [NeZero n] {ζ : K} ( : IsPrimitiveRoot ζ n) :

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