Refactoring `localization_map`

Stream: maths

[Anne Baanen]

I have mentioned before that I want to get rid of the docs#localization_map.codomain trick (recall that for comm_rings R, S and M : submonoid R, localization_map M S is the type of ring_homs R → S that show S is the localization of R at M; to equip S with the R-algebra structure deriving from f, we have a type synonym (f : localization_map M S).codomain := S and an instance algebra R f.codomain := ring_hom.to_algebra f). The main disadvantage of this setup is that we need to transfer all the results involving S to f.codomain. Moreover, it's hard to understand what is going on when you first encounter them. After some experimenting with different ways of bundling the data, it looks like the nicest solution is as follows, as available in the localization_typeclass branch.

Let R S M be as above, and additionally assume [algebra R S], then we express that S is the localization of R at M with a typeclass is_localization M S, which states that algebra_map R S satisfies the assumptions of localization_map. So far, I have ported ring_theory/localization.lean with positive results: there is a lot less glue code needed between f.codomain and S.

[Kevin Buzzard]

At first glance this very much looks like a step in the right direction.

[Anne Baanen]

Downsides I can think of:

• replacing the explicit parameter f with a typeclass param means we have to make M and/or S explicit in different places, which is annoying to figure out
• we put more stress on the typeclass system
• certain things become quite a bit longer to write (e.g. for g : fraction_map R K, fractional_ideal g becomes fractional_ideal (non_zero_divisors R) K)

[Anne Baanen]

Although fixing the last downside is probably as easy as

local notation R`⁰` := non_zero_divisors R

[Anne Baanen]

Before I spend more time on this refactor, I'd like to hear your thoughts.

[Riccardo Brasca]

If you are looking for a real life test case, we were not able to prove docs#minpoly.over_int_eq_over_rat using docs#minpoly.gcd_domain_eq_field_fractions (the second one is the exact same statement as the first one, but for any GCD domain).

[Anne Baanen]

(I think you mean docs#minpoly.gcd_domain_eq_field_fractions?)

[Eric Wieser]

What's your plan for docs#submonoid.localization_map?

[Damiano Testa]

I had a discussion some time ago with Johan about this. I remember that I would have wanted to have something that was a guarantee that some elements were invertible, but not also a guarantee that it was the localization at precisely those elements. With Johan we were calling this a "pre-localization". Thus, prelocalizations of ℤ at 2 include

• rationals with only powers of 2 in the denominator (the usual localization);
• the rationals themselves
• the reals
• zmod (odd)

Essentially, anything that can be a non-trivial algebra over the real localization should be allowed. This is what I feel that is used in most instances, since these are all the rings that appear in the universal property of the localization.

[Damiano Testa]

Another way of saying it: any ring through which the localization map factors should be a "prelocalization_class".

[Anne Baanen]

Eric Wieser said:

What's your plan for submonoid.localization_map?

Nothing concrete at the moment. If there was a smul instance between M and submonoid.localization_map.codomain, then I would like to do something similar.

[Eric Wieser]

It seems odd to me to eliminate localization_map but not submonoid.localization_map, given the latter is just a weaker version of the former.

[Kevin Buzzard]

A prelocalization is precisely a $\Z[1/2]$-algebra. You could have a predicate for this is_prelocalization M S

[Damiano Testa]

It might be a predicate on a function R \to S [ring S], saying that it is a ring hom and each element of M has invertible image in S. (I am not sure if this is possible, to have a function with target a variable ring, though this may be simply since I have not actually played with dependent type theory!)
[Edit: I corrected the names of the Types above, since I had messed them up!]

[Anne Baanen]

Riccardo Brasca said:

If you are looking for a real life test case, we were not able to prove docs#minpoly.over_int_eq_over_rat using docs#minpoly.gcd_domain_eq_field_fractions (the second one is the exact same statement as the first one, but for any GCD domain).

I managed to make them exactly the same after the refactor! Thank you for a good example :D

[Riccardo Brasca]

Very nice!!

[Anne Baanen]

Damiano Testa said:

It might be a predicate on a function R \to S [ring S], saying that it is a ring hom and each element of M has invertible image in S. (I am not sure if this is possible, to have a function with target a variable ring, though this may be simply since I have not actually played with dependent type theory!)
[Edit: I corrected the names of the Types above, since I had messed them up!]

Although it is possible put [ring S] on the right hand side of the arrow (the category theory library does something like this I believe), in practice we'd probably write something like:

def is_prelocalization {R : Type*} [comm_ring R] (M : submonoid R) (S : Type*) [comm_ring S] : (R →+* S) -> Prop := _

(in other words, for each pair of rings R and S, we define a predicate on the ring homs R →+* S)

[Damiano Testa]

I see, thanks Anne! Now I am curious to see how to do the "other" kind, with the typeclass on the target side of the arrow, but I have not looked at anything is the category part of the library.

[Damiano Testa]

Btw, do you really want M to be a submonoid? Would a subset not be also allowed? In this way you can literally localize at {2}, rather than the multiplicative monoid generated by it...

[Damiano Testa]

(In my mind, localization happens at elements and you show later that you might as well add any element in the monoid generated by the elements by which you localize to the set of denominators.)

[Kevin Buzzard]

I don't know whether you want to take on so many things at once, but it is true that several times the idea has come up that we should be localising rings at subsets and not submonoids. Kenny chose to localise at submonoids after he had been a Lean user for about three weeks in 2017, and of course none of us mathematicians knew what we were doing back then.

[Anne Baanen]

I guess the advantage of (pre)localizing at submonoids is that the localization at {2} and {2, 4} are equal (since closure {2} = closure {2, 4}). That doesn't help if you prelocalize at -2 instead...

[Anne Baanen]

(The prelocalizations at -2 are the same as the prelocalizations at 2, because -2 has an inverse iff 2 has, right?)

[Damiano Testa]

I would say so: you can also always add units to your localizing set

[Damiano Testa]

since an invertible element always maps to something invertible under a ring map. You can get a lot of mileage out of this.

[Damiano Testa]

It feels like the API for prelocalization should be automatically generated by this Zulip chat...

[Damiano Testa]

A while back, I PRed is_regular and showed that invertible elements are regular. I wonder if the PR for is_regular might help with these products of invertible elements being invertible.

docs#is_regular

[Kevin Buzzard]

Also, the localisation at {2} and {4} are the same. The theorem is that the localisation at set S is equal to the localisation at the submonoid Sat(S) which is the saturation of the submonoid generated by S, i.e. all the r in R which divide an element in the submonoid generated by S, and localising at S and T is "the same" iff Sat(S)=Sat(T).

[Kevin Buzzard]

(the proof uses that if ab is invertible then so is a)

[Kevin Buzzard]

I still vividly remember this dawning on me when I was a PhD student!

[Anne Baanen]

A month of spare hours later, everything builds! See PR #8119

[Johan Commelin]

Wowowowow! That's fantastic news!

[Filippo A. E. Nuccio]

Great!

[Anne Baanen]

Interestingly, the linter points out that the current setup of fractional ideals actually uses very little properties of is_localization. How heretical would it be to only require an algebra R K instance to define "a fractional ideal of R in K"?

[Anne Baanen]

Thinking about it some more, it makes sense to not assume is_localization, e.g. when we are working with prelocalizations at the "wrong" set of elements.

[Filippo A. E. Nuccio]

So, it would be a subset of K which is a R-module?

[Anne Baanen]

A fractional ideal w.r.t. a submonoid M \sub R in K is defined as a subset S of K which is an R-module, such that there is a a ∈ M with a * S contained in R

[Anne Baanen]

In practice you would have R an integral domain, K the (a) field of fractions of R, and M = R \ {0} = non_zero_divisors R

[Filippo A. E. Nuccio]

Oh well, then I agree that it is not really needed it is a localization.

[Yaël Dillies]

Bourbaki would have loved to have those linters :grinning: