Primitive roots in cyclotomic fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. If is_cyclotomic_extension {n} A B, we define an element zeta n A B : B that is a primitive nth-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 a primitive n-th root of unity in B.
• is_primitive_root.power_basis: if K and L are fields such that is_cyclotomic_extension {n} K L, 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_spec: 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 irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of a primitive root is 1 if n ≠ 2.
• is_primitive_root.sub_one_norm_eq_eval_cyclotomic: if irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is eval 1 (cyclotomic n ℤ), for a primitive root ζ. We also prove the analogous of this result for zeta.
• is_primitive_root.pow_sub_one_norm_prime_pow_ne_two : if irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) p ^ (k - s + 1) ≠ 2. See the following lemmas for similar results. We also prove the analogous of this result for zeta.
• is_primitive_root.sub_one_norm_prime_ne_two : if irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p. We also prove the analogous of this result for zeta.
• is_primitive_root.embeddings_equiv_primitive_roots: the equivalence between L →ₐ[K] A and primitive_roots n A given by the choice of ζ.

Implementation details #

zeta n A B is defined as any primitive root of unity in B, - this must exist, by definition of is_cyclotomic_extension. It is not true in general that it is a root of cyclotomic n B, 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.