Dedekind domains

Stream: maths

[Kenji Nakagawa]

Since there seems to be a decent number of people working on this, I thought it might be worthwhile to get a thread going (and a stream might be good as well).

One of the main things is that there are quite a few definitions to choose from, and two good candidates is based off of discrete valuation rings, and the other is that of being an integrally closed domain. In Cassels-Frochlich, there is also a third, but I haven't had much luck with proving any of the implications.

Currently, I'm trying to work through Marcus's Number Fields and formalize stuff (dependent on #3846) using the integrally closed domain definition. So far, I've proved that any ideal contains some product of primes (and currently, the proof is massive), and the next proof (involving multiplying to get a principal ideal) requires the fact that it's integrally closed, whereas before it has just been Noetherian and non-field. (I'll try to clean and then link/push some code to a branch by tomorrow)

[Johan Commelin]

I think the definition shouldn't really matter once you prove that a bunch of definitions are equivalent

[Johan Commelin]

(Also, re stream: I think this thread should suffice.)

[Anne Baanen]

You can see my work using the "noetherian + each prime ideal is maximal + integral closure is itself" definition here. I was sidetracked a bit on defining and proving some basic properties of the trace form, but should be able to finish that off in a couple of days.

[Thomas Browning]

Are you proving Krull-Akizuki? If I remember correctly, that's the hard part about proving that the integral closure of a Dedekind domain is a Dedekind domain.

[Anne Baanen]

I'm using some shortcuts, basically this: https://math.stackexchange.com/questions/50332/the-integral-closure-of-a-finite-separable-field-extension-of-the-fraction-field plus that you can factor a field extension in a separable part and a purely inseparable part

[Thomas Browning]

I know about the separable shortcut, but how do you handle the purely inseparable case?

[Anne Baanen]

But yes, the Noetherian condition is definitely the one that needs the most machinery

[Anne Baanen]

I use a trick found here: http://www.math.uchicago.edu/~may/MISC/Dedekind.pdf that uses the "Dedekind iff all ideals are invertible".

[Anne Baanen]

(Theorem 2.4, page 3.)

[Thomas Browning]

oh neat, I'll take a look

[Anne Baanen]

By the way, I'm mostly interested in the separable case, so when (if?) I finally make a PR, I will probably leave the inseparable case for later. If you would like to do it, you're welcome to of course :)

[Kenji Nakagawa]

I believe that in most of the literature, it is implicitly implied that dedekind domains are non-fields, and I'm not sure if I saw something along those lines in your code @Anne Baanen (although I don't think this has been relevant so far, or it might be more of a number theory/field theory thing).

Also, in my code I'm not sure if the morally correct way is to create a bunch of definitions like dedekind_id, dedekind_inv and dedekind_dvr and (hopefully) prove equivalences, or just select one for implementation and then write a bunch of iff lemmas. Another question was about how easy/hard it would be to reason about things like k(a) = (b) as ideals of R for some k in the field of fractions (and what the implementation might look like, K-modules(?)). Also, I've noticed that splitting < with ideals tends to have coercions that are annoying to deal with (and make suggest/library_search fail), as well as the fact that sometimes you have to unfold ideal in order to apply a lemma about submodules.

[Kenny Lau]

you compare them as fractional ideals

[Kenji Nakagawa]

Ah, I suppose the most natural way to talk about fractional ideals is with them :sweat_smile:

[Jalex Stark]

(We have a new linkfier that lets us refer to mathlib branches by writing e.g. branch#mushokunosora-dedekind and branch#Vierkantor-dedekind-domain)

[Kevin Buzzard]

So we have two competing Dedekind domain branches? :-/

[Jalex Stark]

I think the divergence is not so bad, at least in a social sense. Kenji sliced a PR off of their branch and Anne gave useful review comments. Hopefully Kenji and Anne have exchanged some PMs to collaborate and avoid duplicate work.

[Anne Baanen]

I've been PR'ing quite a bit of the "finished pieces" of my branch, so apart from the line defining dedekind_domain itself, there is very little new stuff on my branch.

[Anne Baanen]

Unfortunately, I hadn't head of Kenji's project before this thread. I'm open to share work, of course.

[Alexandru-Andrei Bosinta]

I want to work on the Vierkantor branch. Can anyone tell me what is the best way to get involved with the branch? Also, where would I find information on what everyone working on it is up to? I wouldn't want to begin working on something only to find out that someone was already doing that specific part and was already far into it.

[Anne Baanen]

Apart from a definition of Dedekind domain (integrally closed, noetherian, Krull dimension 1) and some work on the trace form, I don't have too much on the branch that is not already in mathlib.

The goal of my branch at the moment is to show that the ring of integers in a number field is Dedekind (assuming that the ring of integers is defined as a suitable integral closure, showing). I already merged a lot of this in mathlib, the remaining part is showing the closure is Noetherian (for now assuming everything is separable). The last week and a bit, I did some work on the trace form, which I want to PR soon, and then I will be ready for concluding Noetherianness. @Kenji Nakagawa has (as I understand it) been focussing on showing the equivalence between various definitions of Dedekind domain. And the plan is to make a PR soon with only the definition, so we can work on a shared base.

To work on a branch that has been pushed to mathlib, it should be enough to run git fetch to get the latest version of all branches and then git checkout -t origin/Vierkantor-dedekind-domain to switch to working on a local copy of the branch. I believe the latest commit builds except for sorry.

[Anne Baanen]

I'm going for dinner now, but I'm sure other people on Zulip can help you if you get stuck.

[Kevin Buzzard]

Thanks for this update Anne! In arithmetic we have the concept of a local field and a global field, and to a certain extent these theories are developed in parallel. The algebraic analogue would be be a discrete valuation ring and a Dedekind domain. I've been working on discrete valuation rings this summer but I got tied up in knots because of some missing API for has_zero which I only resolved recently. I still need to make an API for with_zero (multiplicative int) (the main hold-up being that I think it deserves a name, or at least notation, but I can't think of a good one). Once we have this then I'll be able to prove that a discrete valuation ring has a valuation! This will hopefully be of some use. Some of the definitions of DVR in the literature use Dedekind domains. Some of the definitions of Dedekind domain in the literature use DVRs. Mathematicians! Doncha just love 'em?

[Kevin Buzzard]

Getting the definition in mathlib is really key. There are plenty of mathematicians who want to do stuff but don't know the ins and outs of extend and Prop-valued classes etc. Once the definition is there, these people can get involved

[Kevin Buzzard]

It's a bit like schemes. Now we have a definition, more mathematicians will be able to ask meaningful questions such as "do we have theorem X about schemes"? The answer now might be "we can state it, feel free to try and prove it in a begin end block" which is the part that more mathematicians understand well

[Aaron Anderson]

@Kevin Buzzard, I know it’s mostly a matter of type tags, but why do valuations use multiplicative groups? I thought additive was standard, and that sounds more sensible when our go-to example is integers

[Johan Commelin]

Aaron, it depens on which field of maths you are in. Also... the go-to example is with_top int, which is slightly annoyingly different from int.

[Adam Topaz]

I think this was discussed recently in another thread, but a valuation is a morphism of (multiplicative) monoids_with_zero which satisfies some additional condition. (I personally also like writing value groups additively, but it's a matter of taste and I guess passing between addition/multiplication in lean can get tedious).

[Johan Commelin]

@Aaron Anderson note that a very common other example is the multiplicative nnreal

[Adam Topaz]

I'm actually working on formalizing some stuff about general valuation rings right now. The "easy" way to define the value group is to mod out $K$ (the field) as a multiplicative monoid_with_zero by the equivalence relation induced by multiplication by units from the valuation ring. This is then naturally a multiplicative object :)

[Johan Commelin]

Yup, that's what we did when constructing the canonical valuation in the perfectoid project.

[Aaron Anderson]

Thanks!

[Yakov Pechersky]

Dedekind domains make us hit a new milestone: #4000

[Jasmin Blanchette]

Kevin Buzzard said:

Mathematicians! Doncha just love 'em?

No, I don't. Oh, wait, was this a rherotical question? ;)

[Kevin Buzzard]

Trust us -- we know it's not circular! You guys are just paranoid :-)

[Jasmin Blanchette]

Here's some text I wrote just yesterday in a forthcoming CPP submission:

What is particularly remarkable about this circularity is that it had escaped
the attention of the main author among ***., working in \LaTeX. The
issue was noticed only as we formalized ***. Fortunately, this was still
early enough to prevent public embarrassment.

Regrettably, *** is a computer scientist resp. some C.S. stuff.

[Sebastien Gouezel]

Was it fixable?

[Alexandru-Andrei Bosinta]

How am I supposed to use git fetch? I am using git bash and I tried it using it plainly in a new folder and on a new leanproject, but it gives me an error: fatal: not a git repository (or any of the parent directories): .git

[Johan Commelin]

You have to enter the repo first

[Johan Commelin]

cd my_lean_project

[Alexandru-Andrei Bosinta]

That is what I did. I made a new leanproject and then while I was in that project I tried git fetch and I got that error.

[Anne Baanen]

Did you use leanproject get mathlib, to make a copy of mathlib as a new project, or just leanproject new? If you use leanproject new, then git will not know that you want to make a copy of mathlib.

[Alexandru-Andrei Bosinta]

I initially tried leanproject new and it didn't work, but now I tried leanproject get mathlib and I still get the same error when trying git fetch

[Anne Baanen]

Then I suspect you are not in the correct directory. Can you run pwd in your terminal and copy the output here?

[Anne Baanen]

And also ls -a?

[Johan Commelin]

@Alexandru-Andrei Bosinta leanproject get mathlib will create a directory mathlib inside the directory where you currently are. You need to enter that directory before doing anything else.

[Alexandru-Andrei Bosinta]

Thanks @Johan Commelin. Now it worked.

[Alexandru-Andrei Bosinta]

Well now I ran into another problem: I used leanproject build (because visual studio code was having excessive memory usage errors when I tried to look over a file normally) to compile it, but I got a ton of errors. Some were sorrys, but a lot were just errors. So many errors that if I try to post them all here I will run out of writing space. I am assuming I did something wrong, but I need some help figuring it out. Well, here are the first few errors. I can put more if needed.

C:\Users\alexa\OneDrive\Desktop\vierkantor\mathlib\src\ring_theory\noetherian.lean:416:47: error: unexpected token
C:\Users\alexa\OneDrive\Desktop\vierkantor\mathlib\src\ring_theory\noetherian.lean:425:47: error: unexpected token
C:\Users\alexa\OneDrive\Desktop\vierkantor\mathlib\src\ring_theory\noetherian.lean:430:24: error: unknown identifier 'module.restrict_scalars'
C:\Users\alexa\OneDrive\Desktop\vierkantor\mathlib\src\ring_theory\noetherian.lean:437:6: error: invalid definition, a declaration named 'is_noetherian_ring_of_is_noetherian_coe_submodule' has already been declared
C:\Users\alexa\OneDrive\Desktop\vierkantor\mathlib\src\ring_theory\noetherian.lean:433:38: error: unknown identifier 'order_embedding.rsymm'
Additional information:
C:\Users\alexa\OneDrive\Desktop\vierkantor\mathlib\src\ring_theory\noetherian.lean:433:8: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    ?m_5.well_founded ?m_6
  has type
    well_founded has_lt.lt
  but is expected to have type
    well_founded gt
state:
R : Type u_1,
S : Type u_2,
M : Type u_3,
_inst_1 : comm_ring R,
_inst_2 : ring S,
_inst_3 : add_comm_group M,
_inst_4 : algebra R S,
_inst_5 : module S M,
h : well_founded gt
? well_founded gt

[Johan Commelin]

@Alexandru-Andrei Bosinta Could you please post the output of git log --oneline | head -20?

[Johan Commelin]

You should be able to get mathlib caches for free

[Johan Commelin]

leanproject build is not something that one runs on a daily basis

[Anne Baanen]

The issue is that the last commit is broken. Let me fix it...

[Anne Baanen]

OK, pushed a fix for noetherian.lean.

[Alexandru-Andrei Bosinta]

@Johan Commelin This was the output:

0d833b6dd Merge branch 'Vierkantor-dedekind-domain' of https://github.com/leanprover-community/mathlib into Vierkantor-dedekind-domain
bffc04e65 Trace in a simple field extension
55c82b690 Small fixes
712529538 Finish primitive element theorem
9d4714fcd More progress on simple extensions
22f533c5e A lot of progress toward primitive element theorem
b1b316693 Don't depend on `adjoin` in `algebra_tower`
a9445f8dc A lot of progess on simple field extensions
5cf74fed8 `is_noetherian_of_is_noetherian_top`
dc7da7402 `bilinear_form <-> matrix` now with arbitrary basis
d933856b6 Clean up proof
918984910 Some unfinished work on the trace
0e6c2a641 A set that spans the whole space is a basis if it's of the appropriate size
ca88b16a8 Aug5th End_of_Day
beb519810 Aug5
47e72ada8 Aug5
063e3d4ed Aug4th
7c3fe2b8d Some helper lemmas for showing the integral closure is noetherian
f31eae314 Update mathlib
a91192155 refactor(linear_algebra/*): postpone importing material on direct sums (#3484)

I only ran leanproject build because it seemed like my only option to get it to work. I tried to look over trace.lean (didn't modify anything) and after a long wait I got like 600 errors which all seemed to be related to excessive memory usage. Then I used leanproject build and my comment from before is what I got from it.
Thank you @Anne Baanen for your fix. I got the new commit and I am hoping it will work this time, but it is taking its time to compile.

[Johan Commelin]

@Alexandru-Andrei Bosinta I don't know how much git you know, so you should tell me if I'm boring you.

[Johan Commelin]

leanproject get-cache will use the top-most commit number to check whether there is a precompiled version of mathlib available.

[Alexandru-Andrei Bosinta]

I know pretty much nothing about git, so you won't be able to bore me

[Johan Commelin]

But if that commit exists only on your computer, than of course you are stuck

[Johan Commelin]

In your case, you the top-most commit is the result of you trying to pull commits from github and merge them into what you have locally

[Johan Commelin]

So, if you make sure you get-cache before you do that git pull, than you will have a decently recent set of olean files.

[Johan Commelin]

You could do

git checkout bffc04e65 # change to the previous commit
leanproject get-cache
git checkout 0d833b6dd # go back to the top of the log

[Anne Baanen]

There are still some errors, let's see if I can fix them. I must have updated to a newer mathlib without updating some definitions...

[Anne Baanen]

OK, I think now everything builds up to some sorrys in dedekind_domain.lean itself.

[Alexandru-Andrei Bosinta]

@Johan Commelin I did the commands you said (in the folder with the branch I got earlier) and then I tried again to look over a file and again I got like 200 errors similar to:

invalid import: data.option.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)

Though I did not get the new commit with the new fixes, but I imagine the same thing will happen even if I do get it. Is there a solution to this, or do I just have to do leanproject build and hope it works?

[Kevin Buzzard]

Just close VS code and open it again, or restart lean with ctrl-,shift p lean: restart

[Riccardo Brasca]

Hi there! I am a number theorist and I am interested in working with Lean. I would like to contribute to the part about Dedekind domain: do you have some small lemma I can try to prove? I mean, some sorry that I can complete without too much effort (I am still a beginner)? Thank you!

[Kevin Buzzard]

@Anne Baanen What is the current story with Dedekind domains? I would really like a definition in mathlib -- I don't even care about the API. Do we have a definition yet? I am edgy about sorrying data and I don't want to build on a definition which might change in the PR process or whatever

[Kevin Buzzard]

There are a bunch of extremely competent mathematicians appearing here like Riccardo and @Damiano Testa , who know this material back to front and it would be interesting to see if they can learn Lean by proving theorems at this level of abstraction -- it will provide a good test for our API to see if Lean can model how they're thinking.

[Kevin Buzzard]

But definitions are hard. I am still struggling with the definition of the valuation on a DVR because of stupid design decisions -- the issues are not mathematical, they are simply that I am not good at definitions. I guess what I'm saying is the sooner we get the definition established, the sooner we can start building the API.

[Anne Baanen]

I was just about to ping @Johan Commelin to ask for a new review of the PR, since it's looking good to me.

[Kevin Buzzard]

There are also students at Imperial who would be interested in this stuff. I think that you can go a long way with DVRs and Dedekind Domains, there is a big API which as a graduate student I once worked through -- see the first two chapters of Cassels--Froehlich.

[Anne Baanen]

(@Johan Commelin , could you please review #4000 again? :)

[Kevin Buzzard]

I can take a look too

[Kevin Buzzard]

I'll do it now.

[Anne Baanen]

Thank you!

[Kevin Buzzard]

NB I'm slow :-) I'm reading it now.

[Johan Commelin]

@Anne Baanen Done

[Johan Commelin]

I'll wait a bit to see if Kevin has comments. After that, we can merge this.

[Anne Baanen]

@Johan Commelin Fixed.

[Kevin Buzzard]

yes please wait, I'm about half way through

[Kevin Buzzard]

I'm having to read a bunch of stuff I've not looked at before, like fractional_ideal.lean

[Kevin Buzzard]

So the big theorem should be that for a Dedekind domain, the monoid of fractional ideals is a group with zero?

[Kevin Buzzard]

because apparently 0 is a fractional ideal

[Kevin Buzzard]

I was never sure but I'm happy with the decision

[Kevin Buzzard]

All the others are locally free of rank 1, and this has rank 0

[Anne Baanen]

Kevin Buzzard said:

So the big theorem should be that for a Dedekind domain, the monoid of fractional ideals is a group with zero?

Yes, is_dedekind_domain_inv is the definition using this condition. The additions in fractional_ideal allow us to transfer this condition from one choice of field of fractions to another (is_dedekind_domain_iff).

[Kevin Buzzard]

why are you making all these other structures?

I'm nearly done by the way.

[Kevin Buzzard]

OK I reviewed.

[Kevin Buzzard]

I don't have time to read Zulip for the next few hours but if you ping me I'll maybe spot the notification

[Anne Baanen]

Kevin Buzzard said:

OK I reviewed.

Thank you.

My expectation is that two of the structures are temporary. The advantage of making this PR packing each definition in a structure is to agree on the types of constructors/destructors, which were already diverging between me and @Kenji Nakagawa. Defining the API with only the is_dedekind_domain structure requires the use of sorry. It would be possible, but definitely not in mathlib master and so it will be liable to diverge again. Once the implications are there, to delete the structures, we should just be able to fix existing code by removing the _dvr and _inv parts of the names.

[Johan Commelin]

@Kevin Buzzard There were a couple of more replies to your questions. Could you please take a look. If you are happy with how things are (for this PR), please let me know.

[Kevin Buzzard]

I'll look within a few hours

[Kenji Nakagawa]

I think roughly in order to prove at least one side of the _dvr \iff is_dedekind_domain it would be nice to have R is a DVR iff local is_dedekind_domain. And I suppose this also suggests that we should have a PID is_dedekind_domain. If anyone has progress towards this, that would be of great help.

[Kevin Buzzard]

What is the status of Dedekind domains now? We have the definition but are there any other PRs or branches working on stuff?

[Kevin Buzzard]

I am having real problems with making the valuation on a DVR for completely stupid non-mathematical reasons (see the multiplicity thread)

[Kenji Nakagawa]

I'm currently looking at proving the DVR and integrally closed definitions are equivalent. I believe that currently @Filippo A. E. Nuccio is working on prime factorization, and @Anne Baanen is working towards proving that the ring of integers of a number field is a dedekind domain. As for where this is happening, the github project page is up to date, and the two branches branch#mushokunosora-dedekind and branch#Vierkantor-dedekind-domain don't have overlapping work or divergence.

I believe awhile ago someone had mentioned progress on something about the class group, but that's about as much as I know.

[Kevin Buzzard]

Thanks for the update. In future I'll just look at the project page

[Lambert A'Campo]

May I revive this chat to ask what the current status of proving equivalences between the several definitions of dvrs and Dedekind domains is? I'm interested in writing some of these lemmas but not sure which branch to checkout.

[Kevin Buzzard]

I think everything I did, I PR'ed.

[Kevin Buzzard]

I have been working on changing the definition of a valuation, a recent PR I wrote about ordered monoids got merged so I think I can go ahead and change this now

[Ashvni Narayanan]

Lambert A'Campo said:

May I revive this chat to ask what the current status of proving equivalences between the several definitions of dvrs and Dedekind domains is? I'm interested in writing some of these lemmas but not sure which branch to checkout.

I think @Filippo A. E. Nuccio and @Anne Baanen might be able to tell you more. I am yet to PR what I did, which is on the dd-iff branch.

[Filippo A. E. Nuccio]

@Lambert A'Campo If you leave us a couple of days, we should be able to clarify all the situation and let you know what is still to be done!

[Lambert A'Campo]

Ok as practice I spent the afternoon writing a proof for the following lemma:

/--
A local noetherian integral domain `R` such that the maximal ideal of `R` is principal
and the unique non-zero prime ideal (i.e. `R` has Krull dimension 1)
is a discrete valuation ring.
-/
lemma of_principal_unique_prime_ideal {R : Type u}
  [integral_domain R] [local_ring R] [Inoetherian : is_noetherian_ring R]
  {p : R} (Hprincipal : maximal_ideal R = ideal.span {p})
  (Hunique : ∀ I ≠ (⊥ : ideal R), I.is_prime → I = maximal_ideal R)
  (Hnon_zero : maximal_ideal R ≠ ⊥) :
  discrete_valuation_ring R

My code compiles but is very ugly, should I push it to the dd-iff branch?

[Kenny Lau]

sure

[Lambert A'Campo]

ok I just saw I don't have permission to do that anyways

[Lambert A'Campo]

could push it now