Zulip Chat Archive

Stream: maths

Topic: class groups of number fields?


view this post on Zulip Kevin Buzzard (Feb 13 2020 at 20:20):

Wasn't there someone in NL last summer formalising basics of class groups of number fields? They did invertible ideals, but didn't get as far as defining the class group. I've mentioned this to a couple of people but they didn't know about this. I am pretty sure this person even sent me an email with some stuff -- am currently trying to find it :-/

view this post on Zulip Rob Lewis (Feb 13 2020 at 20:24):

Antoine Bereau in an internship with @Sander Dahmen , maybe? I don't really remember what Antoine was formalizing but that sounds familiar.

view this post on Zulip Kevin Buzzard (Feb 13 2020 at 20:38):

That makes it rather easier to find his email :-)

view this post on Zulip Sander Dahmen (Feb 14 2020 at 12:20):

Rob Lewis said:

Antoine Bereau in an internship with Sander Dahmen , maybe? I don't really remember what Antoine was formalizing but that sounds familiar.

That's correct. His files are a bit old though. Actually @Anne Baanen is (also) reconsidering fractional ideals and we want to look at class groups (or Picard groups) soon.

view this post on Zulip Anne Baanen (Feb 14 2020 at 15:08):

I have a definition of fractional ideals, and their sum and product. But I'm not entirely happy with this definition because the ideal quotient that I'm trying to write is becoming a bit hacky.

view this post on Zulip Johan Commelin (Feb 14 2020 at 16:11):

Is this fractional ideals in any PID, or what generality?

view this post on Zulip Johan Commelin (Feb 14 2020 at 16:12):

Are there tiny number field libraries floating around that should be PR'd to mathlib :question: :wink:

view this post on Zulip Anne Baanen (Feb 14 2020 at 16:14):

The definition should make sense in any inclusion of (commutative) rings, but I'm working with the inclusion of an integral domain R now (to make the quotient make sense)

view this post on Zulip Johan Commelin (Feb 14 2020 at 16:16):

Aah, right, I meant ID, not PID

view this post on Zulip Johan Commelin (Feb 14 2020 at 16:17):

For PID's the question is not so interesting (-;

view this post on Zulip Anne Baanen (Feb 14 2020 at 16:18):

I've just made a branch with the relevant files: https://github.com/leanprover-community/mathlib/compare/master...Vierkantor:fractional_ideal

view this post on Zulip Anne Baanen (Feb 14 2020 at 16:20):

In fact, I haven't tried compiling the files so there may be missing dependencies. :P

view this post on Zulip Anne Baanen (Feb 14 2020 at 16:21):

But I'm probably not going to be available on Zulip this weekend (either being too busy or too ill :grimacing:), so feel free to make your own version

view this post on Zulip Anne Baanen (Feb 14 2020 at 16:22):

OK, apart from the sorry, typechecking passes


Last updated: May 11 2021 at 17:39 UTC