S-integers and S-units

Stream: maths

[David Ang]

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]

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

[Yaël Dillies]

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]

David Ang said:

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

Whoops, the hyphens here are supposed to be underscores

[David Ang]

/poll What should the structures be called?

[Adam Topaz]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

Ah, this is very nice.

[Yaël Dillies]

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]

valuation_subring doesn't have arbitrary joins

[Adam Topaz]

and it only had nonempty sups

[Adam Topaz]

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

[Yaël Dillies]

A tree?

[Adam Topaz]

yeah I guess so.

[Adam Topaz]

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

[Yaël Dillies]

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

[David Ang]

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]

This should be defeq to what you have!

[Adam Topaz]

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]

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

[Junyan Xu]

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]

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]

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]

Want to formalize that in counterexamples/? :)

[David Ang]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]