Zulip Chat Archive

Stream: maths

Topic: S-integers and S-units


David Ang (Aug 24 2022 at 21:39):

I've started a pull request for a basic file containing the definition of S-integers and S-units for a set of primes S (of a Dedekind domain). There are some naming conventions I would like to get opinions for, particularly the name of the file and the name of the structures involved.

David Ang (Aug 24 2022 at 21:40):

/poll What should the name of the file be called?

Yaël Dillies (Aug 24 2022 at 21:41):

Let me point out that we're not held to following the docs#units convention, because we don't have the homonymy problem with docs#unit.

David Ang (Aug 24 2022 at 21:42):

David Ang said:

/poll What should the name of the file be called?

Whoops, the hyphens here are supposed to be underscores

David Ang (Aug 24 2022 at 21:42):

/poll What should the structures be called?

Adam Topaz (Aug 24 2022 at 21:43):

Is the assumption that the ring is a Dedekind domain really necessary at this point?

Adam Topaz (Aug 24 2022 at 21:45):

Oh I see docs#is_dedekind_domain.height_one_spectrum.valuation requires a Dedekind domain, but this is true for any normal ring.

David Ang (Aug 24 2022 at 21:47):

David Ang said:

/poll What should the name of the file be called?

After a basic API for these things, the plan is to ultimately to prove Dirichlet's S-unit theorem, so I would think calling the file S_unit or S_units make more sense over S_integer or S_integers (not a fan of the ring or group stuff now).

David Ang (Aug 24 2022 at 21:49):

Thanks @Oliver Nash for the review, by the way!

Adam Topaz (Aug 24 2022 at 21:49):

BTW, you could use docs#valuation_subring and take the intersection of all subrings given by the valuation subrings assocaited to primes not contained in S to get the same result.

Adam Topaz (Aug 24 2022 at 21:49):

Similarly you could use docs#valuation_subring.unit_group to get the units

Adam Topaz (Aug 24 2022 at 21:54):

I.e. something like this:

import ring_theory.valuation.valuation_subring
import ring_theory.dedekind_domain.adic_valuation

universes v u
open is_dedekind_domain

variables {R : Type u} [comm_ring R] [is_domain R] [is_dedekind_domain R] (K : Type v) [field K]
  [algebra R K] [is_fraction_ring R K] (S : set $ height_one_spectrum R)

noncomputable theory

def S_integer : subring K :=
 P  S, (P.valuation : valuation K _).valuation_subring.to_subring

def S_unit : subgroup Kˣ :=
 P  S, (P.valuation : valuation K _).valuation_subring.unit_group

David Ang (Aug 24 2022 at 21:57):

Ah, this is very nice.

Yaël Dillies (Aug 24 2022 at 21:57):

Dumb order theorist question: I assume you can't have S_integer : valuation_subring K because valuation_subring K is not a complete lattice?

Adam Topaz (Aug 24 2022 at 21:57):

valuation_subring doesn't have arbitrary joins

Adam Topaz (Aug 24 2022 at 21:57):

and it only had nonempty sups

Adam Topaz (Aug 24 2022 at 22:01):

@Yaël Dillies this valuation_subring does have one peculiar property: Given any element vv, the subposet {xvx}\{x | v \le x\} is linearly ordered. Is there an order-theoretic name for such a thing?

Yaël Dillies (Aug 24 2022 at 22:02):

A tree?

Adam Topaz (Aug 24 2022 at 22:02):

yeah I guess so.

Adam Topaz (Aug 24 2022 at 22:02):

do we have a way to speak about such things in mathlib?

Yaël Dillies (Aug 24 2022 at 22:03):

Not per se, but you can already express many close properties. What kind of theorems do you want to state?

David Ang (Aug 24 2022 at 22:15):

Adam Topaz said:

I.e. something like this:

import ring_theory.valuation.valuation_subring
import ring_theory.dedekind_domain.adic_valuation

universes v u
open is_dedekind_domain

variables {R : Type u} [comm_ring R] [is_domain R] [is_dedekind_domain R] (K : Type v) [field K]
  [algebra R K] [is_fraction_ring R K] (S : set $ height_one_spectrum R)

noncomputable theory

def S_integer : subring K :=
 P  S, (P.valuation : valuation K _).valuation_subring.to_subring

def S_unit : subgroup Kˣ :=
 P  S, (P.valuation : valuation K _).valuation_subring.unit_group

Wouldn't the current definition be easier to work with, then having a separate lemma that it's the same as this definition?

Adam Topaz (Aug 24 2022 at 22:17):

This should be defeq to what you have!

Adam Topaz (Aug 24 2022 at 22:35):

okay, maybe not defeq on the nose, but the only difference is some annoyances with the intersection not being defeq to "forall ..." in this case.

Adam Topaz (Aug 24 2022 at 22:35):

But that's a hole in the API for subrings and subgroups, and should be a separate issue altogether.

Junyan Xu (Aug 24 2022 at 23:49):

Would it be reasonable to use the name set.integers and set.units so you can write S.integers K and S.units K? It would be nice to avoid the appearance of a variable in the declaration names and the duplication of S.

If we don't want them to occupy the set namespace can we introduce @[reducible] def set_height_one_spectrum R := set $ height_one_spectrum R and use the names set_height_one_spectrum.integers/units?

Junyan Xu (Aug 25 2022 at 00:10):

Another question: is the S-integers always the localization at a certain submonoid (an intersection of prime_compl, probably)? If so, would be nice to connect to docs#localization.subalgebra.of_field .

Junyan Xu (Aug 25 2022 at 02:13):

I think the answer to my question is no unfortunately, unless the Dedekind domain is a UFD (equivalently a PID); if it's a PID just take one generator of each prime ideal in S, and localize at the submonoid generated by them. If it's not a PID, for example Z[√-5], then the element x = 2/(1+√-5) = (1-√-5)/3 factorizes as the quotient (2,1-√-5)/(3,1+√-5) of two prime ideals, so x is an S-integer with S the singleton {(3, 1+√-5)}. If the S-integers is a localization of Z[√-5], then x can be written as a quotient of two elements in of Z[√-5] with denominator in the submonoid. The ideal (3, 1+√-5) must be a factor of the denominator, but since it's not a principal ideal, the factorization of the denominator must contain another ideal, so 1/denom is not an S-integer even though denom is in the submonoid, contradicting the S-integers being the localization at that submonoid.

Ruben Van de Velde (Aug 25 2022 at 06:41):

Want to formalize that in counterexamples/? :)

David Ang (Aug 25 2022 at 07:39):

The set.integers/units idea sounds good - I’ll see what I can do. One more thing though - does anyone ever use infinite S? Perhaps finset is more appropriate?

Alex J. Best (Aug 25 2022 at 09:56):

Potentially infinite S's seen worth supporting to me, of course some results will only be true for finite S but I'd think there was some use keeping it general where possible.

Damiano Testa (Aug 25 2022 at 11:26):

If using possibly infinite set of S-units, maybe we can have a bridge between localizations at a submonoid and {generating set for the monoid}-units.

As far as I recall, the localization API revolves around having a submonoid and I always found it a little cumbersome to work with inverting a single element.

Junyan Xu (Aug 25 2022 at 15:32):

Yes indeed S-integers is the more general notion (than localization). Given a submonoid M of a Dedekind domain R, you may take S to be the set of all prime ideals appearing in the factorization of some element of M. Clearly the localization at M is contained in the S-integers. Conversely, for x an S-integer, consider all prime ideals where its valuation is > 1; every such prime ideal lies in S, so it's a factor of some element of M. If you multiply x by an appropriate power of the product of these elements of M (which is still an element of M), you get an element of K with valuation >=0 everywhere, so it lies in R, and therefore x is the quotient of two elements of R with denominator in M, or equivalently it lies in the localization of R at M.
So we can make the connection for all Dedekind domains after all!

Kevin Buzzard (Aug 26 2022 at 00:57):

Junyan Xu said:

I think the answer to my question is no unfortunately, unless the Dedekind domain is a UFD (equivalently a PID); if it's a PID just take one generator of each prime ideal in S, and localize at the submonoid generated by them. If it's not a PID, for example Z[√-5], then the element x = 2/(1+√-5) = (1-√-5)/3 factorizes as the quotient (2,1-√-5)/(3,1+√-5) of two prime ideals, so x is an S-integer with S the singleton {(3, 1+√-5)}. If the S-integers is a localization of Z[√-5], then x can be written as a quotient of two elements in of Z[√-5] with denominator in the submonoid. The ideal (3, 1+√-5) must be a factor of the denominator, but since it's not a principal ideal, the factorization of the denominator must contain another ideal, so 1/denom is not an S-integer even though denom is in the submonoid, contradicting the S-integers being the localization at that submonoid.

I don't think this is right. If S={P} as above then P^2=(f) will be principal as the class group has size 2, and localising at S is the same as inverting f.

Kevin Buzzard (Aug 26 2022 at 00:59):

But if you let S={P} where P is a point of infinite order in the class group (e.g. some random complex point of infinite order on an affine elliptic curve) then I believe this gives a Dedekind domain example which is not a localisation.

Junyan Xu (Aug 26 2022 at 02:24):

Oh indeed :sweat_smile: So there are no counterexamples among global fields. The problem is apparently has some parallel with https://mathoverflow.net/a/7185/3332, and your example works in both case.

David Ang (Aug 26 2022 at 22:03):

Adam Topaz said:

okay, maybe not defeq on the nose, but the only difference is some annoyances with the intersection not being defeq to "forall ..." in this case.

I can't seem to equate the two definitions of S-unit groups - one has v.valuation x = 1 while the other has v.valuation.valuation_subring.valuation x = 1, and I'm not sure how to go between the two different value_groups. The two definitions of S-integer rings are equal though!

David Ang (Aug 26 2022 at 22:52):

Junyan Xu said:

Would it be reasonable to use the name set.integers and set.units so you can write S.integers K and S.units K? It would be nice to avoid the appearance of a variable in the declaration names and the duplication of S.

If we don't want them to occupy the set namespace can we introduce @[reducible] def set_height_one_spectrum R := set $ height_one_spectrum R and use the names set_height_one_spectrum.integers/units?

I've refactored them to set.integer and set.unit for now. If this file is not imported, I guess there shouldn't be any harm to have weird definitions in the set namespace?

Adam Topaz (Aug 26 2022 at 22:58):

You're right, it's not defeq, but it's very simple:

import ring_theory.valuation.valuation_subring
import ring_theory.dedekind_domain.adic_valuation

universes v u
open is_dedekind_domain

variables (K Γ : Type*) [field K] [linear_ordered_comm_group_with_zero Γ]
  (v : valuation K Γ)

example (x : Kˣ) : v x = 1  x  v.valuation_subring.unit_group :=
by simpa [(valuation.is_equiv_iff_val_eq_one _ _).mp v.is_equiv_valuation_valuation_subring]

Last updated: Dec 20 2023 at 11:08 UTC