Primitive roots in cyclotomic fields #

If is_cyclotomic_extension {n} A B, we define an element zeta n A B : B that is (under certain assumptions) a primitive n-root of unity in B and we study its properties. We also prove related theorems under the more general assumption of just being a primitive root, for reasons described in the implementation details section.

Main definitions #

is_cyclotomic_extension.zeta n A B: if is_cyclotomic_extension {n} A B, than zeta n A B is an element of B that plays the role of a primitive n-th root of unity.
is_primitive_root.power_basis: if K and L are fields such that is_cyclotomic_extension {n} K L and ne_zero (↑n : K), then is_primitive_root.power_basis gives a K-power basis for L given a primitive root ζ.
is_primitive_root.embeddings_equiv_primitive_roots: the equivalence between L →ₐ[K] A and primitive_roots n A given by the choice of ζ.

Main results #

is_cyclotomic_extension.zeta_primitive_root: if is_domain B and ne_zero (↑n : B), then zeta n A B is a primitive n-th root of unity.
is_cyclotomic_extension.finrank: if irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.
is_primitive_root.norm_eq_one: If K is linearly ordered (in particular for K = ℚ), the norm of a primitive root is 1 if n is odd.
is_primitive_root.sub_one_norm_eq_eval_cyclotomic: If irreducible (cyclotomic n K), then the norm of ζ - 1 is eval 1 (cyclotomic n ℤ).

Implementation details #

zeta n A B is defined as any root of cyclotomic n A in B, that exists because of is_cyclotomic_extension {n} A B. It is not true in general that it is a primitive n-th root of unity, but this holds if is_domain B and ne_zero (↑n : B).

zeta n A B is defined using exists.some, which means we cannot control it. For example, in normal mathematics, we can demand that (zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ)) is equal to zeta p ℚ ℚ(ζₚ), as we are just choosing "an arbitrary primitive root" and we can internally specify that our choices agree. This is not the case here, and it is indeed impossible to prove that these two are equal. Therefore, whenever possible, we prove our results for any primitive root, and only at the "final step", when we need to provide an "explicit" primitive root, we use zeta.

source

noncomputable def is_cyclotomic_extension.zeta (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B] :

If B is a n-th cyclotomic extension of A, then zeta n A B is any root of cyclotomic n A in L.

Equations

is_cyclotomic_extension.zeta n A B = _.some

source

@[simp]

theorem is_cyclotomic_extension.zeta_spec (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B] :

⇑(polynomial.aeval (is_cyclotomic_extension.zeta n A B)) (polynomial.cyclotomic ↑n A) = 0

source

theorem is_cyclotomic_extension.zeta_spec' (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B] :

(polynomial.cyclotomic ↑n B).is_root (is_cyclotomic_extension.zeta n A B)

source

theorem is_cyclotomic_extension.zeta_pow (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B] :

is_cyclotomic_extension.zeta n A B ^ ↑n = 1

source

theorem is_cyclotomic_extension.zeta_primitive_root (n : ℕ+) (A : Type w) (B : Type z) [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B] [is_domain B] [ne_zero ↑↑n] :

is_primitive_root (is_cyclotomic_extension.zeta n A B) ↑n

If is_domain B and ne_zero (↑n : B) then zeta n A B is a primitive n-th root of unity.

source

@[simp]

theorem is_primitive_root.power_basis_dim {n : ℕ+} (K : Type u) {L : Type v} [field K] [field L] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ ↑n) :

(is_primitive_root.power_basis K hζ).dim = (minpoly K ζ).nat_degree

source

noncomputable def is_primitive_root.power_basis {n : ℕ+} (K : Type u) {L : Type v} [field K] [field L] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ ↑n) :

power_basis K L

The power_basis given by a primitive root ζ.

Equations

is_primitive_root.power_basis K hζ = (algebra.adjoin.power_basis _).map (((algebra.adjoin K {ζ}).equiv_of_eq ⊤ _).trans algebra.top_equiv)

source

@[simp]

theorem is_primitive_root.power_basis_gen {n : ℕ+} (K : Type u) {L : Type v} [field K] [field L] [algebra K L] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ ↑n) :

(is_primitive_root.power_basis K hζ).gen = ζ

source

noncomputable def is_primitive_root.embeddings_equiv_primitive_roots {n : ℕ+} {K : Type u} {L : Type v} (C : Type w) [field K] [field L] [comm_ring C] [algebra K L] [algebra K C] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ ↑n) [is_domain C] [ne_zero ↑↑n] (hirr : irreducible (polynomial.cyclotomic ↑n K)) :

(L →ₐ[K] C) ≃ ↥(primitive_roots ↑n C)

The equivalence between L →ₐ[K] A and primitive_roots n A given by a primitive root ζ.

Equations

is_primitive_root.embeddings_equiv_primitive_roots C hζ hirr = (is_primitive_root.power_basis K hζ).lift_equiv.trans {to_fun := λ (x : {y // ⇑(polynomial.aeval y) (minpoly K (is_primitive_root.power_basis K hζ).gen) = 0}), ⟨x.val, _⟩, inv_fun := λ (x : ↥(primitive_roots ↑n C)), ⟨x.val, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem is_primitive_root.embeddings_equiv_primitive_roots_symm_apply_apply {n : ℕ+} {K : Type u} {L : Type v} (C : Type w) [field K] [field L] [comm_ring C] [algebra K L] [algebra K C] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ ↑n) [is_domain C] [ne_zero ↑↑n] (hirr : irreducible (polynomial.cyclotomic ↑n K)) (ᾰ : ↥(primitive_roots ↑n C)) (ᾰ_1 : L) :

⇑(⇑((is_primitive_root.embeddings_equiv_primitive_roots C hζ hirr).symm) ᾰ) ᾰ_1 = ∑ (x : fin (minpoly K ζ).nat_degree), ⇑(⇑((is_primitive_root.power_basis K hζ).basis.repr) ᾰ_1) x • ↑ᾰ ^ ↑x

source

@[simp]

theorem is_primitive_root.embeddings_equiv_primitive_roots_apply_coe {n : ℕ+} {K : Type u} {L : Type v} (C : Type w) [field K] [field L] [comm_ring C] [algebra K L] [algebra K C] [is_cyclotomic_extension {n} K L] {ζ : L} (hζ : is_primitive_root ζ ↑n) [is_domain C] [ne_zero ↑↑n] (hirr : irreducible (polynomial.cyclotomic ↑n K)) (ᾰ : L →ₐ[K] C) :

↑(⇑(is_primitive_root.embeddings_equiv_primitive_roots C hζ hirr) ᾰ) = ⇑ᾰ ζ

source

theorem is_cyclotomic_extension.finrank {n : ℕ+} {K : Type u} (L : Type v) [field K] [field L] [algebra K L] [is_cyclotomic_extension {n} K L] (hirr : irreducible (polynomial.cyclotomic ↑n K)) [ne_zero ↑↑n] :

finite_dimensional.finrank K L = ↑n.totient

If irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.

source

theorem is_primitive_root.norm_eq_one {n : ℕ+} (K : Type u) {L : Type v} [field L] {ζ : L} (hζ : is_primitive_root ζ ↑n) [linear_ordered_field K] [algebra K L] (hodd : odd ↑n) :

⇑(algebra.norm K) ζ = 1

If K is linearly ordered (in particular for K = ℚ), the norm of a primitive root is 1 if n is odd.

source

theorem is_primitive_root.sub_one_norm_eq_eval_cyclotomic {n : ℕ+} {K : Type u} {L : Type v} [field L] {ζ : L} (hζ : is_primitive_root ζ ↑n) [field K] [algebra K L] [is_cyclotomic_extension {n} K L] [ne_zero ↑↑n] (h : 2 < ↑n) (hirr : irreducible (polynomial.cyclotomic ↑n K)) :

⇑(algebra.norm K) (ζ - 1) = ↑(polynomial.eval 1 (polynomial.cyclotomic ↑n ℤ))

If irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is eval 1 (cyclotomic n ℤ).