Kummer Extensions

Main result

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

• autEquivRootsOfUnity: Given an instance IsSplittingField K L (X ^ n - C a) (perhaps via isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top), then the galois group is isomorphic to rootsOfUnity n K, by sending σ ↦ σ α / α for α ^ n = a, and the inverse is given by μ ↦ (α ↦ μ • α).

• autEquivZmod: Furthermore, given an explicit choice ζ of a primitive n-th root of unity, the galois group is then isomorphic to Multiplicative (ZMod n) whose inverse is given by i ↦ (α ↦ ζⁱ • α).

Other results

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

• X_pow_sub_C_irreducible_iff_of_prime_pow: For n = p ^ k an odd prime power, X ^ n - C a is irreducible iff a is not a p-power.
• X_pow_sub_C_irreducible_iff_forall_prime_of_odd: For n odd, X ^ n - C a is irreducible iff a is not a p-power for all prime p ∣ n.
• X_pow_sub_C_irreducible_iff_of_odd: For n odd, X ^ n - C a is irreducible iff a is not a d-power for d ∣ n and d ≠ 1.

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

theorem X_pow_sub_C_splits_of_isPrimitiveRoot {K : Type u} [Field K] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α 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) {α a : R} (hn : 0 < n) (e : α ^ n = a) : Polynomial.X ^ n - Polynomial.C a = ∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C (ζ ^ i * α))

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 a → Irreducible (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 p → p ∣ 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 p → p ∣ 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 ∣ n → d ≠ 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.

def KummerExtension.«termK[_√_]».«delab_app.AdjoinRoot» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def KummerExtension.«termK[_√_]» : Lean.ParserDescr

Equations

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

theorem Polynomial.separable_X_pow_sub_C_of_irreducible {K : Type u} [Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) (a : K) (H : Irreducible (X ^ n - C a)) : (X ^ n - C a).Separable

Also see Polynomial.separable_X_pow_sub_C_unit

noncomputable def autAdjoinRootXPowSubCHom {K : Type u} [Field K] (n : ℕ) (a : K) : ↥(rootsOfUnity n 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.

noncomputable def autAdjoinRootXPowSubC {K : Type u} [Field K] (n : ℕ) (a : K) : ↥(rootsOfUnity n 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

• autAdjoinRootXPowSubC n a = (AlgEquiv.algHomUnitsEquiv K (AdjoinRoot (Polynomial.X ^ n - Polynomial.C a))).toMonoidHom.comp (autAdjoinRootXPowSubCHom n a).toHomUnits

theorem autAdjoinRootXPowSubC_root {K : Type u} [Field K] {n : ℕ} (a : K) (η : ↥(rootsOfUnity n K)) : ((autAdjoinRootXPowSubC n 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) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [NeZero n] (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) : ↥(rootsOfUnity n 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.

noncomputable def autAdjoinRootXPowSubCEquiv {K : Type u} [Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [NeZero n] : ↥(rootsOfUnity n 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

• autAdjoinRootXPowSubCEquiv hζ H = { toFun := (↑(autAdjoinRootXPowSubC n a)).toFun, invFun := AdjoinRootXPowSubCEquivToRootsOfUnity hζ H, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

theorem autAdjoinRootXPowSubCEquiv_root {K : Type u} [Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [NeZero n] (η : ↥(rootsOfUnity n K)) : ((autAdjoinRootXPowSubCEquiv hζ 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) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [NeZero n] (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) : ↑((autAdjoinRootXPowSubCEquiv hζ 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

• adjoinRootXPowSubCEquiv hζ H hα = AlgEquiv.ofBijective (AdjoinRoot.liftHom (Polynomial.X ^ n - Polynomial.C a) α ⋯) ⋯

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ζ H 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ζ H 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) : adjoin K {α} = ⊤

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

• rootOfSplitsXPowSubC hn a L = Polynomial.rootOfSplits (algebraMap K L) ⋯ ⋯

theorem rootOfSplitsXPowSubC_pow {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)] [NeZero n] : rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

noncomputable def autEquivRootsOfUnity {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)] [NeZero n] : (L ≃ₐ[K] L) ≃* ↥(rootsOfUnity n 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

• autEquivRootsOfUnity hζ H L = (adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ H).symm

theorem autEquivRootsOfUnity_apply_rootOfSplit {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)] [NeZero n] (σ : L ≃ₐ[K] L) : σ (rootOfSplitsXPowSubC ⋯ a L) = (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

theorem autEquivRootsOfUnity_smul {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) [NeZero n] (σ : L ≃ₐ[K] L) : (autEquivRootsOfUnity hζ 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)] [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) : (L ≃ₐ[K] L) ≃* Multiplicative (ZMod 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

• autEquivZmod H L hζ = (autEquivRootsOfUnity ⋯ H L).trans ((MulEquiv.subgroupCongr ⋯).trans (AddEquiv.toMultiplicative' ⋯.zmodEquivZPowers.symm))

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) [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) : ((autEquivZmod H L hζ).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) [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℕ) : ((autEquivZmod H L hζ).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)] [NeZero n] : IsCyclic (L ≃ₐ[K] L)

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)] : IsGalois K L

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)] : Module.finrank K L = n

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.