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 root_X_pow_sub_C_pow {K : Type u} [Field K] (n : ) (a : K) :
AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ^ n = (AdjoinRoot.of (Polynomial.X ^ n - Polynomial.C a)) a
theorem root_X_pow_sub_C_ne_zero {K : Type u} [Field K] {n : } (hn : 1 < n) (a : K) :
AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) 0
theorem root_X_pow_sub_C_ne_zero' {K : Type u} [Field K] {n : } {a : K} (hn : 0 < n) (ha : a 0) :
AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) 0
theorem X_pow_sub_C_splits_of_isPrimitiveRoot {K : Type u} [Field K] {n : } {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α : K} {a : K} (e : α ^ n = a) :
Polynomial.Splits (RingHom.id K) (Polynomial.X ^ n - Polynomial.C a)
theorem X_pow_sub_C_eq_prod {R : Type u_1} [CommRing R] [IsDomain R] {n : } {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α : R} {a : R} (hn : 0 < n) (e : α ^ n = a) :
Polynomial.X ^ n - Polynomial.C a = iFinset.range n, (Polynomial.X - Polynomial.C (ζ ^ i * α))
theorem ne_zero_of_irreducible_X_pow_sub_C {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
n 0
theorem ne_zero_of_irreducible_X_pow_sub_C' {K : Type u} [Field K] {n : } (hn : n 1) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
a 0
theorem root_X_pow_sub_C_eq_zero_iff {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) = 0 a = 0
theorem root_X_pow_sub_C_ne_zero_iff {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) 0 a 0
theorem pow_ne_of_irreducible_X_pow_sub_C {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {m : } (hm : m n) (hm' : m 1) (b : K) :
b ^ m a
theorem X_pow_sub_C_irreducible_of_prime {K : Type u} [Field K] {p : } (hp : Nat.Prime p) {a : K} (ha : ∀ (b : K), b ^ p a) :
Irreducible (Polynomial.X ^ p - Polynomial.C a)
theorem X_pow_sub_C_irreducible_iff_of_prime {K : Type u} [Field K] {p : } (hp : Nat.Prime p) {a : K} :
Irreducible (Polynomial.X ^ p - Polynomial.C a) ∀ (b : K), b ^ p a
theorem X_pow_mul_sub_C_irreducible {K : Type u} [Field K] {n : } {m : } {a : K} (hm : Irreducible (Polynomial.X ^ m - Polynomial.C a)) (hn : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = Polynomial.X ^ m - Polynomial.C aIrreducible (Polynomial.X ^ n - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) :
Irreducible (Polynomial.X ^ (n * m) - Polynomial.C a)
theorem X_pow_sub_C_irreducible_of_odd {K : Type u} [Field K] {n : } (hn : Odd n) {a : K} (ha : ∀ (p : ), Nat.Prime pp n∀ (b : K), b ^ p a) :
Irreducible (Polynomial.X ^ n - Polynomial.C a)
theorem X_pow_sub_C_irreducible_iff_forall_prime_of_odd {K : Type u} [Field K] {n : } (hn : Odd n) {a : K} :
Irreducible (Polynomial.X ^ n - Polynomial.C a) ∀ (p : ), Nat.Prime pp n∀ (b : K), b ^ p a
theorem X_pow_sub_C_irreducible_iff_of_odd {K : Type u} [Field K] {n : } (hn : Odd n) {a : K} :
Irreducible (Polynomial.X ^ n - Polynomial.C a) ∀ (d : ), d nd 1∀ (b : K), b ^ d a
theorem X_pow_sub_C_irreducible_of_prime_pow {K : Type u} [Field K] {p : } (hp : Nat.Prime p) (hp' : p 2) (n : ) {a : K} (ha : ∀ (b : K), b ^ p a) :
Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a)
theorem X_pow_sub_C_irreducible_iff_of_prime_pow {K : Type u} [Field K] {p : } (hp : Nat.Prime p) (hp' : p 2) {n : } (hn : n 0) {a : K} :
Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a) ∀ (b : K), b ^ p a

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
      theorem Polynomial.separable_X_pow_sub_C_of_irreducible {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (a : K) (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
      (Polynomial.X ^ n - Polynomial.C a).Separable

      Also see Polynomial.separable_X_pow_sub_C_unit

      noncomputable def autAdjoinRootXPowSubCHom {K : Type u} [Field K] {n : } (hn : 0 < n) (a : K) :
      (rootsOfUnity n, hn K) →* AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) →ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)

      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
        noncomputable def autAdjoinRootXPowSubC {K : Type u} [Field K] {n : } (hn : 0 < n) (a : K) :
        (rootsOfUnity n, hn K) →* AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)

        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
        Instances For
          theorem autAdjoinRootXPowSubC_root {K : Type u} [Field K] {n : } (hn : 0 < n) (a : K) (η : (rootsOfUnity n, hn K)) :
          ((autAdjoinRootXPowSubC hn a) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = η AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
          noncomputable def AdjoinRootXPowSubCEquivToRootsOfUnity {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) :
          (rootsOfUnity n, hn K)

          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
            noncomputable def autAdjoinRootXPowSubCEquiv {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
            (rootsOfUnity n, hn K) ≃* AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)

            The equivalence between the roots of unity of K and Gal(K[ⁿ√a]/K).

            Equations
            Instances For
              theorem autAdjoinRootXPowSubCEquiv_root {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (η : (rootsOfUnity n, hn K)) :
              ((autAdjoinRootXPowSubCEquiv hn H) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = η AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
              theorem autAdjoinRootXPowSubCEquiv_symm_smul {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) :
              ((autAdjoinRootXPowSubCEquiv hn H).symm σ) AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) = σ (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a))

              Galois Group of IsSplittingField K L (X ^ n - C a) #

              theorem isSplittingField_AdjoinRoot_X_pow_sub_C {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) :
              Polynomial.IsSplittingField K (AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) (Polynomial.X ^ n - Polynomial.C a)
              noncomputable def adjoinRootXPowSubCEquiv {K : Type u} [Field K] {n : } {a : K} {L : Type u_1} [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hζ : (primitiveRoots n K).Nonempty) (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (hα : α ^ n = (algebraMap K L) a) :
              AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] L

              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
                theorem adjoinRootXPowSubCEquiv_root {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) :
                (adjoinRootXPowSubCEquiv H ) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = α
                theorem adjoinRootXPowSubCEquiv_symm_eq_root {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) :
                (adjoinRootXPowSubCEquiv H ).symm α = AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
                theorem Algebra.adjoin_root_eq_top_of_isSplittingField {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) :
                theorem IntermediateField.adjoin_root_eq_top_of_isSplittingField {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) :
                Kα =
                @[reducible, inline]
                noncomputable abbrev rootOfSplitsXPowSubC {K : Type u} [Field K] {n : } (hn : 0 < n) (a : K) (L : Type u_2) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] :
                L

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

                Equations
                Instances For
                  theorem rootOfSplitsXPowSubC_pow {K : Type u} [Field K] {n : } (hn : 0 < n) (a : K) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] :
                  noncomputable def autEquivRootsOfUnity {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] :
                  (L ≃ₐ[K] L) ≃* (rootsOfUnity n, hn K)

                  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
                    theorem autEquivRootsOfUnity_apply_rootOfSplit {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] (σ : L ≃ₐ[K] L) :
                    theorem autEquivRootsOfUnity_smul {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) (σ : L ≃ₐ[K] L) :
                    (autEquivRootsOfUnity hn H L) σ α = σ α
                    noncomputable def autEquivZmod {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {ζ : K} (hζ : 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
                      theorem autEquivZmod_symm_apply_intCast {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ) :
                      ((autEquivZmod H L ).symm (Multiplicative.ofAdd m)) α = ζ ^ m α
                      theorem autEquivZmod_symm_apply_natCast {K : Type u} [Field K] {n : } {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ) :
                      ((autEquivZmod H L ).symm (Multiplicative.ofAdd m)) α = ζ ^ m α
                      theorem isCyclic_of_isSplittingField_X_pow_sub_C {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] :
                      theorem isGalois_of_isSplittingField_X_pow_sub_C {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] :
                      theorem finrank_of_isSplittingField_X_pow_sub_C {K : Type u} [Field K] {n : } (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] :

                      Cyclic extensions of order n when K has all n-th roots of unity. #

                      theorem exists_root_adjoin_eq_top_of_isCyclic (K : Type u) [Field K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) [IsGalois K L] [IsCyclic (L ≃ₐ[K] L)] :
                      ∃ (α : L), α ^ Module.finrank K L Set.range (algebraMap K L) Kα =

                      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.

                      theorem irreducible_X_pow_sub_C_of_root_adjoin_eq_top {K : Type u} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] {a : K} {α : L} (ha : α ^ Module.finrank K L = (algebraMap K L) a) (hα : Kα = ) :
                      Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a)
                      theorem isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top {K : Type u} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) {a : K} {α : L} (ha : α ^ Module.finrank K L = (algebraMap K L) a) (hα : Kα = ) :
                      Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a)
                      theorem isCyclic_tfae (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) :
                      [IsGalois K L IsCyclic (L ≃ₐ[K] L), ∃ (a : K), Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a) Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a), ∃ (α : L), α ^ Module.finrank K L Set.range (algebraMap K L) Kα = ].TFAE

                      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.