# mathlib3documentation

number_theory.cyclotomic.rat

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 #

• is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow: if K is a p ^ k-th cyclotomic extension of ℚ, then (adjoin ℤ {ζ}) is the integral closure of ℤ in K.
• is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow: the integral closure of ℤ inside cyclotomic_field (p ^ k) ℚ is cyclotomic_ring (p ^ k) ℤ ℚ.
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ζ : (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
= (-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)] [ K] (hζ : p) (hodd : p 2) :
= (-1) ^ ((p - 1) / 2) * p ^ (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ζ : (p ^ k)) :
= (-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'.

theorem is_cyclotomic_extension.rat.discr_prime_pow_eq_unit_mul_pow' {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ k} K] (hζ : (p ^ k)) :
(u : ˣ) (n : ), = u * p ^ n

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

theorem is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : (p ^ k)) :
K

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

theorem is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : p) :
K

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

@[simp]
theorem is_primitive_root.adjoin_equiv_ring_of_integers_apply {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : (p ^ k)) (ᾰ : {ζ})) :
@[simp]
theorem is_primitive_root.adjoin_equiv_ring_of_integers_symm_apply {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : (p ^ k)) (ᾰ : ) :
= 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ζ : (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
@[protected, instance]

The ring of integers of a p ^ k-th cyclotomic extension of ℚ is a cyclotomic extension.

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ζ : (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ζ : (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ζ : (p ^ k)) :
@[simp]
theorem is_primitive_root.adjoin_equiv_ring_of_integers'_apply {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : p) (ᾰ : {ζ})) :
noncomputable def is_primitive_root.adjoin_equiv_ring_of_integers' {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : p) :

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

Equations
@[simp]
theorem is_primitive_root.adjoin_equiv_ring_of_integers'_symm_apply {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : p) (ᾰ : ) :
= K _)
@[protected, instance]
def is_cyclotomic_extension.ring_of_integers' {p : ℕ+} {K : Type u} [field K] [char_zero K] [hp : fact (nat.prime p)] [ K] :

The ring of integers of a p-th cyclotomic extension of ℚ is a cyclotomic extension.

noncomputable def is_primitive_root.integral_power_basis' {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : 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 : K] (hζ : 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 : K] (hζ : 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ζ : (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ζ : (p ^ k)) :
noncomputable def is_primitive_root.sub_one_integral_power_basis' {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : p) :

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 : K] (hζ : p) :