Zulip Chat Archive

Stream: maths

Topic: class groups of number fields?

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 :-/

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.

Kevin Buzzard (Feb 13 2020 at 20:38):

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

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.

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.

Johan Commelin (Feb 14 2020 at 16:11):

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

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:

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)

Johan Commelin (Feb 14 2020 at 16:16):

Aah, right, I meant ID, not PID

Johan Commelin (Feb 14 2020 at 16:17):

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

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

Anne Baanen (Feb 14 2020 at 16:20):

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

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

Anne Baanen (Feb 14 2020 at 16:22):

OK, apart from the sorry, typechecking passes

Last updated: Dec 20 2023 at 11:08 UTC