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 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 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 ∧ 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 ∧ 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 n ∈ S and that B is generated over A by the roots of X ^ n - 1.

• exists_prim_root : ∀ {n : ℕ+}, n ∈ S → ∃ (r : B), IsPrimitiveRoot r ↑n

  For all 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, b ^ ↑n = 1}

  The n-th roots of unity, for n ∈ S, 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 → ∃ (r : B), IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b : B | ∃ n ∈ S, b ^ ↑n = 1}

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, ∃ (r : B), IsPrimitiveRoot r ↑n) ∧ Algebra.adjoin A {b : B | ∃ n ∈ S, b ^ ↑n = 1} = ⊤

A reformulation of IsCyclotomicExtension that uses ⊤.

theorem IsCyclotomicExtension.iff_singleton (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.

theorem IsCyclotomicExtension.empty (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension ∅ A B] : ⊥ = ⊤

If IsCyclotomicExtension ∅ A B, then the image of A in B equals 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 ∅ A B

If (⊥ : SubAlgebra A B) = ⊤, then IsCyclotomicExtension ∅ 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 = ∅ ∨ S = {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, 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 ∧ 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, 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 ∧ 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 : ℕ+} {S : Set ℕ+} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∀ s ∈ S, n ∣ s) (hS : S.Nonempty) [H : IsCyclotomicExtension S A B] : IsCyclotomicExtension (S ∪ {n}) A B

If ∀ s ∈ S, n ∣ s and S is not empty, then IsCyclotomicExtension S A B implies IsCyclotomicExtension (S ∪ {n}) A B.

theorem IsCyclotomicExtension.iff_union_of_dvd {n : ℕ+} {S : Set ℕ+} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∀ s ∈ S, n ∣ s) (hS : S.Nonempty) : IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

If ∀ s ∈ S, n ∣ s and S is not empty, 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 (n : ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ↑↑n

theorem IsCyclotomicExtension.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.finite_of_singleton (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.integral (S : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] [IsNoetherianRing A] [Finite ↑S] [IsCyclotomicExtension S A B] : Algebra.IsIntegral A B

A finite cyclotomic extension of an integral noetherian domain is integral

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 : ℕ+} (hζ : IsPrimitiveRoot ζ ↑n) : Algebra.adjoin A ((Polynomial.cyclotomic (↑n) A).rootSet B) = Algebra.adjoin A {b : B | ∃ a ∈ {n}, 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 : ℕ+} [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 : ℕ+} [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 : ℕ+} (h : IsPrimitiveRoot ζ ↑n) : IsCyclotomicExtension {n} A ↥(Algebra.adjoin A {ζ})

theorem IsCyclotomicExtension.splits_X_pow_sub_one {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 : ℕ+} {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 IsCyclotomicExtension.isSplittingField_X_pow_sub_one (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.

def IsCyclotomicExtension.algEquiv (n : ℕ+) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (L' : Type u_1) [Field L'] [Algebra K L'] [IsCyclotomicExtension {n} K L'] : L ≃ₐ[K] L'

Any two n-th cyclotomic extensions are isomorphic.

Equations

• IsCyclotomicExtension.algEquiv n K L L' = (Polynomial.IsSplittingField.algEquiv L (Polynomial.X ^ ↑n - 1)).trans (Polynomial.IsSplittingField.algEquiv L' (Polynomial.X ^ ↑n - 1)).symm

theorem IsCyclotomicExtension.isGalois (n : ℕ+) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] : IsGalois K L

theorem IsCyclotomicExtension.splitting_field_cyclotomic (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 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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 the fraction field of A, the A-algebra structure on CyclotomicField n K.

Equations

• CyclotomicField.algebraBase n A K = Polynomial.SplittingField.algebra' (Polynomial.cyclotomic (↑n) K)

instance CyclotomicField.algebra' (n : ℕ+) (K : Type w) [Field K] {R : Type u_1} [CommRing R] [Algebra R K] : Algebra R (CyclotomicField n K)

Equations

• CyclotomicField.algebra' n K = Polynomial.SplittingField.algebra' (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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

instance CyclotomicRing.isCyclotomicExtension (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)

Equations

• ⋯ = ⋯

instance CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCastVal (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)

Equations

• ⋯ = ⋯

theorem CyclotomicRing.eq_adjoin_primitive_root (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 IsAlgClosed.isCyclotomicExtension (S : Set ℕ+) (K : Type w) [Field K] [IsAlgClosed K] (h : ∀ a ∈ S, NeZero ↑↑a) : IsCyclotomicExtension S K K

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

instance IsAlgClosedOfCharZero.isCyclotomicExtension (K : Type w) [Field K] [IsAlgClosed K] [CharZero K] (S : Set ℕ+) : IsCyclotomicExtension S K K

Equations

• ⋯ = ⋯