S-integers of a Dedekind domain is also a Dedekind domain

Stream: Is there code for X?

[Yelong Hua]

I am searching theorems to prove that S-integers of fraction fields of Dedekind domains are Dedekind domains.
I have read the file docs#SInteger, but I don't find theorems related to this proposition. Does it already exist in Mathlib somewhere or it can be proved by theorems in Mathlib ?

[Ruben Van de Velde]

Yeah, I don't think anything happened there since !3#15646, so that's all mathlib knows about them. Maybe @María Inés de Frutos Fernández or @Yaël Dillies know more

[Junyan Xu]

Mathlib knows that a localization of a Dedekind domain is Dedekind docs#IsLocalization.isDedekindDomain However, it hasn't been proven yet that the S-integers are a localization, see thread

[Ruben Van de Velde]

CC @David Ang

[David Ang]

@Junyan Xu do you plan to PR your proof of mem_integers_of_valuation_le_one? I haven't been following this for a while

[David Ang]

Originally the S-integer file was meant to be API for Dirichlet's S-unit theorem, but seems like @Xavier Roblot have proved Dirichlet's (empty)-unit theorem without needing this. I currently have no plans to prove that the S-integers are a Dedekind domain, but it's certainly nice to have it in this file.

[Junyan Xu]

do you plan to PR your proof of mem_integers_of_valuation_le_one?

I think It would make more sense to PR together with the localization result. I hadn't tried much but I felt (as I mentioned in the thread) it's unnecessarily complicated to work with factorization into ideals which might make it hard to make progress, so I proposed some refactorings but didn't actually proceed to do them.

[Yelong Hua]

Junyan Xu said:

Mathlib knows that a localization of a Dedekind domain is Dedekind docs#IsLocalization.isDedekindDomain However, it hasn't been proven yet that the S-integers are a localization, see thread

Sorry, my math is not very good. Is S-integers really a localization? I only know this holds over number fields and I'm not aware of the situation for general Dedekind domains.

[Junyan Xu]

Hmm, you have a good point. I think it doesn't even hold over number fields. In the linked thread I have a statement that goes the other way: any localization of a Dedekind domain coincides with the S-integers for some S. But to go the other way, e.g. when S consists of a single non-principal prime, is impossible. (Edit: Oh sorry it's actually okay since a prime in a number field is of finite order in the class group.) From a geometric point of view, the spectrum of the S-integers in this case is just the spectrum of the original Dedekind domain minus a point, so it's just an open subscheme so it will remain regular if the original spectrum is. If we prove docs#IsDedekindDomainDvr is equivalent to docs#IsDedekindDomain, we should be able to produce the result you want via this route, but maybe a more direct proof is quicker.

[Junyan Xu]

Hmm if S is infinite I think the S-integers are probably not finitely generated over the original Dedekind domain and not noetherian so not a Dedekind domain. If S is finite then it's probably noetherian (what's a short proof?) and then we can use docs#isDedekindDomainInv_iff and show that all nonzero fractional ideals in the S-integers are invertible. Any fractional ideal in the S-integers is finitely generated by noetherianity, so they generate a fractional ideal in the original Dedekind domain, and the fractional ideal in the S-integers generated by the inverse of this fractional ideal will be the inverse of the original fractional ideal.

[Yelong Hua]

Thanks for your reply. I only want to consider the case when S is finite. Regarding the first approach, I feel that it's not easy to show that the localization of S-integers at each prime ideal is the same as the localization of the original ring. As for the second approach, the Krull–Akizuki theorem can establish the Noetherian property of S-integers. Are there any theorems related to the Krull–Akizuki theorem in Mathlib?

[Junyan Xu]

Oh I actually mentioned Krull-Akizuki back then but I totally forgot what it's about. So the ring of S-integers is still noetherian even if S is infinite, and my argument above should show it's Dedekind. I feel it's my math that is not very good :sweat_smile: I should have considered the simplest example Z, in which if you invert infinitely many primes the result is not f.g. over Z but still a localization hence noetherian and Dedekind.

I think no one has done Krull-Akizuki yet, and the proof looks nontrivial and might be hard for a new contributor, but I'd offer my support if anyone choose to do it! An important application is to show the integral closure of a Dedekind domain in a finite extension of its fraction field is Dedekind, which has been proven for separable extensions in mathlib (docs#integralClosure.isDedekindDomain), but I just found it may have also been done in the inseparable case. Let me confirm with @Anne Baanen : was it really done? If yes then there's one less motivation for Krull-Akizuki unfortunately ...

[Thomas Browning]

I suspect only the separable case has been done. But even if it hasn't, Krull Akizuki gives a nice uniform proof that doesn't require the case split.

[Kevin Buzzard]

I've not thought this through so excuse my ignorance. For a general Dedekind domain if S contains one prime P whose Frobenius has infinite order then you can talk about the subring of S-integers in the field of fractions but is this a localisation ring-theoretically?

[Kevin Buzzard]

Oh I see -- then the S-integers are just the integers again :-) You are localising at the set of divisors of P^n but this set only contains units

[Anne Baanen]

Junyan Xu said:

An important application is to show the integral closure of a Dedekind domain in a finite extension of its fraction field is Dedekind, which has been proven for separable extensions in mathlib (docs#integralClosure.isDedekindDomain), but I just found it may have also been done in the inseparable case. Let me confirm with Anne Baanen : was it really done? If yes then there's one less motivation for Krull-Akizuki unfortunately ...

We have only done the separable case, so Krull-Akizuki is still going to be very useful :)