Documentation

Mathlib.NumberTheory.Cyclotomic.Three

Third Cyclotomic Field #

We gather various results about the third cyclotomic field. The following notations are used in this file: K is a number field such that IsCyclotomicExtension {3} ℚ K, ζ is any primitive 3-rd root of unity in K, η is the element in the units of the ring of integers corresponding to ζ and λ = η - 1.

Main results #

This is a special case of the so-called Kummer's lemma (see for example [washington_cyclotomic], Theorem 5.36

theorem IsCyclotomicExtension.Rat.Three.coe_eta {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) :
.unit = .toInteger
theorem IsPrimitiveRoot.toInteger_cube_eq_one {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) :
.toInteger ^ 3 = 1
theorem IsCyclotomicExtension.Rat.Three.Units.mem {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ) :
u [1, -1, .unit, -.unit, .unit ^ 2, -.unit ^ 2]

Let u be a unit in (𝓞 K)ˣ, then u ∈ [1, -1, η, -η, η^2, -η^2].

theorem IsCyclotomicExtension.Rat.Three.eta_sq {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) :
.unit ^ 2 = -.unit - 1

We have that η ^ 2 = -η - 1.

theorem IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : ∃ (n : ), (.toInteger - 1) ^ 2 u - n) :
u = 1 u = -1

If a unit u is congruent to an integer modulo λ ^ 2, then u = 1 or u = -1.

This is a special case of the so-called Kummer's lemma.

theorem IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K) :
.toInteger - 1 x .toInteger - 1 x - 1 .toInteger - 1 x + 1

Let (x : 𝓞 K). Then we have that λ divides one amongst x, x - 1 and x + 1.

theorem IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) :
.unit ^ 2 + .unit + 1 = 0

We have that η ^ 2 + η + 1 = 0.

theorem IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K) :
x ^ 3 - 1 = (x - 1) * (x - .unit) * (x - .unit ^ 2)

We have that x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2).

theorem IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K) :
.toInteger - 1 x * (x - 1) * (x - (.unit + 1))

We have that λ divides x * (x - 1) * (x - (η + 1)).

theorem IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) {x : NumberField.RingOfIntegers K} (h : .toInteger - 1 x - 1) :
(.toInteger - 1) ^ 4 x ^ 3 - 1

If λ divides x - 1, then λ ^ 4 divides x ^ 3 - 1.

theorem IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) {x : NumberField.RingOfIntegers K} (h : .toInteger - 1 x + 1) :
(.toInteger - 1) ^ 4 x ^ 3 + 1

If λ divides x + 1, then λ ^ 4 divides x ^ 3 + 1.

theorem IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) {x : NumberField.RingOfIntegers K} (h : ¬.toInteger - 1 x) :
(.toInteger - 1) ^ 4 x ^ 3 - 1 (.toInteger - 1) ^ 4 x ^ 3 + 1

If λ does not divide x, then λ ^ 4 divides x ^ 3 - 1 or x ^ 3 + 1.