Arithmetic invariants of the cubic of discriminant −23

Let K be generated by an algebraic integer θ with minimal polynomial X³ - X² + 1. Its polynomial discriminant is the squarefree integer −23, so the index formula forces ℤ[θ] = 𝓞 K and discr K = −23. The degree and discriminant sign then give signature (1, 1), unit rank one, and intrinsic label prefix 3.1.23. The field is not Galois and has no proper intermediate fields. The discriminant is below the cubic Minkowski threshold, so 𝓞 K is a principal ideal domain and the class number is 1.

These computations provide the field discriminant and signature used to certify units by excluding competing minimal polynomials. No integral-basis or field-discriminant assumption is made.

References

• D. A. Marcus, Number Fields, Chapters 2–4, for the index–discriminant method.

@[simp]

theorem TauCeti.NumberField.Cubic23.discr_polynomial : (Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1).discr = -23

The discriminant of the defining cubic is −23.

theorem TauCeti.NumberField.Cubic23.finrank_eq_three {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : Module.finrank ℚ K = 3

The field generated by the defining cubic has degree three.

theorem TauCeti.NumberField.Cubic23.index_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : IntegralPrimitiveElement.index ⟨θ, hgen⟩ = 1

The defining generator has index one in the full ring of integers.

theorem TauCeti.NumberField.Cubic23.adjoin_eq_top {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : ℤ[θ] = ⊤

The powers of θ span the full ring of integers as a ℤ-algebra.

theorem TauCeti.NumberField.Cubic23.isMonogenic {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : IsMonogenic K

The cubic field is monogenic, generated integrally by θ.

theorem TauCeti.NumberField.Cubic23.discr_eq_neg_twenty_three {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : NumberField.discr K = -23

The signed field discriminant is −23.

theorem TauCeti.NumberField.Cubic23.nrComplexPlaces_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : NumberField.InfinitePlace.nrComplexPlaces K = 1

There is exactly one complex infinite place: the discriminant −23 is negative.

theorem TauCeti.NumberField.Cubic23.nrRealPlaces_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : NumberField.InfinitePlace.nrRealPlaces K = 1

There is exactly one real infinite place.

theorem TauCeti.NumberField.Cubic23.hasLMFDBIntrinsicLabel {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : HasLMFDBIntrinsicLabel K 3 1 23

The intrinsic label prefix is 3.1.23.

theorem TauCeti.NumberField.Cubic23.isPrincipalIdealRing {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

The ring of integers is a principal ideal domain: the discriminant −23 is below the cubic Minkowski threshold 49 of isPrincipalIdealRing_of_finrank_eq_three_of_natAbs_discr_le_forty_nine.

theorem TauCeti.NumberField.Cubic23.classNumber_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : NumberField.classNumber K = 1

The class number is 1.

theorem TauCeti.NumberField.Cubic23.units_rank_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : NumberField.Units.rank K = 1

The unit group has rank one.

theorem TauCeti.NumberField.Cubic23.intermediateField_eq_bot_or_eq_top {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (E : IntermediateField ℚ K) : E = ⊥ ∨ E = ⊤

The cubic field has no intermediate fields other than the base and the whole field.

theorem TauCeti.NumberField.Cubic23.not_isGalois {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 3 - Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : ¬IsGalois ℚ K

The cubic field is not Galois over ℚ: its signature is mixed.