Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The prime-norm cubic field

Abstract

A prime Eisenstein factor gives a cubic without rational roots and a real cyclic splitting field of degree three.

Theorem 1.1 (No nonzero integer projective zero).

Lean statement: D5/S3/Factorization/QuadraticIdeals/GoldenCubicPrimeNormField.prime_norm_cubic_no_integer_projective_zero

Proof. Machine-checked in Lean as D5/S3/Factorization/QuadraticIdeals/GoldenCubicPrimeNormField.prime_norm_cubic_no_integer_projective_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let pi be a nonzero Eisenstein integer whose principal ideal is prime and which is coprime to its conjugate. Put a = pi.re, b = pi.im, A = a squared minus b squared, and D = 2ab minus b squared. For every integer pair (u,v) other than (0,0), the homogeneous cubic A u cubed - 3D u squared v + 3(D-A)u v squared + A v cubed is nonzero. At the prime ideal generated by pi, a zero would equate the valuations of pi squared times (u+v omega) cubed and its conjugate. The two pi factors contribute incompatible residues modulo three.

Theorem 1.2 (The cubic is irreducible and its splitting field is real cyclic).

Lean statement: D5/S3/Factorization/QuadraticIdeals/GoldenCubicPrimeNormField.golden_cubic_prime_norm_field

Proof. Machine-checked in Lean as D5/S3/Factorization/QuadraticIdeals/GoldenCubicPrimeNormField.golden_cubic_prime_norm_field (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let pi satisfy the same nonzero, prime-ideal, and conjugate-coprime hypotheses, and let its Eisenstein norm equal a natural number P. With A and D as above, the polynomial over Q with cubic coefficients (A, -3D, 3(D-A), A) is irreducible. Its splitting field has degree three over Q, has cyclic Galois group, and is totally real. The discriminant of the corresponding integer cubic is 81 times P to the fourth power.

A rational root would clear denominators to a nonzero integer projective zero. If r is one root of the cubic, every root is r, 1/(1-r), or (r-1)/r; hence a single root generates the splitting field. Opposite signs at zero and one give a real root between them, and the two transformed roots are real as well. The discriminant follows by expanding the cubic formula and using the Eisenstein norm identity.

References