A Local-to-Global Principal-Ideal Gap

Abstract

The norm-two ideal is principal after localization at every nonzero prime but is not principal globally, giving an explicit positive local-to-global defect.

Theorem 1.1 (The norm-two ideal is locally principal but globally nonprincipal).

$$\begin{gathered} (\forall p:\mathrm{Ideal}\left(\mathrm{QuadraticOrder}\right),(\mathrm{IsPrime}\left(p\right)\wedge p\ne 0)\Rightarrow \mathrm{IsPrincipal}\left(\mathrm{IdealMap}\left(normTwoIdeal,\mathrm{LocalizationAtPrime}\left(\mathrm{QuadraticOrder},p\right)\right)\right))\wedge \\ \neg \mathrm{IsPrincipal}\left(normTwoIdeal\right)\wedge \\ (\exists w:\mathrm{positiveHasseDefect}\left(\mathrm{PrincipalIdealPredicate}\left(\mathrm{QuadraticOrder}\right),\mathrm{NonzeroPrimeLocalizationPrincipalPredicate}\left(\mathrm{QuadraticOrder}\right)\right),\mathrm{UnderlyingIdeal}\left(w\right)=normTwoIdeal). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The carrier and ideal are the frozen QuadraticOrder and normTwoIdeal from the adjacent norm-two theorem. Thus the witness is exactly the ideal generated by 2 and 1 + sqrt(-5), not a replacement construction.

At a prime containing 2, the element 3 lies outside the prime and becomes invertible. The identity (1 + sqrt(-5))(1 - sqrt(-5)) = 3 times 2 then makes the localized ideal principal with generator 1 + sqrt(-5). At a prime not containing 2, the image of 2 is a unit, so the localized ideal is the unit ideal.

If the global ideal had generator x, its element norm would divide both 4 and 6, hence would equal 2 because x cannot be a unit. This would give x.re squared plus 5 times x.im squared equal to 2, which has no integer solution. The local proofs and global obstruction are assembled into the displayed positive defect witness whose underlying ideal is normTwoIdeal. This closes atom generic-residual-1798510a7ffd337203122ce61979bcb8bf790bba93f6b013f118ed868eb5a7c0.

References

• Truth anchor: D5/S3/Factorization/QuadraticIdeals/NormTwoIdealLocalGlobalGap.norm_two_ideal_local_global_gap
• Dependency: D5/S3/Factorization/QuadraticIdeals/NormTwoIdeal