Documentation

TauCeti.NumberTheory.NumberField.WorkedExamples.Cubic23.Reciprocal

The cubic field of discriminant −23 as the field of X³ - X + 1 #

The invariants of the cubic field of discriminant −23 are computed in TauCeti.NumberTheory.NumberField.WorkedExamples.Cubic23.Invariants from an integral generator θ with minimal polynomial X³ - X² + 1. The same field is also presented by the cubic X³ - X + 1, whose roots are the reciprocals of the roots of X³ - X² + 1: if r³ - r + 1 = 0 then r (r² - 1) = -1, so r⁻¹ = 1 - r² is an algebraic integer, and it is a root of X³ - X² + 1. This file supplies that generator, so that the invariants of Cubic23.Invariants (discriminant −23, signature (1, 1), class number one, unit rank one) apply to a number field generated by a root of X³ - X + 1. This is the field factor of the étale algebra ℚ[X] ⧸ (X³ - X + 1) attached to the elliptic curve y² = x³ - x + 1.

Main results #

source
theorem TauCeti.NumberField.Cubic23.irreducible_polynomial :
Irreducible (Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1)

The defining cubic X³ - X² + 1 is irreducible over ℤ: it has no root modulo 2, so no integral root, and by Gauss's lemma irreducibility over ℚ descends to ℤ.

source
theorem TauCeti.NumberField.Cubic23.irreducible_X_pow_three_sub_X_add_one :
Irreducible (Polynomial.X ^ 3 - Polynomial.X + 1)

The cubic X³ - X + 1 is irreducible over ℚ: it has no root modulo 2, so no integral root.

source
theorem TauCeti.NumberField.Cubic23.exists_minpoly_eq_and_adjoin_eq_top_of_root {K : Type u_1} [Field K] [NumberField K] {r : K} (hr : r ^ 3 - r + 1 = 0) (hgen : ℚ[r] = ⊤) :
∃ (θ : NumberField.RingOfIntegers K), minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1 ∧ ℚ[↑θ] = ⊤

A root of X³ - X + 1 presents the cubic field of discriminant −23. If a root r of X³ - X + 1 generates the number field K, then its reciprocal r⁻¹ = 1 - r² is an algebraic integer of K with minimal polynomial X³ - X² + 1 over ℤ, which also generates K.