mathlib documentation

number_theory.cyclotomic.rat

Ring of integers of p ^ n-th cyclotomic fields #

We gather results about cyclotomic extensions of . In particular, we compute the ring of integers of a p ^ n-th cyclotomic extension of .

Main results #

theorem is_cyclotomic_extension.rat.discr_prime_pow_ne_two' {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K] (hζ : is_primitive_root ζ (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
algebra.discr ((is_primitive_root.sub_one_power_basis hζ).basis) = (-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

The discriminant of the power basis given by ζ - 1.

theorem is_cyclotomic_extension.rat.discr_odd_prime' {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p} K] (hζ : is_primitive_root ζ p) (hodd : p 2) :
theorem is_cyclotomic_extension.rat.discr_prime_pow' {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :
algebra.discr ((is_primitive_root.sub_one_power_basis hζ).basis) = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

The discriminant of the power basis given by ζ - 1. Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. It is useful only to have a uniform result. See also is_cyclotomic_extension.rat.discr_prime_pow_eq_unit_mul_pow'.

If p is a prime and is_cyclotomic_extension {p ^ k} K L, then there are u : ℤˣ and n : ℕ such that the discriminant of the power basis given by ζ - 1 is u * p ^ n. Often this is enough and less cumbersome to use than is_cyclotomic_extension.rat.discr_prime_pow'.

If K is a p ^ k-th cyclotomic extension of , then (adjoin ℤ {ζ}) is the integral closure of in K.

The integral closure of inside cyclotomic_field (p ^ k) ℚ is cyclotomic_ring (p ^ k) ℤ ℚ.

noncomputable def is_primitive_root.adjoin_equiv_ring_of_integers {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :

The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p ^ k-th root of unity and K is a p ^ k-th cyclotomic extension of .

Equations
noncomputable def is_primitive_root.integral_power_basis {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :

The integral power_basis of 𝓞 K given by a primitive root of unity, where K is a p ^ k cyclotomic extension of .

Equations
@[simp]
theorem is_primitive_root.integral_power_basis_gen {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :
@[simp]
theorem is_primitive_root.integral_power_basis_dim {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :

The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p-th root of unity and K is a p-th cyclotomic extension of .

Equations
noncomputable def is_primitive_root.integral_power_basis' {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p} K] (hζ : is_primitive_root ζ p) :

The integral power_basis of 𝓞 K given by a primitive root of unity, where K is a p-th cyclotomic extension of .

Equations
@[simp]
theorem is_primitive_root.integral_power_basis'_gen {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p} K] (hζ : is_primitive_root ζ p) :
@[simp]
theorem is_primitive_root.power_basis_int'_dim {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p} K] (hζ : is_primitive_root ζ p) :
noncomputable def is_primitive_root.sub_one_integral_power_basis {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :

The integral power_basis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic extension of .

Equations
@[simp]
theorem is_primitive_root.sub_one_integral_power_basis_gen {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :

The integral power_basis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic extension of .

Equations
@[simp]
theorem is_primitive_root.sub_one_integral_power_basis'_gen {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p} K] (hζ : is_primitive_root ζ p) :