Zulip Chat Archive

Stream: new members

Topic: starting some algebraic number theory


Johan Commelin (Oct 04 2021 at 05:47):

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 (Oct 04 2021 at 05:47):

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

Johan Commelin (Oct 04 2021 at 05:48):

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

Anne Baanen (Oct 04 2021 at 07:30):

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 (Oct 04 2021 at 07:31):

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 (Oct 04 2021 at 07:31):

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

Paul Lezeau (Oct 04 2021 at 07:48):

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 (Oct 04 2021 at 18:48):

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 (Oct 04 2021 at 18:51):

(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 (Oct 04 2021 at 18:53):

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

Johan Commelin (Oct 04 2021 at 18:54):

docs#adjoin_root

Johan Commelin (Oct 04 2021 at 18:56):

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


Last updated: Dec 20 2023 at 11:08 UTC