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 : Nat} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α a : K} (e : Eq (HPow.hPow α n) a) : Polynomial.Splits (RingHom.id K) (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))

theorem X_pow_sub_C_eq_prod {R : Type u_1} [CommRing R] [IsDomain R] {n : Nat} {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α a : R} (hn : LT.lt 0 n) (e : Eq (HPow.hPow α n) a) : Eq (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)) ((Finset.range n).prod fun (i : Nat) => HSub.hSub Polynomial.X (DFunLike.coe Polynomial.C (HMul.hMul (HPow.hPow ζ i) α)))

theorem X_pow_mul_sub_C_irreducible {K : Type u} [Field K] {n m : Nat} {a : K} (hm : Irreducible (HSub.hSub (HPow.hPow Polynomial.X m) (DFunLike.coe Polynomial.C a))) (hn : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), Eq (minpoly K x) (HSub.hSub (HPow.hPow Polynomial.X m) (DFunLike.coe Polynomial.C a)) → Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C (IntermediateField.AdjoinSimple.gen K x)))) : Irreducible (HSub.hSub (HPow.hPow Polynomial.X (HMul.hMul n m)) (DFunLike.coe Polynomial.C 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 p → Dvd.dvd p n → ∀ (b : K), Ne (HPow.hPow b p) a) : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C 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 p → Dvd.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 n → Ne 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) : Irreducible (HSub.hSub (HPow.hPow Polynomial.X (HPow.hPow p n)) (DFunLike.coe Polynomial.C 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} : Iff (Irreducible (HSub.hSub (HPow.hPow Polynomial.X (HPow.hPow p n)) (DFunLike.coe Polynomial.C a))) (∀ (b : K), Ne (HPow.hPow 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 : Nat} (hζ : (primitiveRoots n K).Nonempty) (a : K) (H : Irreducible (HSub.hSub (HPow.hPow X n) (DFunLike.coe C a))) : (HSub.hSub (HPow.hPow X n) (DFunLike.coe C a)).Separable

Also see Polynomial.separable_X_pow_sub_C_unit

noncomputable def autAdjoinRootXPowSubCHom {K : Type u} [Field K] (n : Nat) (a : K) : MonoidHom (Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x) (AlgHom K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe 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 : Nat) (a : K) : MonoidHom (Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x) (AlgEquiv K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe 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

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

theorem autAdjoinRootXPowSubC_root {K : Type u} [Field K] {n : Nat} (a : K) (η : Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x) : Eq (DFunLike.coe (DFunLike.coe (autAdjoinRootXPowSubC n a) η) (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))) (HSMul.hSMul η.val.val (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))))

noncomputable def AdjoinRootXPowSubCEquivToRootsOfUnity {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) [NeZero n] (σ : AlgEquiv K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))) : Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x

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 : Nat} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) [NeZero n] : MulEquiv (Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x) (AlgEquiv K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))))

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

Equations

• Eq (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 : Nat} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) [NeZero n] (η : Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x) : Eq (DFunLike.coe (DFunLike.coe (autAdjoinRootXPowSubCEquiv hζ H) η) (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))) (HSMul.hSMul η.val.val (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))))

theorem autAdjoinRootXPowSubCEquiv_symm_smul {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) [NeZero n] (σ : AlgEquiv K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))) : Eq (HSMul.hSMul (DFunLike.coe (autAdjoinRootXPowSubCEquiv hζ H).symm σ).val (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))) (DFunLike.coe σ (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe 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 : Nat} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) : Polynomial.IsSplittingField K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))

noncomputable def adjoinRootXPowSubCEquiv {K : Type u} [Field K] {n : Nat} {a : K} {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))] {α : L} (hζ : (primitiveRoots n K).Nonempty) (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) : AlgEquiv K (AdjoinRoot (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) 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

• Eq (adjoinRootXPowSubCEquiv hζ H hα) (AlgEquiv.ofBijective (AdjoinRoot.liftHom (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)) α ⋯) ⋯)

theorem adjoinRootXPowSubCEquiv_root {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) : Eq (DFunLike.coe (adjoinRootXPowSubCEquiv hζ H hα) (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))) α

theorem adjoinRootXPowSubCEquiv_symm_eq_root {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) : Eq (DFunLike.coe (adjoinRootXPowSubCEquiv hζ H hα).symm α) (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a)))

theorem Algebra.adjoin_root_eq_top_of_isSplittingField {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) : Eq (adjoin K (Singleton.singleton α)) Top.top

theorem IntermediateField.adjoin_root_eq_top_of_isSplittingField {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) : Eq (adjoin K (Singleton.singleton α)) Top.top

@[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

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

theorem rootOfSplitsXPowSubC_pow {K : Type u} [Field K] {n : Nat} (a : K) (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] : Eq (HPow.hPow (rootOfSplitsXPowSubC ⋯ a L) n) (DFunLike.coe (algebraMap K L) a)

noncomputable def autEquivRootsOfUnity {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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] : MulEquiv (AlgEquiv K L L) (Subtype fun (x : Units K) => Membership.mem (rootsOfUnity n K) x)

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

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

theorem autEquivRootsOfUnity_apply_rootOfSplit {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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] (σ : AlgEquiv K L L) : Eq (DFunLike.coe σ (rootOfSplitsXPowSubC ⋯ a L)) (HSMul.hSMul (DFunLike.coe (autEquivRootsOfUnity hζ H L) σ) (rootOfSplitsXPowSubC ⋯ a L))

theorem autEquivRootsOfUnity_smul {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) [NeZero n] (σ : AlgEquiv K L L) : Eq (HSMul.hSMul (DFunLike.coe (autEquivRootsOfUnity hζ H L) σ) α) (DFunLike.coe σ α)

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} (hζ : IsPrimitiveRoot ζ n) : MulEquiv (AlgEquiv K L 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

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

theorem autEquivZmod_symm_apply_intCast {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : Int) : Eq (DFunLike.coe (DFunLike.coe (autEquivZmod H L hζ).symm (DFunLike.coe Multiplicative.ofAdd m.cast)) α) (HSMul.hSMul (HPow.hPow ζ m) α)

theorem autEquivZmod_symm_apply_natCast {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))] {α : L} (hα : Eq (HPow.hPow α n) (DFunLike.coe (algebraMap K L) a)) [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : Nat) : Eq (DFunLike.coe (DFunLike.coe (autEquivZmod H L hζ).symm (DFunLike.coe Multiplicative.ofAdd m.cast)) α) (HSMul.hSMul (HPow.hPow ζ m) α)

theorem isCyclic_of_isSplittingField_X_pow_sub_C {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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] : IsCyclic (AlgEquiv K L L)

theorem isGalois_of_isSplittingField_X_pow_sub_C {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] : IsGalois K L

theorem finrank_of_isSplittingField_X_pow_sub_C {K : Type u} [Field K] {n : Nat} (hζ : (primitiveRoots n K).Nonempty) {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))] : Eq (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 (AlgEquiv K L L)] : Exists fun (α : L) => And (Membership.mem (Set.range (DFunLike.coe (algebraMap K L))) (HPow.hPow α (Module.finrank K L))) (Eq (IntermediateField.adjoin K (Singleton.singleton α)) Top.top)

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 : Eq (HPow.hPow α (Module.finrank K L)) (DFunLike.coe (algebraMap K L) a)) (hα : Eq (IntermediateField.adjoin K (Singleton.singleton α)) Top.top) : Irreducible (HSub.hSub (HPow.hPow Polynomial.X (Module.finrank K L)) (DFunLike.coe 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 : Eq (HPow.hPow α (Module.finrank K L)) (DFunLike.coe (algebraMap K L) a)) (hα : Eq (IntermediateField.adjoin K (Singleton.singleton α)) Top.top) : Polynomial.IsSplittingField K L (HSub.hSub (HPow.hPow Polynomial.X (Module.finrank K L)) (DFunLike.coe 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) : (List.cons (And (IsGalois K L) (IsCyclic (AlgEquiv K L L))) (List.cons (Exists fun (a : K) => And (Irreducible (HSub.hSub (HPow.hPow Polynomial.X (Module.finrank K L)) (DFunLike.coe Polynomial.C a))) (Polynomial.IsSplittingField K L (HSub.hSub (HPow.hPow Polynomial.X (Module.finrank K L)) (DFunLike.coe Polynomial.C a)))) (List.cons (Exists fun (α : L) => And (Membership.mem (Set.range (DFunLike.coe (algebraMap K L))) (HPow.hPow α (Module.finrank K L))) (Eq (IntermediateField.adjoin K (Singleton.singleton α)) Top.top)) List.nil))).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.