Squarefree Pure Cubic Integer Ring
Abstract
A squarefree pure cubic radicand makes the displayed order the full integer ring.
Theorem 1.1 (Maximality of the cubic suborder).
Lean statement: D5/S3/Arith/Lattices/PureCubicSquarefreeMaximality.pure_cubic_squarefree_maximality
Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/PureCubicSquarefreeMaximality.pure_cubic_squarefree_maximality (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let K have a rational power basis generated by theta, of dimension three, with theta cubed equal to B = 1 + 9a for an integer a. Assume B is squarefree. Put beta = (1 + theta + theta squared)/3.
Every element of K integral over the integers is an integer linear combination of 1, theta, and beta. The reverse inclusion holds because these generators form an integral subring, so their span is the full ring of integers of K.
The power-basis discriminant clears denominators using 27 times B squared. At each prime dividing B, the polynomial X cubed minus B is Eisenstein because B is squarefree. Eisenstein integrality removes that prime from a multiple lying in the order. Three-saturation removes the remaining factors of three.