(comm_)semiring: examples?

Stream: maths

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Mario Carneiro]

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]

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

[Damiano Testa]

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]

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]

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]

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]

no but you get the idea

[Mario Carneiro]

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

[Damiano Testa]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Adam Topaz]

One nice exercise is to classify all semiring quotients of nat

[Damiano Testa]

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

[Adam Topaz]

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

[Damiano Testa]

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

[Mario Carneiro]

What are semiring quotients defined as?

[Adam Topaz]

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

[Adam Topaz]

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

[Damiano Testa]

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]

https://arxiv.org/abs/1310.3013

[Mario Carneiro]

The extra element has to be the one

[Damiano Testa]

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]

semiring homs fix both 0 and 1

[Damiano Testa]

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

[Mario Carneiro]

they aren't necessarily different

[Mario Carneiro]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

Ok, these two choices seem to be

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

[Kevin Buzzard]

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]

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]

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]

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]

Of course any theorems about submodules should be stated on submodules

[Kevin Buzzard]

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]

Fortunately docs#ring_quot works for semirings :)

[Kevin Buzzard]

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

[Damiano Testa]

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]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

that's my suggestion, yes

[Damiano Testa]

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

[Damiano Testa]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

Unless there are typeclass subtleties

[Johan Commelin]

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]

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]

@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]

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]

That's exactly how you test it

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

ah, ok!

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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]

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

[Damiano Testa]

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

[Mario Carneiro]

branches are compiled

[Damiano Testa]

ok, thanks!

[Patrick Massot]

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]

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]

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

[Damiano Testa]

Kevin, it is here:

Branch 'comm_semiring'

[Damiano Testa]

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]

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]

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]

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]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

Just compile locally.

[Kevin Buzzard]

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

[Damiano Testa]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Damiano Testa]

you can get more than cache?

[Damiano Testa]

cash?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Damiano Testa]

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]

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]

Unfortunately not to Patrick!

[Patrick Massot]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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]

@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]

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

[Johan Commelin]

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

[Xavier Xarles]

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]

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

[Damiano Testa]

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]

@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]

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

[Xavier Xarles]

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]

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]

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]

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]

no, that sounds like you are good

[Johan Commelin]

apart from those three sorrys

[Damiano Testa]

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]

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

[Johan Commelin]

@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]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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

[Eric Wieser]

branch#comm_semiring

[Damiano Testa]

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

[Damiano Testa]

#5879

Bors seems to think that there are no issues!

[Eric Wieser]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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

[Mario Carneiro]

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]

in a commutative ring all three concepts converge

[Johan Commelin]

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

[Johan Commelin]

and order_dual

[Mario Carneiro]

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

[Mario Carneiro]

and if that means they never get defined, great

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Aaron Anderson]

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]

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]

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]

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]

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]

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

[Adam Topaz]

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]

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]

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]

We have congruence relations on monoids in mathlib.

[Johan Commelin]

@Xavier Xarles :up:

[Damiano Testa]

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]

Johan Commelin said:

We have congruence relations on monoids in mathlib.

Yes, that's what we used.

[Johan Commelin]

Ok, great :thumbs_up:

[Damiano Testa]

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

[Adam Topaz]

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

[Damiano Testa]

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]

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]

That would be more symmetric.

[Adam Topaz]

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

[Damiano Testa]

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]

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

[Adam Topaz]

@Johan Commelin @Kevin Buzzard what do you think?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

Of course it coincides with the correct definition when they are

[Kevin Buzzard]

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

[Damiano Testa]

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]

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]

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

[Kevin Buzzard]

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]

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
ask

(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]

Dear Kevin,

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