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

• IsCyclotomicExtension.Rat.Three.Units.mem: Given a unit u : (𝓞 K)ˣ, we have that u ∈ {1, -1, η, -η, η^2, -η^2}.

• IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent: Given a unit u : (𝓞 K)ˣ, if u is congruent to an integer modulo 3, then u = 1 or u = -1.

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 = hζ.toInteger

theorem IsPrimitiveRoot.toInteger_cube_eq_one {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑3) : hζ.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 : ℤ), (hζ.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) : hζ.toInteger - 1 ∣ x ∨ hζ.toInteger - 1 ∣ x - 1 ∨ hζ.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) : hζ.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 : hζ.toInteger - 1 ∣ x - 1) : (hζ.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 : hζ.toInteger - 1 ∣ x + 1) : (hζ.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 : ¬hζ.toInteger - 1 ∣ x) : (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1

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