starting some algebraic number theory

Stream: new members

[Johan Commelin]

Welcome! The ring-of-integers and class number stuff are pretty recent additions. I know that @Anne Baanen is particularly interested in applying the new stuff to some computations.

[Johan Commelin]

I think that @Paul Lezeau is working towards Dedekinds theorem on splitting of primes.

[Johan Commelin]

We do not yet have a definition of ramification. We should/could surely add this in the very near future.

[Anne Baanen]

Welcome to Lean! As Scott and Johan suggested, I am indeed very much interested in computing some class numbers. The plan is to show "manually" that the class number of ℚ(√-5) is 2, then hopefully that will teach us if and how Lean could do these calculations mostly automatically. So the topics you mention would be great to have soon, and I'm more than happy to help you with that. (Especially if I can take over your work in the case you can't finish it due to time/interest.)

[Anne Baanen]

For ℚ√d, you might like to check out this old file I wrote a while ago - I wrote a lot of it before designing the final version of class numbers and so on, so I'm sure most of the file won't work. Still I hope you find some inspiration. @Sander Dahmen also wants to define a generic "quadratic ring", i.e. R[α] where α is a root of some quadratic polynomial, which we expect makes these kinds of statements a bit nicer to express.

[Anne Baanen]

The ramification degree would be another great addition, perhaps @Paul Lezeau already has this defined as part of Dedekind's theorem?

[Paul Lezeau]

Anne Baanen said:

The ramification degree would be another great addition, perhaps Paul Lezeau already has this defined as part of Dedekind's theorem?

Not yet unfortunately !

[Alex Meiburg]

Well rather simply a quadratic ring, I think the logical starting point would be R[alpha], where alpha is defined as the root of some irreducible polynomial. Then you could have cubic etc. as well.

Of course in most general it would be have R[alpha,beta,gamma...] where those are successive algebraic extensions. I'm sure this exists in some form for the Galois theory I see is already there. Maybe some of that machinery can be built upon, specializing first to rings with only one additional generator, and then further to quadratic rings?

[Alex Meiburg]

(or maybe it would be better to focus on Galois extensions, so given a base ring R and an irreducible polynomial P in R, we have R adjoin all the roots of P)

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib_docs/field_theory/galois.html ?

[Johan Commelin]

docs#adjoin_root

[Johan Commelin]

This works for an arbitrary (comm) ring and an arbitrary polynomial...