Zulip Chat Archive

Stream: maths

Topic: Dedekind domains


view this post on Zulip Kenji Nakagawa (Aug 22 2020 at 06:17):

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)

view this post on Zulip Johan Commelin (Aug 22 2020 at 07:08):

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

view this post on Zulip Johan Commelin (Aug 22 2020 at 07:08):

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

view this post on Zulip Anne Baanen (Aug 22 2020 at 22:58):

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.

view this post on Zulip Thomas Browning (Aug 22 2020 at 23:04):

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.

view this post on Zulip Anne Baanen (Aug 22 2020 at 23:09):

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

view this post on Zulip Thomas Browning (Aug 22 2020 at 23:09):

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

view this post on Zulip Anne Baanen (Aug 22 2020 at 23:09):

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

view this post on Zulip Anne Baanen (Aug 22 2020 at 23:12):

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

view this post on Zulip Anne Baanen (Aug 22 2020 at 23:13):

(Theorem 2.4, page 3.)

view this post on Zulip Thomas Browning (Aug 22 2020 at 23:14):

oh neat, I'll take a look

view this post on Zulip Anne Baanen (Aug 22 2020 at 23:22):

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

view this post on Zulip Kenji Nakagawa (Aug 23 2020 at 06:18):

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.

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:28):

you compare them as fractional ideals

view this post on Zulip Kenji Nakagawa (Aug 23 2020 at 06:32):

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

view this post on Zulip Jalex Stark (Aug 23 2020 at 16:23):

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

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 15:29):

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

view this post on Zulip Jalex Stark (Aug 25 2020 at 14:09):

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.

view this post on Zulip Anne Baanen (Aug 25 2020 at 14:48):

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.

view this post on Zulip Anne Baanen (Aug 25 2020 at 14:49):

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

view this post on Zulip Alexandru-Andrei Bosinta (Aug 31 2020 at 16:44):

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.

view this post on Zulip Anne Baanen (Aug 31 2020 at 17:06):

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.

view this post on Zulip Anne Baanen (Aug 31 2020 at 17:07):

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

view this post on Zulip Kevin Buzzard (Aug 31 2020 at 17:45):

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?

view this post on Zulip Kevin Buzzard (Aug 31 2020 at 17:47):

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

view this post on Zulip Kevin Buzzard (Aug 31 2020 at 17:49):

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

view this post on Zulip Aaron Anderson (Aug 31 2020 at 18:04):

@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

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:13):

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.

view this post on Zulip Adam Topaz (Aug 31 2020 at 18:13):

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).

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:13):

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

view this post on Zulip Adam Topaz (Aug 31 2020 at 18:17):

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 KK (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 :)

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:19):

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

view this post on Zulip Aaron Anderson (Aug 31 2020 at 18:20):

Thanks!

view this post on Zulip Yakov Pechersky (Aug 31 2020 at 19:28):

Dedekind domains make us hit a new milestone: #4000

view this post on Zulip Jasmin Blanchette (Sep 01 2020 at 07:32):

Kevin Buzzard said:

Mathematicians! Doncha just love 'em?

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

view this post on Zulip Kevin Buzzard (Sep 01 2020 at 08:05):

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

view this post on Zulip Jasmin Blanchette (Sep 01 2020 at 08:54):

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.

view this post on Zulip Sebastien Gouezel (Sep 01 2020 at 09:11):

Was it fixable?

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 10:09):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:09):

You have to enter the repo first

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:09):

cd my_lean_project

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 10:14):

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.

view this post on Zulip Anne Baanen (Sep 01 2020 at 10:34):

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.

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 10:54):

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

view this post on Zulip Anne Baanen (Sep 01 2020 at 10:55):

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

view this post on Zulip Anne Baanen (Sep 01 2020 at 10:55):

And also ls -a?

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:57):

@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.

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 11:16):

Thanks @Johan Commelin. Now it worked.

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 13:30):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 13:34):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 13:35):

You should be able to get mathlib caches for free

view this post on Zulip Johan Commelin (Sep 01 2020 at 13:35):

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

view this post on Zulip Anne Baanen (Sep 01 2020 at 13:57):

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

view this post on Zulip Anne Baanen (Sep 01 2020 at 14:01):

OK, pushed a fix for noetherian.lean.

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 14:19):

@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.

view this post on Zulip Johan Commelin (Sep 01 2020 at 14:23):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 14:23):

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

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 14:24):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 14:24):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 14:24):

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

view this post on Zulip Johan Commelin (Sep 01 2020 at 14:25):

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.

view this post on Zulip Johan Commelin (Sep 01 2020 at 14:26):

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

view this post on Zulip Anne Baanen (Sep 01 2020 at 14:35):

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...

view this post on Zulip Anne Baanen (Sep 01 2020 at 14:39):

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

view this post on Zulip Alexandru-Andrei Bosinta (Sep 01 2020 at 15:00):

@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?

view this post on Zulip Kevin Buzzard (Sep 01 2020 at 21:08):

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

view this post on Zulip Riccardo Brasca (Sep 08 2020 at 09:37):

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!

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:40):

@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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:42):

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.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:43):

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.

view this post on Zulip Anne Baanen (Sep 08 2020 at 09:44):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:44):

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.

view this post on Zulip Anne Baanen (Sep 08 2020 at 09:45):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:46):

I can take a look too

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:46):

I'll do it now.

view this post on Zulip Anne Baanen (Sep 08 2020 at 09:46):

Thank you!

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:48):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 10:03):

@Anne Baanen Done

view this post on Zulip Johan Commelin (Sep 08 2020 at 10:19):

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

view this post on Zulip Anne Baanen (Sep 08 2020 at 10:19):

@Johan Commelin Fixed.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:19):

yes please wait, I'm about half way through

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:19):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:20):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:21):

because apparently 0 is a fractional ideal

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:21):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:22):

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

view this post on Zulip Anne Baanen (Sep 08 2020 at 10:29):

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).

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:57):

why are you making all these other structures?

I'm nearly done by the way.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 10:59):

OK I reviewed.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 11:01):

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

view this post on Zulip Anne Baanen (Sep 08 2020 at 12:30):

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.

view this post on Zulip Johan Commelin (Sep 09 2020 at 04:34):

@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.

view this post on Zulip Kevin Buzzard (Sep 09 2020 at 05:10):

I'll look within a few hours

view this post on Zulip Kenji Nakagawa (Sep 11 2020 at 03:56):

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.

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 06:34):

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

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 06:35):

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

view this post on Zulip Kenji Nakagawa (Sep 11 2020 at 07:37):

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.

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 08:37):

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

view this post on Zulip Lambert A'Campo (Jan 03 2021 at 18:00):

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.

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 18:33):

I think everything I did, I PR'ed.

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 18:34):

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

view this post on Zulip Ashvni Narayanan (Jan 04 2021 at 06:31):

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.

view this post on Zulip Filippo A. E. Nuccio (Jan 04 2021 at 08:43):

@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!

view this post on Zulip Lambert A'Campo (Jan 04 2021 at 16:40):

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?

view this post on Zulip Kenny Lau (Jan 04 2021 at 16:50):

sure

view this post on Zulip Lambert A'Campo (Jan 04 2021 at 17:06):

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

view this post on Zulip Lambert A'Campo (Jan 04 2021 at 17:58):

could push it now


Last updated: May 06 2021 at 17:38 UTC