Cyclotomic extensions #

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.
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 and ne_zero ((n : ℕ) : K), then L is the splitting field of X ^ n - 1.
is_cyclotomic_extension.splitting_field_cyclotomic : if is_cyclotomic_extension {n} K L and ne_zero ((n : ℕ) : K), 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} with (n : A) ≠ 0 (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.

source

@[class]

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

Prop

exists_root : ∀ {a : ℕ+}, a ∈ S → (∃ (r : B), ⇑(polynomial.aeval r) (polynomial.cyclotomic ↑a A) = 0)
adjoin_roots : ∀ (x : B), x ∈ algebra.adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1}

Given an A-algebra B and S : set ℕ+, we define is_cyclotomic_extension S A B requiring that cyclotomic a A has a root in B for all a ∈ S and that B is generated over A by the roots of X ^ n - 1.

Instances

source

theorem is_cyclotomic_extension_iff (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] :

is_cyclotomic_extension S A B ↔ (∀ {a : ℕ+}, a ∈ S → (∃ (r : B), ⇑(polynomial.aeval r) (polynomial.cyclotomic ↑a A) = 0)) ∧ ∀ (x : B), x ∈ algebra.adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1}

source

theorem is_cyclotomic_extension.iff_adjoin_eq_top (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] :

is_cyclotomic_extension S A B ↔ (∀ (a : ℕ+), a ∈ S → (∃ (r : B), ⇑(polynomial.aeval r) (polynomial.cyclotomic ↑a A) = 0)) ∧ algebra.adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1} = ⊤

A reformulation of is_cyclotomic_extension that uses ⊤.

source

theorem is_cyclotomic_extension.iff_singleton (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] :

is_cyclotomic_extension {n} A B ↔ (∃ (r : B), ⇑(polynomial.aeval r) (polynomial.cyclotomic ↑n A) = 0) ∧ ∀ (x : B), x ∈ algebra.adjoin A {b : B | b ^ ↑n = 1}

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

source

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

⊥ = ⊤

If is_cyclotomic_extension ∅ A B, then A = B.

source

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

is_cyclotomic_extension (S ∪ T) A C

Transitivity of cyclotomic extensions.

source

theorem is_cyclotomic_extension.union_right (S T : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [h : is_cyclotomic_extension (S ∪ T) A B] :

is_cyclotomic_extension T ↥(algebra.adjoin A {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.

source

theorem is_cyclotomic_extension.union_left (S T : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [h : is_cyclotomic_extension T A B] (hS : S ⊆ T) :

is_cyclotomic_extension S A ↥(algebra.adjoin A {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.

source

theorem is_cyclotomic_extension.finite_of_singleton (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [is_domain B] [h : is_cyclotomic_extension {n} A B] :

module.finite A B

source

theorem is_cyclotomic_extension.finite (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [is_domain B] [h₁ : fintype ↥S] [h₂ : is_cyclotomic_extension S A B] :

module.finite A B

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

source

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

number_field L

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

source

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

algebra.is_integral A B

A finite cyclotomic extension of an integral noetherian domain is integral

source

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

finite_dimensional K C

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

source

theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots (n : ℕ+) {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] [decidable_eq B] [is_domain B] {ζ : B} (hζ : is_primitive_root ζ ↑n) :

algebra.adjoin A ↑((polynomial.map (algebra_map A B) (polynomial.cyclotomic ↑n A)).roots.to_finset) = algebra.adjoin A {b : B | ∃ (a : ℕ+), a ∈ {n} ∧ b ^ ↑a = 1}

source

theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic (n : ℕ+) {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] [decidable_eq B] [is_domain B] (ζ : B) (hζ : is_primitive_root ζ ↑n) :

algebra.adjoin A ↑((polynomial.map (algebra_map A B) (polynomial.cyclotomic ↑n A)).roots.to_finset) = algebra.adjoin A {ζ}

source

theorem is_cyclotomic_extension.adjoin_primitive_root_eq_top (n : ℕ+) {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] [is_domain B] [h : is_cyclotomic_extension {n} A B] (ζ : B) (hζ : is_primitive_root ζ ↑n) :

algebra.adjoin A {ζ} = ⊤

source

theorem is_cyclotomic_extension.splits_X_pow_sub_one (n : ℕ+) (S : set ℕ+) (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [ne_zero ↑↑n] [H : is_cyclotomic_extension S K L] (hS : n ∈ S) :

polynomial.splits (algebra_map K L) (polynomial.X ^ ↑n - 1)

A cyclotomic extension splits X ^ n - 1 if n ∈ S and ne_zero (n : K).

source

theorem is_cyclotomic_extension.splits_cyclotomic (n : ℕ+) (S : set ℕ+) (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [ne_zero ↑↑n] [is_cyclotomic_extension S K L] (hS : n ∈ S) :

polynomial.splits (algebra_map K L) (polynomial.cyclotomic ↑n K)

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

source

theorem is_cyclotomic_extension.splitting_field_X_pow_sub_one (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [ne_zero ↑↑n] [is_cyclotomic_extension {n} K L] :

polynomial.is_splitting_field K L (polynomial.X ^ ↑n - 1)

If is_cyclotomic_extension {n} K L and ne_zero ((n : ℕ) : K), then L is the splitting field of X ^ n - 1.

source

theorem is_cyclotomic_extension.is_galois (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [ne_zero ↑↑n] [is_cyclotomic_extension {n} K L] :

is_galois K L

source

theorem is_cyclotomic_extension.splitting_field_cyclotomic (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [ne_zero ↑↑n] [is_cyclotomic_extension {n} K L] :

polynomial.is_splitting_field K L (polynomial.cyclotomic ↑n K)

If is_cyclotomic_extension {n} K L and ne_zero ((n : ℕ) : K), then L is the splitting field of cyclotomic n K.

source

@[protected, instance]

noncomputable def cyclotomic_field.algebra (n : ℕ+) (K : Type w) [field K] :

algebra K (cyclotomic_field n K)

source

@[protected, instance]

noncomputable def cyclotomic_field.field (n : ℕ+) (K : Type w) [field K] :

field (cyclotomic_field n K)

source

@[protected, instance]

noncomputable def cyclotomic_field.inhabited (n : ℕ+) (K : Type w) [field K] :

inhabited (cyclotomic_field n K)

source

def cyclotomic_field (n : ℕ+) (K : Type w) [field K] :

Type w

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

cyclotomic_field n K = (polynomial.cyclotomic ↑n K).splitting_field

source

@[protected, instance]

def cyclotomic_field.is_cyclotomic_extension (n : ℕ+) (K : Type w) [field K] [ne_zero ↑↑n] :

is_cyclotomic_extension {n} K (cyclotomic_field n K)

source

@[nolint]

noncomputable def cyclotomic_field.algebra_base (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

algebra A (cyclotomic_field n K)

If K is the fraction field of A, the A-algebra structure on cyclotomic_field n K. This is not an instance since it causes diamonds when A = ℤ.

Equations

cyclotomic_field.algebra_base n A K = ((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

source

@[protected, instance]

def cyclotomic_field.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

no_zero_smul_divisors A (cyclotomic_field n K)

source

def cyclotomic_ring (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

Type w

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

cyclotomic_ring n A K = ↥(algebra.adjoin A {b : cyclotomic_field n K | b ^ ↑n = 1})

source

@[protected, instance]

noncomputable def cyclotomic_ring.inhabited (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

inhabited (cyclotomic_ring n A K)

source

@[protected, instance]

def cyclotomic_ring.is_domain (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

is_domain (cyclotomic_ring n A K)

source

@[protected, instance]

noncomputable def cyclotomic_ring.comm_ring (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

comm_ring (cyclotomic_ring n A K)

source

noncomputable def cyclotomic_ring.algebra_base (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

algebra A (cyclotomic_ring n A K)

The A-algebra structure on cyclotomic_ring n A K. This is not an instance since it causes diamonds when A = ℤ.

Equations

cyclotomic_ring.algebra_base n A K = (algebra.adjoin A {b : cyclotomic_field n K | b ^ ↑n = 1}).algebra

source

@[protected, instance]

def cyclotomic_ring.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

no_zero_smul_divisors A (cyclotomic_ring n A K)

source

theorem cyclotomic_ring.algebra_base_injective (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

function.injective ⇑(algebra_map A (cyclotomic_ring n A K))

source

@[protected, instance]

noncomputable def cyclotomic_ring.cyclotomic_field.algebra (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

algebra (cyclotomic_ring n A K) (cyclotomic_field n K)

Equations

cyclotomic_ring.cyclotomic_field.algebra n A K = (algebra.adjoin A {b : cyclotomic_field n K | b ^ ↑n = 1}).to_algebra

source

theorem cyclotomic_ring.adjoin_algebra_injective (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

function.injective ⇑(algebra_map (cyclotomic_ring n A K) (cyclotomic_field n K))

source

@[protected, instance]

def cyclotomic_ring.cyclotomic_field.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

no_zero_smul_divisors (cyclotomic_ring n A K) (cyclotomic_field n K)

source

@[protected, instance]

def cyclotomic_ring.cyclotomic_field.is_scalar_tower (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

is_scalar_tower A (cyclotomic_ring n A K) (cyclotomic_field n K)

source

@[protected, instance]

def cyclotomic_ring.is_cyclotomic_extension (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [ne_zero ↑↑n] :

is_cyclotomic_extension {n} A (cyclotomic_ring n A K)

source

@[protected, instance]

def cyclotomic_ring.cyclotomic_field.is_fraction_ring (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [ne_zero ↑↑n] :

is_fraction_ring (cyclotomic_ring n A K) (cyclotomic_field n K)

source

theorem cyclotomic_ring.eq_adjoin_primitive_root (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] {μ : cyclotomic_field n K} (h : is_primitive_root μ ↑n) :

cyclotomic_ring n A K = ↥(algebra.adjoin A {μ})