## Stream: maths

### Topic: (comm_)semiring: examples?

#### Damiano Testa (Jan 17 2021 at 17:42):

Dear All,

I do not think that I ever really encountered semirings in math, until I started using Lean. Of course, I had seen the "semiring" of polynomials with coefficients in ℕ, and a couple of times I used something about the semiring of sums of squares in an ordered ring.

I want to point out that I am sold on the idea of using semirings (likely comm_semirings), but I would like to have a good supply of examples that are not "essentially comm_rings".

My question: what are good examples of comm_semiring that are not sub_semirings of a comm_ring? Besides boolean_algebras with inf and sup (in either order) as addition and multiplication, I do not have many more examples.

The underlying goal that I am trying to achieve is to see how much of commutative algebra can be done by working with (comm_)semirings alone. For this, I would like to have access to examples that would help suggesting results and disproving statements.

Thanks!

#### Riccardo Brasca (Jan 17 2021 at 17:43):

The tropical semiring?
https://en.wikipedia.org/wiki/Tropical_semiring

#### Damiano Testa (Jan 17 2021 at 17:50):

That's a very good suggestion! I had not thought of that! Thanks!

#### Mario Carneiro (Jan 17 2021 at 17:55):

The underlying goal that I am trying to achieve is to see how much of commutative algebra can be done by working with (comm_)semirings alone. For this, I would like to have access to examples that would help suggesting results and disproving statements.

Rather than looking for examples, an easy way to achieve this is to just pretend that semirings are rings until you get in trouble. It is surprisingly common for mathematical textbooks to make stronger assumptions than necessary for no reason besides making it easier to think about the subject. Just like how every vector space looks like R^2 and every topological space looks like a picture of a cloud, just ignore the full range of examples and use the nice ones to guide proof sketches.

#### Adam Topaz (Jan 17 2021 at 17:59):

You can get very far doing commutative algebra with semirings. You can even "do" algebraic geometry.

#### Damiano Testa (Jan 17 2021 at 17:59):

Thank you Mario! I completely agree with you on unnecessary assumptions in maths: I find this really inspiring about Lean (and formalization in general).

I have also been playing in my head with trying to find a statement that "requires" a comm_ring and so far I have mostly failed. Of course, there are some tautological statements that "need" existence of opposites, but not much besides almost tautologies.

The reason for asking for examples, though, is to see if there is really a wealth of examples to justify the effort of reproving known statements. Thus, before embarking on this journey, I would like to at least have a few well-chosen examples as justification.

#### Mario Carneiro (Jan 17 2021 at 17:59):

The main thing that you can't do in a semiring is to cancel additions. This means that you can have things like an add that saturates, for example ennreal or fin n

#### Damiano Testa (Jan 17 2021 at 18:02):

Adam, this is exactly what I would like to understand: how much of what I know of algebraic geometry is really relying on what the ground (semi)-ring is. I always thought that making assumptions on the base ring such as field, integral_domain, reduced were often just safety nets that never really played a role. Now I am trying to see whether even the existence of opposites is actually ever a serious issue...

#### Alex J. Best (Jan 17 2021 at 18:02):

I don't think fin ns add saturates, I think it would be nice if it did though. Or maybe that's what you're saying too :smile:

#### Mario Carneiro (Jan 17 2021 at 18:02):

no but you get the idea

#### Mario Carneiro (Jan 17 2021 at 18:02):

anyway you probably want fin (n+1) for that

#### Damiano Testa (Jan 17 2021 at 18:04):

I like the ideas of ennreal (which, if I understand correctly what it is, is similar to the sums of squares of \R?).

I will take a look at what is the addition on fin n!

#### Mario Carneiro (Jan 17 2021 at 18:06):

ennreal is the extended nonnegative reals, $[0,\infty]$

#### Mario Carneiro (Jan 17 2021 at 18:07):

the addition on fin n is broken but the one I'm talking about is (a + b : fin (n+1)) := min(n, a + b)

#### Damiano Testa (Jan 17 2021 at 18:07):

Ah, I see, it also has an \infty! Thanks!

#### Mario Carneiro (Jan 17 2021 at 18:07):

the nonnegative reals are also a semiring but I think you already mentioned it as a boring example

#### Damiano Testa (Jan 17 2021 at 18:08):

Ok, thanks: also fin (n+1) is a good example!

#### Damiano Testa (Jan 17 2021 at 18:08):

Well, not boring, just not "exotic" enough...

#### Adam Topaz (Jan 17 2021 at 18:08):

One nice exercise is to classify all semiring quotients of nat

#### Damiano Testa (Jan 17 2021 at 18:09):

Adam: is your question equivalent to "classify cyclic semirings?"?

#### Adam Topaz (Jan 17 2021 at 18:09):

I don't know what cyclic semirings are...

#### Damiano Testa (Jan 17 2021 at 18:10):

generated by a single element... ah, there is zero also!

#### Mario Carneiro (Jan 17 2021 at 18:10):

What are semiring quotients defined as?

#### Adam Topaz (Jan 17 2021 at 18:10):

There's also some work by Borger et al about Witt vectors in the context of semirings

#### Adam Topaz (Jan 17 2021 at 18:10):

Semiring quotients of N are semirings with a surjective semiring hom from N

#### Damiano Testa (Jan 17 2021 at 18:11):

Ok, so, if I understand correctly, a semiring quotient of N is a semiring that contains 0 and is generated by a (possibly extra) element, right?

#### Adam Topaz (Jan 17 2021 at 18:11):

https://arxiv.org/abs/1310.3013

#### Mario Carneiro (Jan 17 2021 at 18:12):

The extra element has to be the one

#### Damiano Testa (Jan 17 2021 at 18:12):

I guess that semirings contain zero by definition, though... so it is simply a semiring generated by a single element (which could be zero itself), right?

#### Mario Carneiro (Jan 17 2021 at 18:12):

semiring homs fix both 0 and 1

#### Damiano Testa (Jan 17 2021 at 18:12):

zero and one are different in a semiring? I thought that (0) was a semiring?

#### Mario Carneiro (Jan 17 2021 at 18:13):

they aren't necessarily different

#### Mario Carneiro (Jan 17 2021 at 18:13):

but 0 has to act like 0 and 1 like 1, so they can only coincide in the zero ring

#### Damiano Testa (Jan 17 2021 at 18:13):

ok, so we either have the zero semiring or a ring with o and everything is generated by the non-zero element 1

#### Damiano Testa (Jan 17 2021 at 18:14):

So either the semiring is N or it is finite, and n.1 = m, with m \leq n, I would say...

#### Damiano Testa (Jan 17 2021 at 18:15):

I am not sure whether all choices of 0 \leq m \leq n are allowed, but it seems like it...

#### Damiano Testa (Jan 17 2021 at 18:16):

this is a great exercise to practice-formalize in Lean: thank you Adam!

#### Kevin Buzzard (Jan 17 2021 at 23:50):

Damiano -- Z/3Z is a semiring quotient of N but so is fin 3 with 2+1=2.

#### Damiano Testa (Jan 18 2021 at 01:54):

Ok, these two choices seem to be

• (m, n) = (0, 3) for Z/3Z and
• (m, n)=(2, 3) for fin 3

#### Kevin Buzzard (Jan 18 2021 at 06:45):

Aah I see. If you know the dynamics of the +1 function you know the entire semiring structure because addition is repeated +1 and multiplication is repeated addition

#### Damiano Testa (Jan 19 2021 at 06:36):

I am playing around with the idea of allowing ideal to take a comm_semiring instance, instead of a comm_ring instance.

Thus, ideal shifts more towards being submodule R R. An alternative could be converting lemmas for ideal into lemmas for (appropriately special) submodules.

To try this out, I replaced comm_ring for comm_semiring in ring_theory/ideal/basic.lean and a good 300 lines of code are just automatically converted.

Before I actually take action, what are people views on this? Is it something that would be useful? For me, personally, there is a blur in the notion of submodule R M <= submodule R R <= ideal R and it seems that trying to push lemmas towards the left would help sharpen the boundaries. For instance, I would be hard pressed to come up with a lemma about an ideal that is really awkward to state for a submodule R M. If M is actually cyclic, then the distinction between ideal and submodule R (span R singleton) is even more subtle.

#### Damiano Testa (Jan 19 2021 at 06:44):

Procedurally, the simplest first step could be to simply change the definition, create a section comm_semiring in the file and "float" all the lemmas that are already proved-as-stated into this section.

Later, the remaining lemmas can be adapted, maybe by proving an alternative version for the extended def of ideal, and the old lemma would then be the conversion of the newer more general version to what it was before.

#### Mario Carneiro (Jan 19 2021 at 06:46):

Isn't ideal R defined as submodule R R? Clearly then it serves a purpose, namely to specialize to the case where the two types are the same

#### Mario Carneiro (Jan 19 2021 at 06:46):

Of course any theorems about submodules should be stated on submodules

#### Kevin Buzzard (Jan 19 2021 at 06:55):

I think I was at least partly at fault for ideals only being defined for commutative rings, because we needed them for schemes very early on and I didn't have a clue about this semiring stuff. Since then there has been plenty of noise from people saying we should have have them for noncommutative rings but I don't think I've ever heard anyone suggest we need them for semirings!

Here is an argument against it. The reason we have normal subgroups and ideals is that for sensible objects like groups and rings, these are exactly the objects we use to form quotient objects. For semirings this is not the case. For general algebraic objects one forms quotients by quotienting out by a general equivalence relation, not some kind of subobject. The equivalence relation needs to play well with the structure fields and then the quotient object inherits the structure. For groups and rings it's kind of a coincidence (at least as far as I can see) that in both cases such an equivalence relation comes from a certain kind of subobject (the most striking case is abelian groups, where quotients are the same thing as subobjects, perhaps the reason why exact sequences are so important). For commutative semirings it is not true that every quotient object is the quotient by an ideal and this is perhaps the reason that ideals don't seem to have as much significance mathematically for semirings.

Having said all that, of course it's certainly the mathlib philosophy that objects should be defined in the biggest generality in which they make sense, and this is definitely an argument for doing it. You just might find that mathematically it doesn't buy you much in practice.

#### Adam Topaz (Jan 19 2021 at 07:03):

Fortunately docs#ring_quot works for semirings :)

#### Kevin Buzzard (Jan 19 2021 at 07:03):

This will be the thing which is used in practice rather than ideals, I guess

#### Damiano Testa (Jan 19 2021 at 07:09):

Kevin, I understand and share your view.

Still, there are lots of results in ring_theory/ideal/basic that work for submodule R R with [comm_semiring R] (rather than ideal for a [comm_ring]) as stated-and-proven. It should be uncontroversial (this is never the case...) that these should be stated at least in this generality, though, right?

#### Mario Carneiro (Jan 19 2021 at 07:12):

I don't think it is an issue to define ideal R to take comm_semiring, or even semiring as an argument, and given that I'm sure many theorems will generalize without you having to do anything. I wouldn't use submodule R R in place of ideal R though; the theorems about submodule M R should be proven in that generality, and then specialized to ideal R

#### Damiano Testa (Jan 19 2021 at 07:12):

Mario, it is true that ideal R = submodule R R, but the definition only applies with a background [comm_ring R], instead of a [comm_semiring R] assumption.

#### Mario Carneiro (Jan 19 2021 at 07:13):

However you might have to be careful that the definition is still correct in the semiring case (I would go for a left ideal)

#### Damiano Testa (Jan 19 2021 at 07:16):

Ok, so the consensus seems to be to leave the definition of idealwith the implied assumption on R fixed, but convert the statements of the lemmas to apply to submodule R R with a weaker assumption on R, right?

I also agree with removing the comm assumption and then left/right ideal: I was planning to only tackle the comm issue, not allowing non-commutative rings, at least for the moment!

#### Mario Carneiro (Jan 19 2021 at 07:16):

Well you can do exactly the same thing as you're doing now: just take the comm off and put it back in on theorems that fail

#### Damiano Testa (Jan 19 2021 at 07:17):

Procedurally, rather than changing the definition of ideal change the variables from

variables [comm_ring α] (I : ideal α) {a b : α}


to

variables [comm_semiring α] (I : submodule R R) {a b : α}


and see what copiles, right?

#### Mario Carneiro (Jan 19 2021 at 07:18):

No, I mean variables [comm_semiring α] (I : ideal R) {a b : α}

#### Mario Carneiro (Jan 19 2021 at 07:18):

or variables [semiring α] (I : ideal R) {a b : α}

#### Damiano Testa (Jan 19 2021 at 07:19):

Ok, I think that I have confused myself: do people want to change the definition of ideal to allow a comm_semiring instead of a comm_ring underlying ring?

#### Mario Carneiro (Jan 19 2021 at 07:19):

that's my suggestion, yes

#### Damiano Testa (Jan 19 2021 at 07:20):

I see, I think that Kevin had argued (weakly) against that. Maybe, we should reach a consensus on this, before changing!

#### Damiano Testa (Jan 19 2021 at 07:20):

(Btw, Mario, in my experiment, what you suggest is exactly what I did.)

#### Mario Carneiro (Jan 19 2021 at 07:24):

Kevin's argument, which I agree with, about the danger of "trivial generalization" is that you can end up stating true theorems about a useless thing. A definition that makes sense in a restricted situation may no longer be correct in a general setting. This is like defining implication as not a \/ b in classical logic and then generalizing to intuitionistic, or defining quotient rings by taking the quotient wrt an ideal and then generalizing to where not all quotients are quotients by an ideal. The definition and theorems are still correct but it's no longer capturing the right idea

#### Mario Carneiro (Jan 19 2021 at 07:25):

In the best case, there is a way to tweak the definition such that it is correct in the generalization and equivalent to the old definition in the original restricted setting

#### Mario Carneiro (Jan 19 2021 at 07:27):

In other cases, you might have a bifurcation of concepts, like left / right / two-sided ideals in the noncommutative setting, and then you have to pick which one is the official one that gets the simple name in the restricted setting and give new names for the others

#### Mario Carneiro (Jan 19 2021 at 07:28):

In the worst case the correct definition in the general setting is annoying to work with in the restricted setting because it's paying attention to subtleties that don't matter, and now the restricted setting (which is what most people care about) has been made worse by the generalization

#### Mario Carneiro (Jan 19 2021 at 07:30):

an example of the latter might be free_comm_ring R A, which is a quotient of an inductive type for constructivity reasons but classically is just the same thing as mv_polynomial R A

#### Damiano Testa (Jan 19 2021 at 07:31):

I completely agree.

I am still not convinced that there is a general consensus on allowing comm_semirings as coefficients for ideals, or whether we should stick to the current definition of ideal and simply state more lemmas for submodule R R.

#### Mario Carneiro (Jan 19 2021 at 07:31):

I don't think there is any reason for submodule R R to have theorems if ideal R exists

#### Johan Commelin (Jan 19 2021 at 07:32):

Mario, I think Damiano means that the R in submodule R R could have weaker assumptions.

#### Mario Carneiro (Jan 19 2021 at 07:32):

I agree with that, but they should be applied to ideal too

#### Johan Commelin (Jan 19 2021 at 07:32):

But I think in this case ideal R will not become harder to use if we generalise it.

#### Johan Commelin (Jan 19 2021 at 07:33):

@Damiano Testa nevertheless, I fear that refactoring ideal will be a huge effort.

#### Mario Carneiro (Jan 19 2021 at 07:33):

Why would it? Trivial generalization is usually not very hard, although it might be useless

#### Mario Carneiro (Jan 19 2021 at 07:34):

Unless there are typeclass subtleties

#### Johan Commelin (Jan 19 2021 at 07:34):

It is used all over the place. And typeclass inference of unification may take slightly different paths if you generalise it, so you might suddenly face painful broken proofs in functional analysis, measure theory, or whatever.

#### Damiano Testa (Jan 19 2021 at 07:34):

Not speaking for the difficulties in Lean, but the refactor could simply be to allow the rings to be comm_semiring, but then only gradually change the uses of ideals to a more general setting, as needed.

#### Johan Commelin (Jan 19 2021 at 07:35):

@Mario Carneiro module R M is an abbreviation for semimodule R M. Nevertheless, if you globaly search replace semimodule by module, and remove the old module-def, mathlib will be broken in tons of places.

#### Damiano Testa (Jan 19 2021 at 07:35):

I see, is there a way to test this out? Simply changing the definition of ideal and touching nothing else. What would break?

#### Mario Carneiro (Jan 19 2021 at 07:35):

That's exactly how you test it

#### Johan Commelin (Jan 19 2021 at 07:36):

@Damiano Testa you can just make the change, and see what happens.

#### Johan Commelin (Jan 19 2021 at 07:36):

Either push it to a branch, and wait till CI tells you, or compile locally with lean --make src/

#### Damiano Testa (Jan 19 2021 at 07:36):

Ok, I have and I get a bunch of red lines in this file. I thought that you were suggesting that other files would break as well

ah, ok!

#### Johan Commelin (Jan 19 2021 at 07:36):

I would be surprised if other files don't break.

#### Damiano Testa (Jan 19 2021 at 07:37):

I am going to start a fresh copy of mathlib, simply change the comm_ring to comm_semiring and let it build

#### Johan Commelin (Jan 19 2021 at 07:37):

This is some weird thing. From a maths point of view, it is clear that nothing should break. From a CS point of view, it is clear that something should break.

#### Johan Commelin (Jan 19 2021 at 07:38):

I mean, you are changing a fundamental def'n in a library with ~450.000 lines of code. Something must break, right?

#### Damiano Testa (Jan 19 2021 at 07:39):

if I push to a branch, would it automatically compile, or should I create a PR?

#### Mario Carneiro (Jan 19 2021 at 07:39):

branches are compiled

ok, thanks!

#### Patrick Massot (Jan 19 2021 at 07:52):

If you have time and energy for a giant refactor I think it would be much more useful to get rid of useless commutativity than to put semi-rings everywhere.

#### Damiano Testa (Jan 19 2021 at 07:52):

I realize that this is my crusade, but the first line that breaks down in ring_theory/ideal/basic is 310. Unfortunately, I do not understand what it does... I will try to figure it out, but if anyone has a tip, it would be greatly appreciated!

instance (I : ideal α) : has_mul I.quotient :=
⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound$ begin
refine calc a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ : _
... ∈ I : I.add_mem (I.mul_mem_left _ h₁) (I.mul_mem_right _ h₂),
rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
end⟩


the three dots give the error

invalid type ascription, term has type
a₁ * a₂ - b₁ * b₂ ∈ ↑I
but is expected to have type
setoid.r (a₁ * a₂) (b₁ * b₂)


#### Kevin Buzzard (Jan 19 2021 at 07:54):

Can you push to a branch so it's easy for others to see the error?

#### Damiano Testa (Jan 19 2021 at 07:58):

Kevin, it is here:

Branch 'comm_semiring'

#### Damiano Testa (Jan 19 2021 at 08:00):

Patrick, I will look into this, but for the comm_semiring I have two goals that I want to achieve.

One is to create a bridge between topology and algebra, using the comm_semiring structure on boolean_algebras of, say, open sets.

The other is to bring more algebraic geometry to tropical geometry. It was Riccardo's observation that the underlying ring for tropical geometry is a comm_semiring. A lot of results similar to results in algebraic geometry hold in tropical geometry, but there is no direct approach. I wonder whether the great similarities between comm_semirings and comm_rings could help!

Both these examples are commutative...

#### Damiano Testa (Jan 19 2021 at 08:02):

For goal one: if there is an analogue of Spec for comm_semirings with good properties, what is Spec (boolean_semiring topological_space)?

#### Eric Wieser (Jan 19 2021 at 08:04):

I tried the non-commutative refactor a while ago, but gave up because Scott introduced ring_quot and solved the problem I actually cared about. There's an open PR with my attempt somewhere still

#### Xavier Xarles (Jan 19 2021 at 11:44):

Dear all, I just realize there is this topic on something I am working on (together with @Marc Masdeu ), that is to do all that it is possible on ideals on lean but for comm_semirings. We had some things done and appart of the quotients (which clearly need to be redone) and some proof that rewrote (concretely, that maximal ideals are prime), must of the file works. Our suggestion, however, is that it should be better to define something like "semideals" or "semiideals" like for modules we use semimodules, in order not to conflict with the things done for ideals.

In order to do quotients, one should develope "congruences" for semimodules: equivalence relations that preserve the structure. Congruences are developed for monoids, so it should not be difficult to do it (in fact, I have some things done). Then the quotient by a subsemimodule is just the quotient by the congruence it generates. But it is not true anymore that the kernel of the quotient by a subsemimodule is the subsemimodule: it is only true for the "saturated" subsemimodules.

To go further, so to do Spec, schemes and so on, it is possible, and it has been developed for several people (including myself in a "private" preprint). It can be done and it should be not difficult.

#### Kevin Buzzard (Jan 19 2021 at 11:57):

Are "prime semi-ideals" the correct objects that one should use to make Spec? Or does one look at e.g. surjections from semirings to semi-integral-domains up to equivalence? Or are these the same thing?

#### Damiano Testa (Jan 19 2021 at 12:07):

In case anyone is interested, this fixed the first broken file:

instance (I : ideal α) : has_mul I.quotient :=
⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound$ begin
obtain F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂),
have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁,
{ rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁] },
rw ← this at F,
convert F
end⟩


#### Xavier Xarles (Jan 19 2021 at 12:07):

One can define Spec with "prime semi-ideals", with "prime saturated semi-ideals" or with "prime congruences", and all three work and are diferent. The main topic of my preprint is the relation of the first two with valuation theory.

#### Xavier Xarles (Jan 19 2021 at 12:13):

So, in my preprint I explain why you naturaly need the two notions of Spec, with ideals and with saturated ideals. I had the idea to see if it is possible to formalize in lean all to give my preprint much more rigor, but it is going to be quite hard.

#### Xavier Xarles (Jan 19 2021 at 12:17):

On the other hand,I was really suprised by lean, when I saw that I could take out all the lemmas using the substraction and using the quotient from the ideal lean file, and change comm_ring for comm_semiring evrywhere and most of the results worked without changes. I thing this really shows that lean can prove that when we say "the same proof works" it is literaly true sometimes.

#### Kevin Buzzard (Jan 19 2021 at 12:47):

@Xavier Xarles right now a (multiplicative) valuation on a commutative ring $R$ in Lean is defined to be a monoid-with-zero homomorphism (i.e. $v(ab)=v(a)v(b)$, $v(0)=0$, $v(1)=1$) from $R$ to $\Gamma\cup\{0\}$, where $\Gamma$ is a totally ordered abelian group (group law $\times$), satisfying $v(a+b)\geq min\{v(a),v(b)\}$. Eric Wieser and I have been reorganising the theory of ordered monoids recently and I was going to change this definition of a valuation to allow the target to be a general totally ordered monoid-with-zero. Should I also change it to allow commutative semirings?

#### Kevin Buzzard (Jan 19 2021 at 12:49):

For the theory of perfectoid spaces we only needed groups-with-zero as the target, but more recently Lau and I realised that in the theory of tilting it's more convenient to allow monoids with zero sometimes. For example there is a "truncated valuation" on $R/pR$ if $R$ is the integers of a (possibly highly ramified) p-adic local field, taking values in $\{0\}\cup(1/p,1]$.

#### Kevin Buzzard (Jan 19 2021 at 12:52):

This was going to be my next PR when I've got through this week (somehow I am giving a lot of talks this week).

#### Damiano Testa (Jan 19 2021 at 13:39):

Is there a way to find out about more than one error at a time? I fixed two files, but I only found out about the second one, after I fixed the first. Is there a way to get all the errors that are within reach of the current position, or will I have to fix one, recompile, fix another, and so on?

#### Kevin Buzzard (Jan 19 2021 at 13:39):

Just compile locally.

#### Kevin Buzzard (Jan 19 2021 at 13:40):

In a terminal, cd to the root of your modded mathlib and then type lean --make src and go and have lunch

#### Damiano Testa (Jan 19 2021 at 13:40):

ok, I will do that, maybe while talking to a student, since I just had lunch! :smile:

#### Patrick Massot (Jan 19 2021 at 13:42):

I'm very proud that users have now forgotten that you can compile mathlib locally.

#### Kevin Buzzard (Jan 19 2021 at 13:43):

If you got 10 cents every time someone typed leanproject get-<something> then you would be doing very well by now!

#### Damiano Testa (Jan 19 2021 at 13:43):

you can get more than cache?

#### Damiano Testa (Jan 19 2021 at 13:43):

cash?

#### Kevin Buzzard (Jan 19 2021 at 13:44):

If you're working on a project which uses mathlib as a dependency, then you can type leanproject get-mathlib-cache to update mathlib

#### Damiano Testa (Jan 19 2021 at 13:44):

Ah, I never dared to make a dependency, since I am still unsure with github

#### Kevin Buzzard (Jan 19 2021 at 13:45):

When you start working on https://github.com/leanprover-community/lean-liquid you'll learn about get-mathlib-cache

#### Damiano Testa (Jan 19 2021 at 13:45):

While we are on this topic, does the make command go sequentially through the files, starting with the ones that import nothing and the proceeding to the next layer recursively?

#### Rob Lewis (Jan 19 2021 at 13:45):

Kevin Buzzard said:

If you got 10 cents every time someone typed leanproject get-<something> then you would be doing very well by now!

We (well, MSR) pay a cent or so, but still!

#### Kevin Buzzard (Jan 19 2021 at 13:46):

Unfortunately not to Patrick!

#### Patrick Massot (Jan 19 2021 at 13:46):

Note that Rob, Gabriel and Bryan should also get a share. Without the CI and Azure infrastructure leanproject couldn't work.

#### Kevin Buzzard (Jan 19 2021 at 13:47):

@Damiano Testa if you have got a fully compiled mathlib and then just change a few files, make will start by compiling one of those, and then move on to other files you changed, and the files which import those files etc. If you have a multi-core machine (which you probably do) then it might work on several at once.

#### Rob Lewis (Jan 19 2021 at 13:47):

And Leo, who helped us arrange the grant that actually pays for it

#### Kevin Buzzard (Jan 19 2021 at 13:48):

Aah, so MS is paying MS! Sounds like a tax dodge.

#### Patrick Massot (Jan 19 2021 at 13:48):

Kevin, you haven't been paying attention during my opening talk at LT2021...

#### Kevin Buzzard (Jan 19 2021 at 13:49):

I promise I was there and listening! I'm just getting forgetful ;-)

#### Damiano Testa (Jan 19 2021 at 13:49):

Kevin, thanks for the explanation! I am sure that there is a lot more under the surface, but it is good to know that it will start from there the interesting stuff has happened!

#### Rob Lewis (Jan 19 2021 at 13:49):

MS Research is paying MS Azure, I bet the internal overhead costs more than the taxes they pay!

#### Kevin Buzzard (Jan 19 2021 at 13:49):

It might well look at earlier files, but if it sees a lean file and an olean file, and these files are compatible, then it just skips the lean file.

#### Xavier Xarles (Jan 19 2021 at 14:26):

@Kevin Buzzard The notion I use in that paper is even more general, as done in a paper by Giansiracusa and Giansiracusa: a (pre)valuation is a map to an idempotent semiring that it is multiplicative and "subadditive". A totally ordered monoid-with-zero becomes an idempotent semiring with the min (or max) operation. But I am not sure this notion is really useful: they introduced in a paper but nobody seems to be using it (a part from me). And I decided to called prevaluation, as valuation is a very well-known notion so it is better not to create confusion.

#### Adam Topaz (Jan 19 2021 at 14:27):

@Xavier Xarles Can you send a link to this paper you mentioned?

#### Johan Commelin (Jan 19 2021 at 14:27):

Do they or you have any applications for such prevaluations that are not possible with the monoid-with-zero version?

#### Xavier Xarles (Jan 19 2021 at 14:30):

The link to the paper is: https://arxiv.org/abs/1308.0042 (it is publish in Duke). There is a not publish sequel in https://arxiv.org/abs/1410.4348

#### Adam Topaz (Jan 19 2021 at 14:31):

Thanks! (I have a student working on similar things right now)

#### Damiano Testa (Jan 19 2021 at 14:32):

On the compiling front: mathlib is now timing out on the file ring_theory/jacobson.lean and I do not know how to make it faster. One of the "slow" proofs is quite long, so maybe it should be split. For the moment, though, is it possible to instruct lean not to compile a file, or should I simply move it outside of its reach?

#### Xavier Xarles (Jan 19 2021 at 14:35):

@Johan Commelin They need in the construction of the "universal valuation", and you need the general version for this. Also for other constructions, as the "universal tropicalization". They would like to do "scheme theoretic" versions of these. In some some sense it is what I did in my preprint (I will send it to arxiv some day). But it is not used to solve really anything outside the theory... as far as I know.

#### Adam Topaz (Jan 19 2021 at 14:43):

This universal valuation looks exactly like something we might write in lean :)
(as a quotient of a giant inductive type, etc.)

#### Xavier Xarles (Jan 19 2021 at 14:46):

There is a quite natural construction of the universal valuation I do in my paper: it is "reminiscent" of the idempotent semiring of the ideals in a commutative ring.

#### Adam Topaz (Jan 19 2021 at 14:48):

I guess the key thing one must check to see whether there is a scheme-theoretic version of the universal valuation is whether the construction in the affine case is compatible with localizations. Is this condition easy to check?

#### Xavier Xarles (Jan 19 2021 at 14:50):

This is exactly one of the points: but it is quite easy, as valuation is a morphism of multiplicative monoids, and localization is about multiplicative monoids only...

#### Damiano Testa (Jan 19 2021 at 15:29):

Both on my computer and on the remote branch, the output of compiling mathlib has an output informing me that 3 proofs use sorry. I have sorried them myself, since they now time out.

Does this mean that everything else is in order? Or does it simply mean that once the compiling got to this file it ended its work?

#### Johan Commelin (Jan 19 2021 at 15:30):

no, that sounds like you are good

#### Johan Commelin (Jan 19 2021 at 15:30):

apart from those three sorrys

#### Damiano Testa (Jan 19 2021 at 15:31):

Ok, so the change allowing an ideal to take a comm_semiring instead of a comm_ring instance builds.

I have not yet moved anything to actually use this new generality, simply allowed Lean to have it.

#### Damiano Testa (Jan 19 2021 at 15:32):

So, now I have to fix the 3 missing proofs in src/ring_theory/jacobson.lean!

#### Johan Commelin (Jan 19 2021 at 18:41):

@Damiano Testa Great! And good luck with fixing those proofs. If you get stuck after and they fight back hard, I'm sure you can get some help here.

#### Damiano Testa (Jan 19 2021 at 19:10):

Ok, thanks! At the moment, I am trying to zoom in on the issue. It seems that there are some instances that lean is failing to find. I will try to narrow this down further

#### Damiano Testa (Jan 19 2021 at 19:11):

My strategy is to tear apart the proofs, to see if separately they compile: is this acceptable (assuming that it works)?

#### Johan Commelin (Jan 19 2021 at 19:14):

The statements typecheck, right? The problem is the proofs? I would just sorry parts of them, and try to narrow in like that.

#### Damiano Testa (Jan 19 2021 at 19:16):

Yes, the statements are ok. I think that it is one of the have in one proof that causes problems. I have not inspected the others yet: I'll try to find some time tomorrow

#### Xavier Xarles (Jan 22 2021 at 08:39):

Kevin Buzzard said:

Are "prime semi-ideals" the correct objects that one should use to make Spec? Or does one look at e.g. surjections from semirings to semi-integral-domains up to equivalence? Or are these the same thing?

Just one example that can be helpful in the "easiest" semiring $N$ of the natural numbers (including zero, of course). There is a unique maximal ideal, which is $N\{1}$. There are plenty of ideals whose saturation (=kernel of the quotient they generate) are the total ideal. So Spec(N) is huge. On the other hand, one can show that the "saturated prime ideals" are only the ones of the form pN, for p a prime number, so the "saturated spectrum" of N and the Spec of the integers are "the same".

#### Damiano Testa (Jan 25 2021 at 10:47):

Dear All,

I managed to push the comm_semiring branch so that it compiles! The only serious changes happened in file ring_theory/jacobson.lean. It is my opinion that several further proofs of the file can be simplified and sped up. However, for the moment, I am happy with the fact that I managed to make it work!

If anyone wants to take a look, I would be happy to listen to comments and suggestions!

#### Damiano Testa (Jan 25 2021 at 10:49):

More importantly, I would like to know if there is a consensus on whether to replace the definition of ideal to take a comm_semiring base, instead of a comm_ring base. This branch only changes the definition, but makes no use at all of the more general possibilities.

#### Johan Commelin (Jan 25 2021 at 10:52):

If it all compiles, I don't see any reason why we shouldn't go for it

#### Eric Wieser (Jan 25 2021 at 10:59):

branch#comm_semiring

#### Damiano Testa (Jan 25 2021 at 11:02):

Very well, so I will make a PR out of it and see what happens!

#### Damiano Testa (Jan 25 2021 at 11:10):

#5879

Bors seems to think that there are no issues!

#### Eric Wieser (Jan 25 2021 at 15:29):

On a related note, there are a bunch of places where assuming docs#integral_domain pulls in a comm_ring requirement where really only comm_semiring or even just semiring is needed. I've cleaned a few of those up in #5877. I imagine most of the uses of [integral_domain R] in mathlib are overly strict.

#### Damiano Testa (Jan 25 2021 at 16:14):

I am very happy that you are doing this change, Eric! I also think that most of the time that there is an assumption of integral_domain, simply knowing that multiplication by a non-zero element is injective would suffice!

#### Eric Wieser (Jan 25 2021 at 16:15):

Ah, unfortunately we don't have a typeclass that combines semiring with docs#cancel_monoid_with_zero without taking on extra assumptions as well

#### Damiano Testa (Jan 25 2021 at 16:39):

I think that there was a discussion of semidomain at some point... I did not manage to work on it, though. Let me see if I can find it!

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/left.2Fright.20cancelative.20semiring

#### Damiano Testa (Jan 25 2021 at 16:40):

About the comm_semiring change to ideal: it compiled! I feel very proud! :big_smile:

#### Kevin Buzzard (Jan 25 2021 at 18:09):

Yeah that is a really cool refactor. The thing that comes up now and again though is the fact that we don't have ideals for non-commutative rings, and that might well be a lot harder. But actually I wonder whether that should even be a refactor. There is no such thing as an ideal of a non-commutative ring, there's a left ideal, a right ideal and a bi-ideal.

#### Eric Wieser (Jan 25 2021 at 18:15):

The refactor would be to define ideal as the bi-ideal of a non-necessarily commutative ring, I think

#### Eric Wieser (Jan 25 2021 at 18:15):

Since when the ring is commutative, the bi-ideal and ideal coincide, right?

#### Mario Carneiro (Jan 25 2021 at 18:16):

I still think what I said above: an ideal should be a left ideal (because the definition is the same as in the commutative case), a right ideal shouldn't exist (it's a left ideal in the opposite ring), and a bi-ideal should be a different definition

#### Mario Carneiro (Jan 25 2021 at 18:17):

in a commutative ring all three concepts converge

#### Johan Commelin (Jan 25 2021 at 18:17):

I agree, except that I don't know if right ideals shouldn't exist. After all we also have sup and inf...

#### Johan Commelin (Jan 25 2021 at 18:17):

and order_dual

#### Mario Carneiro (Jan 25 2021 at 18:17):

I think we should try to avoid mentioning them until they become necessary for something

#### Mario Carneiro (Jan 25 2021 at 18:18):

and if that means they never get defined, great

#### Mario Carneiro (Jan 25 2021 at 18:19):

sup and inf are actually useful, this is more like mul and opposite-mul

#### Kevin Buzzard (Jan 25 2021 at 18:25):

Do we have submodules of a non-commutative R-module? Those will be left ideals I guess.

#### Eric Wieser (Jan 25 2021 at 18:26):

I don't think docs#submodule requires commutativity (so yes)

#### Aaron Anderson (Jan 25 2021 at 18:29):

Mario Carneiro said:

I think we should try to avoid mentioning them until they become necessary for something

I think the only circumstance where I really would want to define right-submodules is if it's a more useful way to define bi-submodules

#### Damiano Testa (Jan 26 2021 at 03:22):

I will keep in mind the comm_semiring/semiring issue while refactoring. I agree that getting left-ideals should be easy.

I also agree with Mario that I would add right ideals on a need-to-use basis: duplicating code is a lengthy and imprecise process. My experience of working with dual/opposites is limited and unsuccessful. For this reason, I would either try to avoid right ideals, or duplicate the needed lemmas only. Of course, if someone else is able to make Lean understand the companion version of every lemma, that would be awesome!

#### Kyle Miller (Jan 27 2021 at 20:49):

Jumping into this discussion without too much context, have you considered defining subbimodules and then having a left (resp. right) ideal of $R$ be a $(R,\mathbb{Z})$-submodule (resp. a $(\mathbb{Z},R)$-submodule), where an ideal is an $(R,R)$-submodule? It's not uncommon needing to deal with left and right ideals simultaneously (one example is left and right annihilators of right and left ideals in Frobenius algebras). It's also useful being able to consider relationships between $(R,\mathbb{Z})$-submodules and $(R,A)$-submodules for $A$ a subring of $R$, so, when possible, it might be worth generalizing statements about left ideals to ones where $A$ can be anything. Doing this also all sounds like a lot more work with no immediate benefit, so take it with a grain of salt. :smile:

#### Damiano Testa (Jan 29 2021 at 14:29):

Continuing with the refactor, I have now changed many lemmas in ring_theory/ideal/basic so that they use comm_semiring instead of comm_ring.

Besides removing assumptions from further "easy" lemmas, the main sticking point is going to be dealing with quotients. As I have not really given the issue of quotients in a comm_semiring much thought, I will not start doing this anytime soon. However, from the discussion above, it seems that @Xavier Xarles and @Marc Masdeu have been working on this. I hope that this refactor will be useful to them!

PR #5954

#### Kevin Buzzard (Jan 29 2021 at 14:31):

In commutative ring theory the correct thing to quotient out by is an ideal. In semiring theory this is no longer the case, I suspect, so maybe it's easiest just to leave the quotients alone.

#### Kevin Buzzard (Jan 29 2021 at 14:32):

I don't think we have normal submonoids, and this is probably for the same reason.

#### Adam Topaz (Jan 29 2021 at 14:33):

There's a general notion of "congruence relations" (I can't remember the name right now...) in the context of universal algebra which tells you exactly what the condition on a relation you need so that the quotient inherits the algebraic structure. This is the thing that one has to use for quotients of objects like semirings and monoids.

#### Xavier Xarles (Jan 29 2021 at 14:34):

I don't know if you did the prime ideals part. The proof of maximal implies prime needs to be redone: Marc and myself have a wrote a proof with lean that work for any comm_semiring.
About quotients, there are some dificulties as quotients with respect to a ideal in comm_semirings can be defined, but the standard way is to do it through "congruences", that is one of the things we are doing.

#### Damiano Testa (Jan 29 2021 at 14:34):

Kyle, did I understand correctly that you would like to also remove the commutative assumption on the ring? I like the idea of removing it, however, out of prejudice, I think that it might be easier to first get rid of additive inverses and then to go with non-commutativity. Do you agree?

#### Johan Commelin (Jan 29 2021 at 14:35):

We have congruence relations on monoids in mathlib.

#### Johan Commelin (Jan 29 2021 at 14:35):

@Xavier Xarles :up:

#### Damiano Testa (Jan 29 2021 at 14:35):

Xavier, I also have rewritten that proof: it is contained in the current PR #5954 (which is not in mathlib, and is building at the moment).

#### Xavier Xarles (Jan 29 2021 at 14:35):

Johan Commelin said:

We have congruence relations on monoids in mathlib.

Yes, that's what we used.

#### Johan Commelin (Jan 29 2021 at 14:36):

Ok, great :thumbs_up:

#### Damiano Testa (Jan 29 2021 at 14:37):

Kevin, I agree with you. For the moment, I do not plan to touch quotients!

#### Adam Topaz (Jan 29 2021 at 14:39):

Oh, and the so-called ring_quot in mathlib docs#ring_quot is actually a semiring_quot.

#### Damiano Testa (Jan 29 2021 at 14:50):

One thing that I noticed is that a local ring is defined to be one for which either for every a in the ring, a or 1-a is a unit. While I do not know if local_semiring are useful, the definition would also apply to comm_semirings if we required a or 1+a to be a unit.

This definition is equivalent to the given one for comm_rings. What do people think of replacing the - by a + in

class local_ring (α : Type u) [comm_ring α] extends nontrivial α : Prop :=
-- old
-- (is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))
-- candidate
(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 + a)))


#### Adam Topaz (Jan 29 2021 at 14:51):

You can say that for all a b such that 1 = a + b, at least one of a or b is a unit.

#### Adam Topaz (Jan 29 2021 at 14:51):

That would be more symmetric.

#### Adam Topaz (Jan 29 2021 at 14:52):

And IMO this definition makes sense from the point of view of localizations of semirings

#### Damiano Testa (Jan 29 2021 at 14:55):

Adam, I like your definition, but I wonder whether using two variables summing to one is "Lean-better" than having a single variable. As you know much more about Lean than I do, I defer this to you!

#### Adam Topaz (Jan 29 2021 at 14:57):

This suggestion is from my mathematical taste, not really from my experience with lean ::)

#### Adam Topaz (Jan 29 2021 at 14:57):

@Johan Commelin @Kevin Buzzard what do you think?

#### Kevin Buzzard (Jan 29 2021 at 15:19):

I don't care what the definition says as long as anyone who fiddles with it reproves all of the API.

#### Kevin Buzzard (Jan 29 2021 at 15:20):

And if the new proofs turn out to be twice as long you might have a hard job convincing the maintainers that this is a move in the right direction. However I suspect this will not happen -- the new proofs will probably be about the same size as the old ones

#### Kevin Buzzard (Jan 29 2021 at 15:22):

Damiano, if you're amused by the definition of local ring, I have this vague memory that lean's definition of a local homomorphism doesn't assume that the source and target are local

#### Kevin Buzzard (Jan 29 2021 at 15:22):

Of course it coincides with the correct definition when they are

#### Kevin Buzzard (Jan 29 2021 at 15:23):

A nice summary of the local homomorphism story is "email from Buzzard to Conrad and de Jong", I'll dig it out

#### Damiano Testa (Jan 29 2021 at 15:24):

Whenever I hear these things, it always makes me wonder what it means that you develop an "intuition" for mathematical concepts, when these concepts are then so far from what you actually use in implications...

#### Adam Topaz (Jan 29 2021 at 15:40):

I don't know if you're into to this kind of thing @Damiano Testa , but you might be able to get some intuition from this paper:
https://doi.org/10.1016/0021-8693%2877%2990284-8

#### Adam Topaz (Jan 29 2021 at 15:42):

(see e.g. the bottom of page 242 for the "definition" of a "local ring")

#### Kevin Buzzard (Jan 29 2021 at 16:17):

A local ring homomorphism is usually defined in the books as f:R->S such that f(m_R) is a subset of m_S. The person who typed this definition into Lean went with the logically equivalent statement that if f(r) is a unit, then r is a unit. The linter immediately observed that the assumption that R and S were local was superfluous and this was a definition which made sense for an arbitrary ring homomorphism. OK. So it's the same situation -- the definition of local ring hom in Lean now doesn't assume that R and S are local, it just says that f is a ring hom such that if f(r) is a unit then r is a unit.

So yesterday I was doing some stuff with multivariable polynomials, and I changed a bit the proof that if A and B were local, and f:A->B was a local homomorphism then so was the induced ring hom A[[X]]->B[[X]] (here X can be a set of variables if you like). I was amused that the linter then complained about this lemma! It claimed that I didn't need A or B to be local in my proof. And indeed it's right -- an element of a power series ring is a unit iff the constant term is a unit.

I then mentioned this to Johan Commelin and Kenny Lau (two other Lean people interested in alg geom; Kenny is an UG at Imperial and Johan a post-doc in Freiburg). Some random thoughts came out of this. Any inclusion of number fields gives an inclusion of rings of integers which is a "local ring hom" in the above sense. More generally any injective integral extension is a local ring hom (I'm pretty sure I've seen this proof before recently, maybe it comes up in the proof of the Nullstellensatz?). If Spec(f): Spec(S)->Spec(R) is surjective then f is a local ring hom. Then we found this: https://stacks.math.columbia.edu/tag/00GQ, so clearly the idea has come up before. Is this concept of being a local ring hom, in the non-local setting, useful in some way? Discovered by a computer :-) Presumably discovered by a human first? I think a logician might say something like "f reflects units" or something?

#### Kevin Buzzard (Jan 29 2021 at 16:20):

De Jong's reponse:

Comments: (1) if k is a field and f : k[x_1, \ldots, x_n] ---> k[y_1,
..., y_m] is a k-algebra map, then f is "local" in your sense if and
only if f(x_1), ..., f(x_n) are algebraically independent. (2) If A =
Gamma(C, O_X) where C is an affine smooth curve over a field and if B
= Gamma(C - P, O_C) where P is a closed point on C which has infinite
order in the class group of C then A ---> B is "local" in your sense.

There are many ways that we could have generalized "local homomorphism
of local rings" to ring maps. For example given f : R ---> S we could

(a) f reflects units (what you said)
(b) the image of Spec(f) contains all closed points
(c) Spec(f) sends closed points to closed points

Observe that (b) implies (a). If I had to make a definition which
applies to general rings I might have chosen the condition "(b) +
(c)". But I understand that when formalizing it is very natural to
choose (a).

#### Damiano Testa (Jan 29 2021 at 21:19):

Dear Kevin,

thank you very much for digging this conversation out: it is very interesting!

Last updated: May 18 2021 at 07:19 UTC