# mathlib3documentation

number_theory.cyclotomic.basic

# Cyclotomic extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let A and B be commutative rings with algebra A B. For S : set ℕ+, we define a class is_cyclotomic_extension 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 #

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

## Main results #

• is_cyclotomic_extension.trans : if is_cyclotomic_extension S A B and is_cyclotomic_extension T B C, then is_cyclotomic_extension (S ∪ T) A C if function.injective (algebra_map B C).
• is_cyclotomic_extension.union_right : given is_cyclotomic_extension (S ∪ T) A B, then is_cyclotomic_extension T (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }) B.
• is_cyclotomic_extension.union_right : given is_cyclotomic_extension T A B and S ⊆ T, then is_cyclotomic_extension S A (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }).
• is_cyclotomic_extension.finite : if S is finite and is_cyclotomic_extension S A B, then B is a finite A-algebra.
• is_cyclotomic_extension.number_field : a finite cyclotomic extension of a number field is a number field.
• is_cyclotomic_extension.splitting_field_X_pow_sub_one : if is_cyclotomic_extension {n} K L, then L is the splitting field of X ^ n - 1.
• is_cyclotomic_extension.splitting_field_cyclotomic : if is_cyclotomic_extension {n} K L, then L is the splitting field of cyclotomic n K.

## Implementation details #

Our definition of is_cyclotomic_extension 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 is_cyclotomic_extension namespace. Note that some results, for example is_cyclotomic_extension.trans, is_cyclotomic_extension.finite, is_cyclotomic_extension.number_field, is_cyclotomic_extension.finite_dimensional, is_cyclotomic_extension.is_galois and cyclotomic_field.algebra_base are lemmas, but they can be made local instances. Some of them are included in the cyclotomic locale.

@[class]
structure is_cyclotomic_extension (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] :
Prop

Given an A-algebra B and S : set ℕ+, we define is_cyclotomic_extension S A B requiring that there is a 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.

Instances of this typeclass
theorem is_cyclotomic_extension_iff (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] :
( {n : ℕ+}, n S ( (r : B), n)) (x : B), x {b : B | (n : ℕ+), n S b ^ n = 1}
theorem is_cyclotomic_extension.iff_adjoin_eq_top (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] :
( (n : ℕ+), n S ( (r : B), n)) {b : B | (n : ℕ+), n S b ^ n = 1} =

A reformulation of is_cyclotomic_extension that uses ⊤.

theorem is_cyclotomic_extension.iff_singleton (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] :
B ( (r : B), (x : B), x {b : B | b ^ n = 1}

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

theorem is_cyclotomic_extension.empty (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [h : B] :

If is_cyclotomic_extension ∅ A B, then the image of A in B equals B.

theorem is_cyclotomic_extension.singleton_one (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [h : B] :

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

If (⊥ : subalgebra A B) = ⊤, then is_cyclotomic_extension ∅ A B.

theorem is_cyclotomic_extension.trans (S T : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] (C : Type w) [comm_ring C] [ C] [ C] [ C] [hS : B] [hT : C] (h : function.injective C)) :

Transitivity of cyclotomic extensions.

theorem is_cyclotomic_extension.subsingleton_iff (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [subsingleton B] :
S = S = {1}
theorem is_cyclotomic_extension.union_right (S T : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [h : is_cyclotomic_extension (S T) A B] :
{b : B | (a : ℕ+), 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 is_cyclotomic_extension.union_left (S T : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [h : B] (hS : S T) :
{b : B | (a : ℕ+), 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 is_cyclotomic_extension.of_union_of_dvd {n : ℕ+} {S : set ℕ+} (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] (h : (s : ℕ+), s S n s) (hS : S.nonempty) [H : B] :

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

theorem is_cyclotomic_extension.iff_union_of_dvd {n : ℕ+} {S : set ℕ+} (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] (h : (s : ℕ+), s S n s) (hS : S.nonempty) :

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

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

theorem is_cyclotomic_extension.singleton_one_of_bot_eq_top {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [ B] (h : = ) :
B

If (⊥ : subalgebra A B) = ⊤, then is_cyclotomic_extension {1} A B.

If function.surjective (algebra_map A B), then is_cyclotomic_extension {1} A B.

@[protected]
theorem is_cyclotomic_extension.equiv (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] {C : Type u_1} [comm_ring C] [ C] [h : B] (f : B ≃ₐ[A] C) :

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

@[protected]
theorem is_cyclotomic_extension.ne_zero (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [h : B] [is_domain B] :
@[protected]
theorem is_cyclotomic_extension.ne_zero' (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [ B] [is_domain B] :
theorem is_cyclotomic_extension.finite_of_singleton (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [is_domain B] [h : B] :
@[protected]
theorem is_cyclotomic_extension.finite (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [is_domain B] [h₁ : finite S] [h₂ : B] :

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

theorem is_cyclotomic_extension.number_field (S : set ℕ+) (K : Type w) (L : Type z) [field K] [field L] [ L] [h : number_field K] [finite S] [ L] :

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

theorem is_cyclotomic_extension.integral (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [ B] [is_domain B] [finite S] [ B] :

A finite cyclotomic extension of an integral noetherian domain is integral

theorem is_cyclotomic_extension.finite_dimensional (S : set ℕ+) (K : Type w) [field K] (C : Type z) [finite S] [comm_ring C] [ C] [is_domain C] [ C] :

If S is finite and is_cyclotomic_extension S K A, then finite_dimensional K A.

theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [ B] [is_domain B] {ζ : B} {n : ℕ+} (hζ : n) :
A).root_set B) = {b : B | (a : ℕ+), a {n} b ^ a = 1}
theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [ B] {n : ℕ+} [is_domain B] {ζ : B} (hζ : n) :
A).root_set B) = {ζ}
theorem is_cyclotomic_extension.adjoin_primitive_root_eq_top {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [ B] {n : ℕ+} [is_domain B] [h : B] {ζ : B} (hζ : n) :
{ζ} =
theorem is_primitive_root.adjoin_is_cyclotomic_extension (A : Type u) {B : Type v} [comm_ring A] [comm_ring B] [ B] {ζ : B} {n : ℕ+} (h : n) :
{ζ})
theorem is_cyclotomic_extension.splits_X_pow_sub_one {n : ℕ+} {S : set ℕ+} (K : Type w) (L : Type z) [field K] [field L] [ L] [H : L] (hS : n S) :
- 1)

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

theorem is_cyclotomic_extension.splits_cyclotomic {n : ℕ+} {S : set ℕ+} (K : Type w) (L : Type z) [field K] [field L] [ L] [ L] (hS : n S) :

A cyclotomic extension splits cyclotomic n K if n ∈ S and ne_zero (n : K).

theorem is_cyclotomic_extension.splitting_field_X_pow_sub_one (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [ L] [ L] :
- 1)

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

noncomputable def is_cyclotomic_extension.alg_equiv (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [ L] [ L] (L' : Type u_1) [field L'] [ L'] [ L'] :
L ≃ₐ[K] L'

Any two n-th cyclotomic extensions are isomorphic.

Equations
• = let h₁ : - 1) := _, h₂ : - 1) := _ in
theorem is_cyclotomic_extension.is_galois (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [ L] [ L] :
L
theorem is_cyclotomic_extension.splitting_field_cyclotomic (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [ L] [ L] :

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

@[protected, instance]
noncomputable def cyclotomic_field.algebra (n : ℕ+) (K : Type w) [field K] :
K)
@[protected, instance]
noncomputable def cyclotomic_field.field (n : ℕ+) (K : Type w) [field K] :
@[protected, instance]
noncomputable def cyclotomic_field.inhabited (n : ℕ+) (K : Type w) [field K] :
def cyclotomic_field (n : ℕ+) (K : Type w) [field K] :

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

Equations
Instances for cyclotomic_field
@[protected, instance]
def cyclotomic_field.char_zero (n : ℕ+) (K : Type w) [field K] [char_zero K] :
@[protected, instance]
@[protected, nolint, instance]
noncomputable def cyclotomic_field.algebra_base (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
K)

If K is the fraction field of A, the A-algebra structure on cyclotomic_field n K.

Equations
@[protected, instance]
noncomputable def cyclotomic_field.algebra' (n : ℕ+) (K : Type w) [field K] {R : Type u_1} [comm_ring R] [ K] :
K)
Equations
@[protected, instance]
def cyclotomic_field.is_scalar_tower (n : ℕ+) (K : Type w) [field K] {R : Type u_1} [comm_ring R] [ K] :
K)
@[protected, instance]
def cyclotomic_field.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
@[nolint]
def cyclotomic_ring (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :

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

Equations
Instances for cyclotomic_ring
@[protected, instance]
noncomputable def cyclotomic_ring.inhabited (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
@[protected, instance]
def cyclotomic_ring.is_domain (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
@[protected, instance]
noncomputable def cyclotomic_ring.comm_ring (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
@[protected, instance]
noncomputable def cyclotomic_ring.algebra_base (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
A K)

The A-algebra structure on cyclotomic_ring n A K.

Equations
@[protected, instance]
def cyclotomic_ring.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
A K)
theorem cyclotomic_ring.algebra_base_injective (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
@[protected, instance]
noncomputable def cyclotomic_ring.cyclotomic_field.algebra (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
algebra A K) K)
Equations
theorem cyclotomic_ring.adjoin_algebra_injective (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
@[protected, instance]
def cyclotomic_ring.cyclotomic_field.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
K)
@[protected, instance]
def cyclotomic_ring.cyclotomic_field.is_scalar_tower (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] :
A K) K)
@[protected, instance]
def cyclotomic_ring.is_cyclotomic_extension (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] [ne_zero n] :
A K)
@[protected, instance]
theorem cyclotomic_ring.eq_adjoin_primitive_root (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [ K] [ K] {μ : K} (h : n) :
K = {μ})
theorem is_alg_closed.is_cyclotomic_extension (S : set ℕ+) (K : Type w) [field K] (h : (a : ℕ+), a S ) :

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

@[protected, instance]