Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Ideal Factorization of Odd Eisenstein Factors

Abstract

Every odd oriented Eisenstein factor has an explicit ideal product indexed by the prime factors of its scalar norm.

Theorem 1.1 (The oriented ideal is the product of its explicit prime-indexed factors).

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

Source. Repository-derived.

Commentary.

For odd b, eta is -2 + b omega, B is b squared plus 2b plus 4, and the factor at p is the ideal generated by eta and p. The quotient of the Eisenstein order by that factor is Z/pZ, so its norm is p.

Modulo eta, the product of those factors is generated by the prime factorization of B and therefore vanishes. Its absolute ideal norm is B, the same as the norm of the principal ideal of eta. Containment and norm equality yield the ideal identity.

This statement concerns ideals for every odd b. Primary generators and original-depth exponents require additional results.

References