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

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.

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

If is_cyclotomic_extension {1} A B, then the image of A in B equals 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] (h : function.injective (algebra_map 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.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] :

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

If (⊥ : subalgebra 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] [algebra A B] {C : Type u_1} [comm_ring C] [algebra A C] [h : is_cyclotomic_extension S A 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] [algebra A B] [h : is_cyclotomic_extension {n} A B] [is_domain B] :
@[protected]
@[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] :

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

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

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

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

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

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

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]
@[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]

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