mathlib documentation

number_theory.cyclotomic.basic

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 #

Main results #

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. 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] [algebra A B] :
Prop

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 of this typeclass
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}
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 .

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.

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.

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

If is_cyclotomic_extension {1} A B, then A = B.

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] :

Transitivity of cyclotomic extensions.

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.

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.

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] :
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] :

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] [algebra K L] [h : number_field K] [fintype S] [is_cyclotomic_extension S K L] :

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

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) [fintype S] [comm_ring C] [algebra K C] [is_domain C] [is_cyclotomic_extension S K C] :

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

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) :
theorem is_primitive_root.adjoin_is_cyclotomic_extension (A : Type u) {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] [is_domain B] {ζ : B} {n : ℕ+} (h : is_primitive_root ζ n) :
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) :

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

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) :

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

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

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] :

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

@[protected, instance]
noncomputable def cyclotomic_field.algebra (n : ℕ+) (K : Type w) [field 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] :
@[protected, instance]
@[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] :

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
@[protected, instance]
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
Instances for cyclotomic_ring
@[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] :
@[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] :
@[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] :
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] :

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

Equations
@[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] :
@[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] :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
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) :

Algebraically closed fields are cyclotomic extensions over themselves.