Cyclotomic extensions

Let A and B be commutative rings with Algebra A B. For S : Set ℕ, we define a class IsCyclotomicExtension S A B expressing the fact that B is obtained from A by adding n-th primitive roots of unity, for all nonzero n ∈ S.

Main definitions

• IsCyclotomicExtension S A B : means that B is obtained from A by adding n-th primitive roots of unity, for all nonzero n ∈ S.
• CyclotomicField: given n : ℕ and a field K, we define CyclotomicField n K as the splitting field of cyclotomic n K. If n is nonzero in K, it has the instance IsCyclotomicExtension {n} K (CyclotomicField n K).
• CyclotomicRing : if A is a domain with fraction field K and n : ℕ, we define CyclotomicRing n A K as the A-subalgebra of CyclotomicField n K generated by the roots of X ^ n - 1. If n is nonzero in A, it has the instance IsCyclotomicExtension {n} A (CyclotomicRing n A K).

Main results

• IsCyclotomicExtension.trans : if IsCyclotomicExtension S A B and IsCyclotomicExtension T B C, then IsCyclotomicExtension (S ∪ T) A C if Function.Injective (algebraMap B C).
• IsCyclotomicExtension.union_right : given IsCyclotomicExtension (S ∪ T) A B, then IsCyclotomicExtension T (adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ (a : ℕ) = 1 }) B.
• IsCyclotomicExtension.union_left : given IsCyclotomicExtension T A B and S ⊆ T, then IsCyclotomicExtension S A (adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ (a : ℕ) = 1 }).
• IsCyclotomicExtension.finite : if S is finite and IsCyclotomicExtension S A B, then B is a finite A-algebra.
• IsCyclotomicExtension.numberField : a finite cyclotomic extension of a number field is a number field.
• IsCyclotomicExtension.isSplittingField_X_pow_sub_one : if IsCyclotomicExtension {n} K L, then L is the splitting field of X ^ n - 1.
• IsCyclotomicExtension.splitting_field_cyclotomic : if IsCyclotomicExtension {n} K L, then L is the splitting field of cyclotomic n K.

Implementation details

Our definition of IsCyclotomicExtension is very general, to allow rings of any characteristic and infinite extensions, but it will mainly be used in the case S = {n} and for integral domains. All results are in the IsCyclotomicExtension namespace. Note that some results, for example IsCyclotomicExtension.trans, IsCyclotomicExtension.finite, IsCyclotomicExtension.numberField, IsCyclotomicExtension.finiteDimensional, IsCyclotomicExtension.isGalois and CyclotomicField.algebraBase are lemmas, but they can be made local instances. Some of them are included in the Cyclotomic locale.

class IsCyclotomicExtension (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : Prop

Given an A-algebra B and S : Set ℕ, we define IsCyclotomicExtension S A B requiring that there is an n-th primitive root of unity in B for all nonzero n ∈ S and that B is generated over A by the roots of X ^ n - 1.

• exists_isPrimitiveRoot {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0) : ∃ (r : B), IsPrimitiveRoot r n

  For all nonzero n ∈ S, there exists a primitive n-th root of unity in B.

• adjoin_roots (x : B) : x ∈ Algebra.adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

  The n-th roots of unity, for n ∈ S nonzero, generate B as an A-algebra.

theorem isCyclotomicExtension_iff (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B ↔ (∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

@[deprecated IsCyclotomicExtension.exists_isPrimitiveRoot (since := "2025-05-21")]

theorem IsCyclotomicExtension.exists_prim_root {S : Set ℕ} (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0) : ∃ (r : B), IsPrimitiveRoot r n

theorem IsCyclotomicExtension.iff_adjoin_eq_top (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B ↔ (∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n) ∧ Algebra.adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤

A reformulation of IsCyclotomicExtension that uses ⊤.

theorem IsCyclotomicExtension.iff_singleton (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension {n} A B ↔ (∃ (r : B), IsPrimitiveRoot r n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b : B | b ^ n = 1}

A reformulation of IsCyclotomicExtension in the case S is a singleton.

instance IsCyclotomicExtension.instSubsingleton (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension ∅ A B] : Subsingleton (Subalgebra A B)

theorem IsCyclotomicExtension.eq_self_sdiff_zero (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B

theorem IsCyclotomicExtension.singleton_one (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension {1} A B] : ⊥ = ⊤

If IsCyclotomicExtension {1} A B, then the image of A in B equals B.

theorem IsCyclotomicExtension.singleton_zero_of_bot_eq_top {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (h : ⊥ = ⊤) : IsCyclotomicExtension {0} A B

If (⊥ : SubAlgebra A B) = ⊤, then IsCyclotomicExtension {0} A B.

theorem IsCyclotomicExtension.isCyclotomicExtension_zero_iff {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension {0} A B ↔ Function.Surjective ⇑(algebraMap A B)

theorem IsCyclotomicExtension.trans (S T : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C] [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C] (h : Function.Injective ⇑(algebraMap B C)) : IsCyclotomicExtension (S ∪ T) A C

Transitivity of cyclotomic extensions.

theorem IsCyclotomicExtension.subsingleton_iff (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [Subsingleton B] : IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}

theorem IsCyclotomicExtension.union_right (S T : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension (S ∪ T) A B] : IsCyclotomicExtension T (↥(Algebra.adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B

If B is a cyclotomic extension of A given by roots of unity of order in S ∪ T, then B is a cyclotomic extension of adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 } given by roots of unity of order in T.

theorem IsCyclotomicExtension.union_left (S T : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) : IsCyclotomicExtension S A ↥(Algebra.adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

If B is a cyclotomic extension of A given by roots of unity of order in T and S ⊆ T, then adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 } is a cyclotomic extension of B given by roots of unity of order in S.

theorem IsCyclotomicExtension.of_union_of_dvd {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) [H : IsCyclotomicExtension S A B] : IsCyclotomicExtension (S ∪ {n}) A B

If there exists a nonzero s ∈ S such that n ∣ s, then IsCyclotomicExtension S A B implies IsCyclotomicExtension (S ∪ {n}) A B.

theorem IsCyclotomicExtension.iff_union_of_dvd {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) : IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

If there exists a nonzero s ∈ S such that n ∣ s, then IsCyclotomicExtension S A B if and only if IsCyclotomicExtension (S ∪ {n}) A B.

theorem IsCyclotomicExtension.iff_union_singleton_one (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

IsCyclotomicExtension S A B is equivalent to IsCyclotomicExtension (S ∪ {1}) A B.

theorem IsCyclotomicExtension.singleton_one_of_bot_eq_top {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (h : ⊥ = ⊤) : IsCyclotomicExtension {1} A B

If (⊥ : SubAlgebra A B) = ⊤, then IsCyclotomicExtension {1} A B.

theorem IsCyclotomicExtension.singleton_one_of_algebraMap_bijective {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (h : Function.Surjective ⇑(algebraMap A B)) : IsCyclotomicExtension {1} A B

If Function.Surjective (algebraMap A B), then IsCyclotomicExtension {1} A B.

theorem IsCyclotomicExtension.equiv (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] {C : Type u_1} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension S A B] (f : B ≃ₐ[A] C) : IsCyclotomicExtension S A C

Given (f : B ≃ₐ[A] C), if IsCyclotomicExtension S A B then IsCyclotomicExtension S A C.

theorem IsCyclotomicExtension.neZero_of_mem (n : ℕ) [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] (hn : n ∈ S) : NeZero ↑n

theorem IsCyclotomicExtension.neZero_of_mem' (n : ℕ) [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] (hn : n ∈ S) : NeZero ↑n

theorem IsCyclotomicExtension.neZero (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ↑n

theorem IsCyclotomicExtension.neZero' (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ↑n

theorem IsCyclotomicExtension.integral (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] : Algebra.IsIntegral A B

A cyclotomic extension is integral.

theorem Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n) : IsCyclotomicExtension S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

theorem IsCyclotomicExtension.algEquiv_eq_of_apply_eq (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] {f g : B ≃ₐ[A] B} (H : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n ∧ f r = g r) : f = g

Two elements in the Galois group of a cyclotomic extension are equal if their actions on primitive roots are equal.

theorem IsCyclotomicExtension.isMulCommutative (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] : IsMulCommutative (B ≃ₐ[A] B)

Cyclotomic extensions are abelian.

theorem IsCyclotomicExtension.finite_of_singleton (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] [h : IsCyclotomicExtension {n} A B] : Module.Finite A B

theorem IsCyclotomicExtension.finite (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] [h₁ : Finite ↑S] [h₂ : IsCyclotomicExtension S A B] : Module.Finite A B

If S is finite and IsCyclotomicExtension S A B, then B is a finite A-algebra.

theorem IsCyclotomicExtension.numberField (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [h : NumberField K] [Finite ↑S] [IsCyclotomicExtension S K L] : NumberField L

A cyclotomic finite extension of a number field is a number field.

theorem IsCyclotomicExtension.finiteDimensional (S : Set ℕ) (K : Type w) [Field K] (C : Type z) [Finite ↑S] [CommRing C] [Algebra K C] [IsDomain C] [IsCyclotomicExtension S K C] : FiniteDimensional K C

If S is finite and IsCyclotomicExtension S K A, then finiteDimensional K A.

theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] {ζ : B} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) : Algebra.adjoin A ((Polynomial.cyclotomic n A).rootSet B) = Algebra.adjoin A {b : B | ∃ a ∈ {n}, a ≠ 0 ∧ b ^ a = 1}

theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {n : ℕ} [NeZero n] [IsDomain B] {ζ : B} (hζ : IsPrimitiveRoot ζ n) : Algebra.adjoin A ((Polynomial.cyclotomic n A).rootSet B) = Algebra.adjoin A {ζ}

theorem IsCyclotomicExtension.adjoin_primitive_root_eq_top {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {n : ℕ} [NeZero n] [IsDomain B] [h : IsCyclotomicExtension {n} A B] {ζ : B} (hζ : IsPrimitiveRoot ζ n) : Algebra.adjoin A {ζ} = ⊤

theorem IsPrimitiveRoot.adjoin_isCyclotomicExtension (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {ζ : B} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} A ↥(Algebra.adjoin A {ζ})

theorem IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension (K : Type w) {L : Type z} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] {n : ℕ} [NeZero n] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} K ↥K⟮ζ⟯

theorem IsCyclotomicExtension.splits_X_pow_sub_one {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [H : IsCyclotomicExtension S K L] (hS : n ∈ S) : Polynomial.Splits (algebraMap K L) (Polynomial.X ^ n - 1)

A cyclotomic extension splits X ^ n - 1 if n ∈ S.

theorem IsCyclotomicExtension.splits_cyclotomic {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (hS : n ∈ S) : Polynomial.Splits (algebraMap K L) (Polynomial.cyclotomic n K)

A cyclotomic extension splits cyclotomic n K if n ∈ S.

theorem IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n) : IsCyclotomicExtension S K ↥(adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

theorem IsCyclotomicExtension.isSeparable (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] : Algebra.IsSeparable K L

theorem IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (M : Type u_1) [Field M] [Algebra K M] [IsSepClosed M] : Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

theorem IsCyclotomicExtension.isGalois (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] : IsGalois K L

noncomputable def IsCyclotomicExtension.algEquiv (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (L' : Type u_1) [Field L'] [Algebra K L'] [IsCyclotomicExtension S K L'] : L ≃ₐ[K] L'

Any two S-cyclotomic extensions are isomorphic.

Equations

• IsCyclotomicExtension.algEquiv S K L L' = ⋯.some.trans ⋯.some.symm

theorem IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (M : Type u_1) [Field M] [Algebra K M] (h : ∀ n ∈ S, n ≠ 0 → ∃ (r : M), IsPrimitiveRoot r n) : Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

theorem IsCyclotomicExtension.isSplittingField_X_pow_sub_one (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] : Polynomial.IsSplittingField K L (Polynomial.X ^ n - 1)

If IsCyclotomicExtension {n} K L, then L is the splitting field of X ^ n - 1.

theorem IsCyclotomicExtension.splitting_field_cyclotomic (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] : Polynomial.IsSplittingField K L (Polynomial.cyclotomic n K)

If IsCyclotomicExtension {n} K L, then L is the splitting field of cyclotomic n K.

def CyclotomicField (n : ℕ) (K : Type w) [Field K] : Type w

Given a nonzero n : ℕ and a field K, we define CyclotomicField n K as the splitting field of cyclotomic n K. If n is nonzero in K, it has the instance IsCyclotomicExtension {n} K (CyclotomicField n K).

Equations

• CyclotomicField n K = (Polynomial.cyclotomic n K).SplittingField

instance CyclotomicField.instField (n : ℕ) (K : Type w) [Field K] : Field (CyclotomicField n K)

Equations

• CyclotomicField.instField n K = id inferInstance

instance CyclotomicField.algebra (n : ℕ) (K : Type w) [Field K] : Algebra K (CyclotomicField n K)

Equations

• CyclotomicField.algebra n K = id inferInstance

instance CyclotomicField.instInhabited (n : ℕ) (K : Type w) [Field K] : Inhabited (CyclotomicField n K)

Equations

• CyclotomicField.instInhabited n K = id inferInstance

instance CyclotomicField.instCharZero (n : ℕ) (K : Type w) [Field K] [CharZero K] : CharZero (CyclotomicField n K)

instance CyclotomicField.isCyclotomicExtension (n : ℕ) [NeZero n] (K : Type w) [Field K] [NeZero ↑n] : IsCyclotomicExtension {n} K (CyclotomicField n K)

instance CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfNat (K : Type w) [Field K] : IsCyclotomicExtension {0} K (CyclotomicField 0 K)

instance CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero (n : ℕ) (K : Type w) [Field K] [CharZero K] : IsCyclotomicExtension {n} K (CyclotomicField n K)

instance CyclotomicField.instNumberField (n : ℕ) (K : Type w) [Field K] [NumberField K] : NumberField (CyclotomicField n K)

instance CyclotomicField.algebraBase (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : Algebra A (CyclotomicField n K)

If K is an A-algebra, the A-algebra structure on CyclotomicField n K.

Equations

• CyclotomicField.algebraBase n A K = Polynomial.SplittingField.instAlgebra (Polynomial.cyclotomic n K)

instance instIsScalarTowerCyclotomicField (n : ℕ) (K : Type w) [Field K] {R : Type u_1} [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicField n K)

instance instNoZeroSMulDivisorsCyclotomicFieldOfIsFractionRing (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicField n K)

def CyclotomicRing (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : Type w

If A is a domain with fraction field K and n : ℕ, we define CyclotomicRing n A K as the A-subalgebra of CyclotomicField n K generated by the roots of X ^ n - 1. If n is nonzero in A, it has the instance IsCyclotomicExtension {n} A (CyclotomicRing n A K).

Equations

• CyclotomicRing n A K = ↥(Algebra.adjoin A {b : CyclotomicField n K | b ^ n = 1})

instance CyclotomicRing.instCommRing (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : CommRing (CyclotomicRing n A K)

Equations

• CyclotomicRing.instCommRing n A K = id inferInstance

instance CyclotomicRing.instIsDomain (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : IsDomain (CyclotomicRing n A K)

instance CyclotomicRing.instInhabited (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : Inhabited (CyclotomicRing n A K)

Equations

• CyclotomicRing.instInhabited n A K = id inferInstance

instance CyclotomicRing.algebraBase (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : Algebra A (CyclotomicRing n A K)

The A-algebra structure on CyclotomicRing n A K.

Equations

• CyclotomicRing.algebraBase n A K = (Algebra.adjoin A {b : CyclotomicField n K | b ^ n = 1}).algebra

instance CyclotomicRing.instNoZeroSMulDivisorsOfIsFractionRing (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicRing n A K)

theorem CyclotomicRing.algebraBase_injective (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] : Function.Injective ⇑(algebraMap A (CyclotomicRing n A K))

instance CyclotomicRing.instAlgebraCyclotomicField (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : Algebra (CyclotomicRing n A K) (CyclotomicField n K)

Equations

• CyclotomicRing.instAlgebraCyclotomicField n A K = (Algebra.adjoin A {b : CyclotomicField n K | b ^ n = 1}).toAlgebra

theorem CyclotomicRing.adjoin_algebra_injective (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : Function.Injective ⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))

instance CyclotomicRing.instNoZeroSMulDivisorsCyclotomicField (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : NoZeroSMulDivisors (CyclotomicRing n A K) (CyclotomicField n K)

instance CyclotomicRing.instIsScalarTowerCyclotomicField (n : ℕ) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] : IsScalarTower A (CyclotomicRing n A K) (CyclotomicField n K)

instance CyclotomicRing.isCyclotomicExtension (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [NeZero ↑n] : IsCyclotomicExtension {n} A (CyclotomicRing n A K)

instance CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDomain A] [NeZero ↑n] : IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K)

theorem CyclotomicRing.eq_adjoin_primitive_root (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] {μ : CyclotomicField n K} (h : IsPrimitiveRoot μ n) : CyclotomicRing n A K = ↥(Algebra.adjoin A {μ})

theorem IsSepClosed.isCyclotomicExtension (S : Set ℕ) (K : Type w) [Field K] [IsSepClosed K] (h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a) : IsCyclotomicExtension S K K

Separably closed fields are S-cyclotomic extensions over themselves if NeZero ((a : ℕ) : K) for all nonzero a ∈ S.

@[deprecated IsSepClosed.isCyclotomicExtension (since := "2025-06-22")]

theorem IsAlgClosed.isCyclotomicExtension (S : Set ℕ) (K : Type w) [Field K] [IsSepClosed K] (h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a) : IsCyclotomicExtension S K K

Alias of IsSepClosed.isCyclotomicExtension.

---

Separably closed fields are S-cyclotomic extensions over themselves if NeZero ((a : ℕ) : K) for all nonzero a ∈ S.

instance IsSepClosedOfCharZero.isCyclotomicExtension (K : Type w) [Field K] [IsSepClosed K] [CharZero K] (S : Set ℕ) : IsCyclotomicExtension S K K

@[deprecated IsSepClosedOfCharZero.isCyclotomicExtension (since := "2025-06-22")]

theorem IsAlgClosedOfCharZero.isCyclotomicExtension (K : Type w) [Field K] [IsSepClosed K] [CharZero K] (S : Set ℕ) : IsCyclotomicExtension S K K

Alias of IsSepClosedOfCharZero.isCyclotomicExtension.

theorem IsCyclotomicExtension.mem_of_pow_eq_one (S : Set ℕ) {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C : Subalgebra A B) [h : IsCyclotomicExtension S A ↥C] {m : ℕ} {ζ : B} (h₁ : m ∈ S) (h₂ : m ≠ 0) (hζ : ζ ^ m = 1) : ζ ∈ C

theorem isCyclotomicExtension_iff_eq_adjoin (S : Set ℕ) {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C : Subalgebra A B) (hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n) : IsCyclotomicExtension S A ↥C ↔ C = Algebra.adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

theorem isCyclotomicExtension_singleton_iff_eq_adjoin (n : ℕ) [NeZero n] {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C : Subalgebra A B) {ζ : B} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} A ↥C ↔ C = Algebra.adjoin A {ζ}

theorem IsCyclotomicExtension.eq (S : Set ℕ) {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension S A ↥C₁] [h₂ : IsCyclotomicExtension S A ↥C₂] : C₁ = C₂

theorem IsCyclotomicExtension.le_of_dvd {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (n₁ n₂ : ℕ) (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₂] (h : n₁ ∣ n₂) : C₁ ≤ C₂

theorem IsCyclotomicExtension.lcm_sup {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (n₁ n₂ : ℕ) (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₁] [NeZero n₂] : IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

theorem IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) {ζ : L} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} K ↥F ↔ F = K⟮ζ⟯

theorem IntermediateField.isCyclotomicExtension_eq (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension S K ↥F₁] [h₂ : IsCyclotomicExtension S K ↥F₂] : F₁ = F₂

theorem IntermediateField.isCyclotomicExtension_le_of_dvd (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (n₁ n₂ : ℕ) (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension {n₁} K ↥F₁] [h₂ : IsCyclotomicExtension {n₂} K ↥F₂] [NeZero n₂] (h : n₁ ∣ n₂) : F₁ ≤ F₂

theorem IntermediateField.isCyclotomicExtension_lcm_sup (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (n₁ n₂ : ℕ) (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension {n₁} K ↥F₁] [h₂ : IsCyclotomicExtension {n₂} K ↥F₂] [NeZero n₁] [NeZero n₂] : IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)