Non-principal ideal in Dedekind domain

Stream: Is there code for X?

[Junyan Xu]

I'm sure someone has done this (indeed various nontrivial class groups have been computed in Lean), but what's the easiest way to produce an example with what we have in mathlib?

import Mathlib
def R : Type := sorry
instance : CommRing R := sorry
instance : IsDedekindDomain R := sorry
example : ∃ I : Ideal R, ¬ I.IsPrincipal := sorry

Context: I need it for this counterexample.

[Riccardo Brasca]

It's a bit ridiculous, but the API of cyclotomic fields and of the norm is well developed, so I think the usual proof for the 23-th cyclotomic field should be doable.

[Riccardo Brasca]

The only reason I am proposing cyclotomic fields rather than quadratic fields is that the API is probably better.

[Edison Xie]

Riccardo Brasca said:

The only reason I am proposing cyclotomic fields rather than quadratic fields is that the API is probably better.

This will be fixed by the series of PR on quadratic algebra I’m currently doing! :-)

[Kevin Buzzard]

It's not hard to prove that there's no solution to $a^2+5b^2=\pm2$ in integers so I would be tempted to try $\Z[\sqrt{-5}]\supseteq(2,1+\sqrt{-5})$ despite these API claims.

[Junyan Xu]

Yeah, I think that's probably the easiest. We could use Zsqrtd (-5) to do the computations (with Ideal.absNorm_span_singleton) and show it's isomorphic to NumberField.RingOfIntegers in ℚ(√-5) to show it's a Dedekind domain.

[Junyan Xu]

Okay IsIntegralClosure.isDedekindDomain should make our life a lot easier. We could do this $\mathbb{R}[X,Y]/(X^2+Y^2-1)$ example as well. Or the coordinate ring of an elliptic curve, which we already showed to contain non-principal ideals.

[Junyan Xu]

I've worked out a proof to show the CoordinateRing of an elliptic curve is integrally closed. It works as follows: rather than using FunctionField it would be more convenient to use K(X)[Y]/W(X,Y) as a model of the fraction ring of the coordinate ring K[X][Y]/W(X,Y). An arbitrary element of the function field can be written as p+qY with p,q in K(X). (Probably we should use QuadraticAlgebra for this and CoordinateRing.) We want to show that if p+qY is integral over the coordinate ring (equivalently, over K[X]) then p and q are actually in K[X]. p+qY being integral implies that the minimal polynomial over K(X) has coefficients in K[X], i.e. the trace and norm of p+qY are in K[X]. The discriminant of the minpoly is Tr²-4N which must also be in K[X] and can be computed to equal q² * W.twoTorsionPolynomial, so if twoTorsionPolynomial has no double root then q must be in K[X], then the norm being in K[X] means that p satisfies a monic quadratic equation with coefficients in K[X], which implies that p is integral too. (We have Tr(p+qY)=2p-(a₁X+a₃)q; See norm_smul_basis for N(p+qY).) Since the discriminant of twoTorsionPolynomial is 16 times the discriminant of the elliptic curve, if the characteristic is not 2 then we're done.

In characteristic 2 we have Tr(p+qY)=(a₁X+a₃)q so if a₁=0 then a₃≠0 (since Δ ≠ 0) therefore q ∈ K[X] and we are done. In the a₁≠0 case, it's most convenient to make a coordinate change so that the Weierstrass equation becomes Y²+XY=X³+a₂X²+a₆ (first replace X by (X+a₃)/a₁, then replace Y by Y+a₄; this is the ordinary (non-supersingular) case in char 2, see Silverman A1.1(c)). Then a₆ = Δ ≠ 0, Xq = Tr(p+qY) ∈ K[X] and p² + Xpq + (X³+a₂X²+a₆)q² = N(p+qY) ∈ K[X]. Multiplying the latter expression by X² we see that (Xp)² + X(Xq)(Xp) + (X³+a₂X²+a₆)(Xq)² ∈ X²K[X], so Xp satisfies a monic quadratic equation with coefficients in K[X] and thus Xp ∈ K[X]. Write Xp = p₀ + p₁X and Xq = q₀ + q₁X in K[X]/X²K[X] with p₀,p₁,q₀,q₁ ∈ K, then we get p₀² + Xp₀q₀ + a₆q₀² = 0 in K[X]/X²K[X], i.e. p₀q₀ = 0 and p₀² + a₆q₀² = 0, so p₀ = q₀ = 0, i.e. X divides both Xp and Xq in K[X], so p and q are in fact in K[X].

I'll probably make this a project in an upcoming workshop. If anyone has code that helps towards this please let me know.