GaussianRat

Stream: Is there code for X?

[Geoffrey Irving]

Do we have $\mathbb{Q}[i]$ (the rational equivalent of GaussianInt)?

[Geoffrey Irving]

Oops, seems I don't know the syntax for inline latex (fixed).

[Ruben Van de Velde]

Double dollars

[Johan Commelin]

Not in mathlib, afaik. But the VU (A'dam) project had quad_ring for quadratic number fields.

[Geoffrey Irving]

I'll just spell it out as tuples for now; I need only a tiny bit of it.

[Eric Wieser]

CliffordAlgebra (-.sq : QuadraticForm ℚ ℚ), but it's computationally awful :upside_down:

[Geoffrey Irving]

I think ℚ × ℚ is easier for the moment. Mostly I want to take linear combinations. :)

[Eric Wieser]

Also discussed here:

Eric Wieser said:

A question for the community: is it time to merge some subset of docs#ZSqrtd and docs#Complex and docs#GaussianInt and docs#Unitization and docs#TrivSqZeroExt into a single structure that would work here too for $\mathbb{Q}[\sqrt{d}]$?

[Riccardo Brasca]

I think that independently of the spell we choose we want a characteristic predicate rather than an explicit definition.

[Kevin Buzzard]

Well that will raise an interesting question because these objects have a nontrivial automorphism so are not the solution to a (certain kind of) universal problem. You can be isomorphic to $\mathbb{Q}(i)$ in two ways, and for all most of the other characteristic predicates we have (e.g. localisations in algebra, and limits/colimits in category theory) they are characterising something rigid (i.e. no nontrivial automorphisms).

[Kevin Buzzard]

You can do the ugly thing and choose an $i$ but this is like choosing a basis -- this is breaking symmetry and proving certain theorems will be harder.

[Geoffrey Irving]

The type class could pick out i.

[Adam Topaz]

Riccardo Brasca said:

I think that independently of the spell we choose we want a characteristic predicate rather than an explicit definition.

+1 for this (and similarly for everything else in mathlib)

[Adam Topaz]

I'm starting to think more and more that literally everything we define should have a "characteristic predicate" of some sort

[Johan Commelin]

@Kevin Buzzard We already have a predicate for algebraic closures, right?

[Adam Topaz]

docs#IsAlgebraicClosure

[Kevin Buzzard]

That's a 404 but you might be right (I changed "all" to "most" :-) )

[Adam Topaz]

I guess we have IsAlgebraic and AlgebraicallyClosed

[Kevin Buzzard]

The issue will be that the proposition isGaussianRat will be a proposition but it won't be as useful as you think (e.g. you won't be able to get a map to the complexes because you'll have to choose an $i$) and isPointedGaussianRatwill involve a choice so won't be a Prop and there will be a risk of diamonds.

[Adam Topaz]

But something can surely be done since you can characterize the Gaussian rats as the unique extension of $$\Q$$ of degree 2 which contains some element whose square is $-1$.

[Michael Stoll]

Why should $\mathbb{Q}(i)$ get preferential treatment among all nontrivial number fields? (Also, we do have CylcotomicField 4 Rat.)

[Adam Topaz]

It shouldn't.

[Michael Stoll]

So there should be predicates for each other number field as well? :smile:

[Adam Topaz]

I'm claiming that the answer is yes, for the explicit number fields

[Michael Stoll]

What is an "explicit number field"?

[Adam Topaz]

I knew you were going to ask that :)

[Adam Topaz]

And I don't have an answer

[Michael Stoll]

$\mathbb{Q}(\sqrt[3]{2})$, $\mathbb{Q}(\sqrt{\sqrt{3}+5})$, ...

[Adam Topaz]

I guess given some field $K$ and some irreducible poly $f$ you could make a characteristic predicate for an extension of $K$ generated by a root of $f$.

[Michael Stoll]

"There exists a $\mathbb{Q}$-algebra isomorphism with $\mathbb{Q}[X]/\langle f \rangle$".

[Adam Topaz]

Yeah something like that

[Adam Topaz]

But then the point is that given a field with such an instance the only things you will ever be able to say about such a field must be compatible with that algebra iso, and you couldn’t use any other implementation details

[Junyan Xu]

docs#IsAdjoinRoot is apparently not well known enough ...

[Adam Topaz]

But that has data!

[Adam Topaz]

so it does "choose a basis"

[Adam Topaz]

I'm sure now Kevin will contest the use of "Is" in "IsAdjointRoot"

[Kevin Buzzard]

Yes I think it's a great shame that there are type-valued declarations called Is..., with IsROrC being the canonical one I complain about.

[Yaël Dillies]

Kevin Buzzard said:

You can do the ugly thing and choose an $i$ but this is like choosing a basis -- this is breaking symmetry and proving certain theorems will be harder.

Okay but you could have a type synonym OtherC which has an IsROrC instance where I := -I. Similarly, you could have synonyms which change the non-canonical choice of basis.

[Kevin Buzzard]

Yes but these ideas which people have about this topic just sound to me like it's 1900 and people are saying "you don't need vector spaces, you can just use R^n and carry around matrices". Yes you can do this, I'm just saying it's a lousy idea! However I've never managed to explicitly give an example of this because we're nowhere near the part of the Langlands philosophy where you see the issues in lean yet.

Basically I'm going to come back to this later and do IsROrC the way I want to do it but only when I need it which might be in quite a long time

[Adam Topaz]

"IsRorC done right"

[Andrew Yang]

What about Polynomial.IsSplittingField ℚ K (Polynomial.X ^ 2 + 1) using docs#Polynomial.IsSplittingField

[Junyan Xu]

We can in fact characterize an algebraic extension (not necessarily normal) by the set of polynomials in the base field that have a root in it, or equivalently by the set of minimal polynomials of its elements over the base field, but those are not finite amounts of data. See I.M.Isaacs, Roots of Polynomials in Algebraic Extensions of Fields.
image.png
image.png

[Junyan Xu]

Back to the original question: the simplest concrete model is probably AdjoinRoot ℚ (X^2+1), which is simpler than both SplittingField (how docs#CyclotomicField is defined) and CliffordAlgebra.

If the focus is on computability we should introduce something like docs#Zsqrtd but in a more general form. docs#ZSqrtd and docs#Complex are both homogeneous products, i.e. of the form R × R (but packaged as a structure). The other two examples docs#Unitization and docs#TrivSqZeroExt that Eric gave are heterogeneous products (also allow different universes).

For computing with number fields, rings and finite fields it's probably more important to generalize the former two from R × R to Fin n → R, and generalize the polynomials X^2-d and X^2+1 to arbitrary monic polynomials. The addition already comes with Fin n → R and the multiplication can be easily defined computably like this, but I didn't go on to prove it's isomorphic to AdjoinRoot as an R-algebra. As I remarked there, even though you can characterize finite fields as splitting fields of X^p^n-X or just by the cardinality p^n, for concrete computations you'd still choose a primitive polynomial Fin n → 𝔽_p .

[Kevin Buzzard]

If there really is a need for concrete quadratic stuff then perhaps one should just define $R[X]/(X^2+aX+b)$ as a function of $R$, $a$ and $b$ as re, im : R with the induced +,- and *.

[Kevin Buzzard]

I am slightly concerned that this is just making another way to do something we can already do though

[Michael Stoll]

That would also be convenient for working with hyperelliptic curves, for example.

[Junyan Xu]

Projective coordinates for elliptic curves #8485 originally used the "structure with three fields" design but David changed it to Fin 3 → R by my request, because there's already a Units R-action on it that you'd quotient by, and it's easier to connect to MvPolynomial.

[Michael Stoll]

I think it does make sense to have a representation for quadratic rings and fields that is convenient to use with concrete examples, as they tend to occur quite a bit more frequently in applications than more general extensions.

[Junyan Xu]

If you make a structure re, im : R you need to manually put the +,- instances, and I wouldn't call the * induced.

[Michael Stoll]

You possibly could use the isomorphism with Fin 2 \to R to transport the structure?

[Junyan Xu]

as they tend to occur quite a bit more frequently in applications than more general extensions.

If that's the case then it's better to follow Eric's suggestion to unify all four.

[Junyan Xu]

Yeah, it would be reasonable to define the AdjoinRoot algebra structure on Fin n → R generally and transport to R x R in the special case of quadratic rings.

[Andrew Yang]

If we are fine with choosing a root why not just use AdjoinRoot and define re and im as b.basis.repr · 0 and b.basis.repr · 1 where b is some docs#AdjoinRoot.powerBasis

[Junyan Xu]

AdjoinRoot is defined using Polynomial, so I don't think anything that goes through it can be computable ... (I guess it's a more subtle question whether the kernel could reduce results of operations to a normal form, though.)

[Andrew Yang]

Do we really care about computable computable? I thought having a good set of simp lemmas and/or tactics is the computable we care about.

[Geoffrey Irving]

The thread has diverged a fair ways, but in my actual use case I do need it to be fully computational. But I'm also happy with just tuples for now, and in general I'm okay if computational needs define their own types with noncomputable isomorphisms into the mathematical structures for proving theorems.

[Junyan Xu]

In that case you can take a look at Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves by @Anne Baanen @Alex J. Best et al. The code is here and they actually took the "structure with two fields approach" rather than Fin 2 → R :melting_face:
image.png

[Junyan Xu]

Do we really care about computable computable? I thought having a good set of simp lemmas and/or tactics is the computable we care about.

It's nice to be able to prove identities in ℕ, ℤ, and ℚ by rfl, and it would be nice to extend this to finite extensions of them. There are occasionally talks about proofs by reflection too ... I realize that Fin n → R doesn't quite serve this goal (unlike R × R) because rfl won't do funext and fin_cases, but by decide probably works. AdjoinRoot is a quotient type and certainly doesn't reduce the representative to something of lower degree, but I realize you can probably put a DecidableEq instance on it to make by decide work too.

Edit: I think the instance can be constructed computably (if the monic polynomial p you mod by has a computable support and if the ring has DecidableEq), but would require you redefine modByMonic in a computable way (but you can do that within your decision algorithm). Once the polynomials are reduced to degree < n := natDegree p you can just compare the first n coefficients. The problem is that this instance won't be able to decide an equality between terms that involve polynomial multiplication, because a coefficient of a product of polynomials is a sum over a Finset constructed from the supports, and if the supports are noncomputable (e.g. from an earlier addition or multiplication step) then the coefficient won't reduce. So unless we redefine polynomial multiplication in a computable way (for your specific ring with DecidableEq, or use the DFinsupp approach) the instance won't be of much use.

[Junyan Xu]

I'd like to report here that I developed a framework that allows computing polynomial operations and deciding properties by kernel reduction (rfl) using typeclasses as opposed to meta-programming, but I haven't got time to implement computations in AdjoinRoot following this approach yet. Details are in this thread