Computable algebraic integers

Stream: maths

[Kenny Lau]

The following is just for my personal curiosity, I have no intention of doing or using any of the following results:

How difficult is it (maybe in theory) to implement a computable type of algebraic integers?

By which I mean:

1. There should be a bijection from this type A to the IntegralClosure of ℤ in ℂ (the inverse would be noncomputable)
2. All the ring operations (0, 1, +, x) on A should be computable, and equality should be decidable.
3. There should also be a computable function A → ℤ[X] that gives you the minimal polynomial of a given algebraic integer (so we would first need to make ℤ[X] computable :melt: )
4. maybe other properties that don't come to mind yet.

I've only ever heard about it in theory, where you basically well-order every monic integer polynomial, and for each one you can computably find approximations to its roots in ℂ, which allows you to pick an order on the roots as well (in terms of what they get sent to in ℂ), but then the details will undoubtedly get very messy very quickly, so I'm just wondering if anyone has actually done anything like this.

I guess if we compare it to existing computer algebra systems (CAS), they only take one finite extension at a time, which I guess could also be good enough.

[Aaron Liu]

This sounds greatly difficult

[Aaron Liu]

I guess it depends on how computable you want it to be

[Aaron Liu]

Do you want it to be computable or efficiently computable

[Aaron Liu]

Just Computable I think should be pretty easy (if insanely tedious)

[Jz Pan]

I think firstly you need to compute an integral basis

Maybe you want to check out Cohen's Computational Algebraic Number Theory GTM books

[Kevin Buzzard]

What did the odd order people do in Rocq for the character theory part of the proof? I thought they had (and solved) a problem very close to this.

I thought that the conclusion of the discussion about computable polynomials was not "polynomials need to be made computable" but "computable polynomials need to be written as a separate thing"

[Kevin Buzzard]

And as Aaron said, are you going for "computable in theory" or "actually useful" because these are two very different things. Existing CASs tend to go for "actually useful" which involves not doing what you're suggesting at all but instead working with a good model of $\mathbb{Q}[X]/(f).$

[Bas Spitters]

Have a look at the work by @Cyril Cohen and @Assia Mahboubi on real algebraic geometry:
https://inria.hal.science/inria-00593738v4

[Artie Khovanov]

I think that's a little different - that's the decision procedure for arithmetical statements about real closed fields

[Artie Khovanov]

So good for eg solving real polynomial inequalities

[Artie Khovanov]

I think computational ANT uses quite different methods?

[Cyril Cohen]

Indeed the paper of mine which is closest to this topic is rather https://inria.hal.science/hal-00671809v2/
But the I/we reused many of the methods in the QE paper.