mathlib3 documentation

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 #

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} 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.

source
@[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 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
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 ↔ (∀ {n : ℕ+}, n ∈ S → (∃ (r : B), is_primitive_root r ↑n)) ∧ ∀ (x : B), x ∈ algebra.adjoin A {b : B | ∃ (n : ℕ+), n ∈ S ∧ b ^ ↑n = 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 ↔ (∀ (n : ℕ+), n ∈ S → (∃ (r : B), is_primitive_root r ↑n)) ∧ algebra.adjoin A {b : B | ∃ (n : ℕ+), n ∈ S ∧ b ^ ↑n = 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), is_primitive_root r ↑n) ∧ ∀ (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 the image of A in B equals B.

source
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 the image of A in B equals B.

source
theorem is_cyclotomic_extension.singleton_zero_of_bot_eq_top {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] (h : ⊥ = ⊤) :
is_cyclotomic_extension ∅ A B

If (⊥ : subalgebra A B) = ⊤, then is_cyclotomic_extension ∅ 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] (h : function.injective ⇑(algebra_map B C)) :
is_cyclotomic_extension (S ∪ T) A C

Transitivity of cyclotomic extensions.

source
theorem is_cyclotomic_extension.subsingleton_iff (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [subsingleton B] :
is_cyclotomic_extension S A B ↔ S = ∅ ∨ S = {1}
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.of_union_of_dvd {n : ℕ+} {S : set ℕ+} (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] (h : ∀ (s : ℕ+), s ∈ S → n ∣ s) (hS : S.nonempty) [H : is_cyclotomic_extension S A B] :
is_cyclotomic_extension (S ∪ {n}) A 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.

source
theorem is_cyclotomic_extension.iff_union_of_dvd {n : ℕ+} {S : set ℕ+} (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] (h : ∀ (s : ℕ+), s ∈ S → n ∣ s) (hS : S.nonempty) :
is_cyclotomic_extension S A B ↔ is_cyclotomic_extension (S ∪ {n}) A B

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.

source
theorem is_cyclotomic_extension.iff_union_singleton_one (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] :
is_cyclotomic_extension S A B ↔ is_cyclotomic_extension (S ∪ {1}) A B

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

source
theorem is_cyclotomic_extension.singleton_one_of_bot_eq_top {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] (h : ⊥ = ⊤) :
is_cyclotomic_extension {1} A B

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

source
theorem is_cyclotomic_extension.singleton_one_of_algebra_map_bijective {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] (h : function.surjective ⇑(algebra_map A B)) :
is_cyclotomic_extension {1} A B

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

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

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

source
@[protected]
theorem is_cyclotomic_extension.ne_zero (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [h : is_cyclotomic_extension {n} A B] [is_domain B] :
ne_zero ↑↑n
source
@[protected]
theorem is_cyclotomic_extension.ne_zero' (n : ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B] [is_domain B] :
ne_zero ↑↑n
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
@[protected]
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₁ : finite ↥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] [finite ↥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] [finite ↥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) [finite ↥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 {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) :
algebra.adjoin A ((polynomial.cyclotomic ↑n A).root_set B) = algebra.adjoin A {b : B | ∃ (a : ℕ+), a ∈ {n} ∧ b ^ ↑a = 1}
source
theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] {n : ℕ+} [is_domain B] {ζ : B} (hζ : is_primitive_root ζ ↑n) :
algebra.adjoin A ((polynomial.cyclotomic ↑n A).root_set B) = algebra.adjoin A {ζ}
source
theorem is_cyclotomic_extension.adjoin_primitive_root_eq_top {A : Type u} {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] {n : ℕ+} [is_domain B] [h : is_cyclotomic_extension {n} A B] {ζ : B} (hζ : is_primitive_root ζ ↑n) :
algebra.adjoin A {ζ} = ⊤
source
theorem is_primitive_root.adjoin_is_cyclotomic_extension (A : Type u) {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] {ζ : B} {n : ℕ+} (h : is_primitive_root ζ ↑n) :
is_cyclotomic_extension {n} A ↥(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] [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.

source
theorem is_cyclotomic_extension.splits_cyclotomic {n : ℕ+} {S : set ℕ+} (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [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] [is_cyclotomic_extension {n} K L] :
polynomial.is_splitting_field K L (polynomial.X ^ ↑n - 1)

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

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

Any two n-th cyclotomic extensions are isomorphic.

Equations
source
theorem is_cyclotomic_extension.is_galois (n : ℕ+) (K : Type w) (L : Type z) [field K] [field L] [algebra K L] [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] [is_cyclotomic_extension {n} K L] :
polynomial.is_splitting_field K L (polynomial.cyclotomic ↑n K)

If is_cyclotomic_extension {n} K L, 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
Instances for cyclotomic_field
source
@[protected, instance]
def cyclotomic_field.char_zero (n : ℕ+) (K : Type w) [field K] [char_zero K] :
char_zero (cyclotomic_field n K)
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
@[protected, nolint, instance]
noncomputable def cyclotomic_field.algebra_base (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [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.

Equations
source
@[protected, instance]
noncomputable def cyclotomic_field.algebra' (n : ℕ+) (K : Type w) [field K] {R : Type u_1} [comm_ring R] [algebra R K] :
algebra R (cyclotomic_field n K)
Equations
source
@[protected, instance]
def cyclotomic_field.is_scalar_tower (n : ℕ+) (K : Type w) [field K] {R : Type u_1} [comm_ring R] [algebra R K] :
is_scalar_tower R K (cyclotomic_field n K)
source
@[protected, instance]
def cyclotomic_field.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [algebra A K] [is_fraction_ring A K] :
no_zero_smul_divisors A (cyclotomic_field n K)
source
@[nolint]
def cyclotomic_ring (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [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
source
@[protected, instance]
noncomputable def cyclotomic_ring.inhabited (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [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] [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] [algebra A K] [is_fraction_ring A K] :
comm_ring (cyclotomic_ring n A K)
source
@[protected, instance]
noncomputable def cyclotomic_ring.algebra_base (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [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.

Equations
source
@[protected, instance]
def cyclotomic_ring.no_zero_smul_divisors (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [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] [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] [algebra A K] [is_fraction_ring A K] :
algebra (cyclotomic_ring n A K) (cyclotomic_field n K)
Equations
source
theorem cyclotomic_ring.adjoin_algebra_injective (n : ℕ+) (A : Type u) (K : Type w) [comm_ring A] [field K] [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] [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] [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] [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] [algebra A K] [is_fraction_ring A K] [is_domain A] [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] [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 {μ})
source
theorem is_alg_closed.is_cyclotomic_extension (S : set ℕ+) (K : Type w) [field K] [is_alg_closed K] (h : ∀ (a : ℕ+), a ∈ S → ne_zero ↑↑a) :
is_cyclotomic_extension S K K

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

source
@[protected, instance]
def is_alg_closed_of_char_zero.is_cyclotomic_extension (K : Type w) [field K] [is_alg_closed K] [char_zero K] (S : set ℕ+) :
is_cyclotomic_extension S K K