Simple-Prime Saturation of a Pure Cubic Order
Abstract
A simple prime divisor of a pure cubic radicand saturates the integral order locally.
Theorem 1.1 (Integral elements at a simple divisor).
Lean statement: D5/S3/Arith/Lattices/PureCubicPrimeSaturation.pure_cubic_prime_saturation
Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/PureCubicPrimeSaturation.pure_cubic_prime_saturation (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let K have a rational cubic power basis generated by theta, with theta cubed equal to B = 1 + 9a. Put beta = (1 + theta + theta squared)/3 and let A be the integer span of 1, theta, and beta.
For a prime p dividing B exactly once, every integral element z of K with p times z in A already lies in A. Other prime factors of B may occur repeatedly.
The polynomial X cubed minus B is Eisenstein at p. Multiplying the order membership by three places p times (3z) in the ring generated by theta. Eisenstein integrality puts 3z there, and the previously established three-saturation of A then gives z in A.