Noncommutative ring things

Stream: mathlib4

[Haruhisa Enomoto]

Hello. I'm studying representation theory of non-commutative algebras. A little over a year ago, I asked questions about how 2-sided ideals, right ideals, bimodules, can be formulated, or were not formulated in mathlib 3.
I left Lean 3 alone for a while, and I recently got interested in Lean 4 again. As far as I can see in mathlib4 docs, currently:

• Right or two-sided ideals are not defined (but could be implemented easily using subbimodule), so quotient ring is only implemented for commutative ring.
• Tensor product (of right modules and left modules) are only defined for two modules over a commutative ring (so flatness is only defined for commutative case).

I definitely want them, but for example if I implement and generalize definition to non-commutative setting, lots of works should be done for previous commutative ring statements to work (so maybe making a new project for my own noncommutative purpose is easier). So is there anyone working for this direction? Or maybe there are very few people who want non-commutative things in mathlib4?

[Jireh Loreaux]

I definitely want all the noncommutative ring things, especially two-sided ideals. Unfortunately, I also want them for non-unital rings, so I've been holding off. But I think @Eric Wieser may have been working on the tensor product of non-unital algebras. Also pinging @Oliver Nash since we had a discussion about two-sided ideals in non-unital rings a few months ago.

[Anatole Dedecker]

We definitely want all of this, it’s mostly a matter of manpower and finding reasonable APIs (the main point, as you said, is making sure that everything still works transparently in the commutative case)

[Eric Wieser]

We're still a very long way from tensor products of modules over non-commutative rings; the work I did on this was a lean3 branch that never got merged, and it touches so many files that porting it is essentially starting from scratch.

[Eric Wieser]

However, we can get the tensor product of non-associative and non-unital algebras quite easily

[Kevin Buzzard]

What always concerns me about the proposals for noncommutative ideals is that people always bring in things like the opposite ring because we have an aversion to right actions, and this isn't at all what the paper literature looks like

[Haruhisa Enomoto]

So is it true that currently every action in mathlib is left action, and introducing right action (like right ideals, right modules, etc) is not recommended (and instead use left action of opposite ring) in mathlib community?

[Kevin Buzzard]

I rather like the idea of having a new piece of notation for right actions

[Eric Wieser]

We can have new notation without a new typeclass

[Anatole Dedecker]

I agree with Eric. We definitely want some notation, but it’s not a big deal if internally it’s implemented as a left action from the opposite ring.

[Eric Wieser]

The big blocker right now is that we need Algebra to mean "left and right module", otherwise nothing we develop for right-modules will work for algebras. That was the goal of the stuck-in-lean3 !3#10716

[Anatole Dedecker]

Actually this goes way beyond rings, it would be nice to have a better notation for right group actions. A naive idea that will probably introduce diamonds would be to have something like instance [SMul G\mop M] : SMul M G. But another notation would work to

[Eric Wieser]

Note that "full" (i.e. diamond-free) support for right actions (via a new typeclass or otherwise) require us to add right_nsmul and right_zsmul and right_qsmul fields to field, along with the 6 new proof fields to keep them happy, and the 7 corresponding fields about pow and zpow to keep to_additive happy. So a 16-field increase in total.

[Anatole Dedecker]

I think this kind of long term thing is perfectly suited to GitHub projects, someone who has spent some time thinking about this should make some kind of general blueprint that we can refine over time.

[Eric Wieser]

!3#10716 opted to ignore this and put up with diamonds, to avoid the scope becoming unmanageable

[Kevin Buzzard]

It would be good to record these thoughts somewhere easy to find, because I'm sure they've come up before but Zulip is now very big to search

[Haruhisa Enomoto]

So I personally want right actions, but I'm wondering that if we add right actions (right modules, etc), then should we make a right-action-counterpart of every existing theorem about left actions? Or maybe we can use to_additive-like automation?

[Eric Wieser]

We have right actions already via MulOpposite, and a reasonable number of constructions that use them

[Eric Wieser]

Perhaps the spelling is ugly, but it's not the main problem here

[Eric Wieser]

(as an example, docs#TrivSqZeroExt.semiring works only on bi-modules)

[Yaël Dillies]

The idea here is to avoid all duplication by considering a right R-action as a left Rᵐᵒᵖ-action (docs#MulOpposite).

[Yaël Dillies]

(I sent that message an hour ago, rip)

[Eric Wieser]

Kevin Buzzard said:

It would be good to record these thoughts somewhere easy to find, because I'm sure they've come up before but Zulip is now very big to search

I'll make a mathlib4 issue to summarize the changes that went into the mathlib3 PR, and why we need them

[Kevin Buzzard]

I was happy to ignore non-commutative rings for many years because I wanted to push algebraic geometry at least as far as schemes, and there only commutative rings were necessary. But at some point we have to get non-commutative rings working.

[Eric Wieser]

My claim is that the obstacles are, in order:

• making algebras imply right actions without diamonds
• refactoring tensor products to actually be meaningful on left/right modules
• documentation and reducing verbosity

[Eric Wieser]

Until we do that first step, our non-commutative results can't be applied to the commutative setting

[Anatole Dedecker]

I would exchange your last two points, I don’t think tensor products are the most urgent things here (and we already have plenty of things to do about tensor products in the commutative world). For example being able to quotient an algebra by a bi-ideal feels way more fundamental to me (am I right that we don’t have this?)

[Kalle Kytölä]

Yes, last time I checked we didn't have quotients of algebras (or rings). So I believe in Mathlib we cannot currently even state the First Isomorphism Theorem for Algebras (or Rings). :cry:

[Eric Wieser]

I think we could state it today using docs#RingCon instead of a BiIdeal, but I agree that's not ideal

[Eric Wieser]

(I don't think docs#RingCon.ker exists, but it easily could (as the ring version of docs#Setoid.ker))

[Eric Wieser]

To be clear: we have the quotients, just not the ideals

[Kalle Kytölä]

Ok, I agree there are workarounds to state it. But the usual statement is that for an algebra homomorphism $\varphi \colon A \to A'$, the kernel $\mathrm{Ker}(\varphi) \subset A$ is an ideal (2-sided), and quotients $A/I$ of algebras are defined for ideals (2-sided), and $A/\mathrm{Ker}(\varphi) \cong \varphi(A) \subset A'$ as an algebra. I think stating this without ideals (2-sided) and quotients by ideals does not accurately correspond to the mathematical statement.

[Eric Wieser]

I think the statement would look pretty much the same whether ker is an ideal or a RingCon, since the two are isomorphic anyway and the syntax wouldn't need to change. I understand it's desirable to talk about ideals to match the commutative case

[Kalle Kytölä]

Sure. But I think we also do want to match the math usage of quotients in algebra context (not just type-theoretically / quotients by equivalence relations).

[Eric Wieser]

Do we actually care about right-/left- ideals, or only two -sided ones?

[Eric Wieser]

(that is; are we currently avoiding the two-sided ones because of my first point about the commutative case?)

[Kalle Kytölä]

For quotient algebras 2-sided ideals. For other purposes both. For example you can construct a module over an algebra by quotienting by a one-sided ideal (quotient by a left ideal gives a left module, if I don't have my terminology backwards).

[Eric Wieser]

But you can also just call that a quotient by a Submodule R R, right?

[Kalle Kytölä]

So quotient left-modules are satisfactory as they are. Quotient algebras don't (in my interpretation) exist in Mathlib yet.

[Eric Wieser]

I'm asking if we can redefine ideal to only be two-sided, and if anyone will care

[Eric Wieser]

(after we refactor algebras; before we do that the answer is "yes, everyone doing commutative rings")

[Kalle Kytölä]

Eric Wieser said:

I'm asking if we can redefine ideal to only be two-sided, and if anyone will care

I'm also interested in whether anyone would mind! For the commutative case it doesn't make a difference. In the noncommutative case the 2-sided ideal seems like the most important notion (the kernel of a homomorphism, i.e., the thing you quotient by).

And at least for algebras and Lie algebras etc. the notion of left ideals is the same as a submodule of the algebra viewed as a module over itself. Are there any situations when left ideals would not be submodules, or where treating them as submodules would not be satisfactory? (I'm assuming the implementation of right modules and right ideals will be figured out and then the same goes for them.)

[Kevin Buzzard]

Left ideals are just R-submodules of R, and I guess people care about modules and submodules in the noncommutative case.

[Kevin Buzzard]

Of course, we might find that people are happy to call them submodules rather than left ideals (I think that dropping the concept of ideal completely and only using submodule language would have had rather more pushback from the commutative people)

[Eric Wieser]

Right ideals are Submodule Rᵐᵒᵖ R

[Haruhisa Enomoto]

I agree that we don't need left ideals and right ideals (actually in rep theory of algebras, one-sided ideals rarely appear since they're just submodules and rep theory doesn't like ideal theory). So as for ideals, I want only two-sided ideals.
But currently ideal in mathlib is defined to be left ideal, so some terminology or definition should be fixed (if we don't need one-sided ideal). For example, ideally we replace the definition of ideal in mathlib to be two-sided?

[Kevin Buzzard]

The definition of group in mathlib contains axioms which follow from other axioms (for example we have both mul_one and one_mul because it extends monoid, but one of these can be dropped in the presence of inverses) so, whilst it would be a big refactor, it would not be inconsistent with our set-up to have ideals defined as two-sided ideals.

[Anatole Dedecker]

Kalle Kytölä said:

I think stating this without ideals (2-sided) and quotients by ideals does not accurately correspond to the mathematical statement.

I'm contradicting myself a bit here, but actually I think it does, and I would be very happy(*) if we played with equivalences relations the same game we have for subobjects. But of course we would at least need a proper theory of two-sided ideals to state that such an ideal defines a ring congruence.

(*) me being happy does not mean it's the right solution, I'm not seriously suggesting we should just work with ring congruences, just that in my mind it's the right concept, and ideals are just a nice way to represent them.

[Eric Wieser]

Ring congruences also generalize to semirings where quotients by ideals don't

[D. J. Bernstein]

In the study of elliptic curves, one type of object that naturally appears is an ideal "connecting" two subrings R, S of a quaternion algebra, meaning that I is simultaneously a left ideal of R and a right ideal of S. It's not surprising for a paper on this topic such as https://eprint.iacr.org/2022/234 to use the word "ideal" more than 100 times and to use the word "module" exactly 0 times.

[Jireh Loreaux]

Also, as I've already stated: we need to think about the non-unital case. For example, Kevin's claim that left ideals are just R-submodules of R is not true whenever you want an ideal of a non-unital ring.

Now, maybe the answer is to define it in terms of the unitization, but this gets a bit complicated quickly once you want to start talking about 2-sided ideals as subbimodules of the unitization of the tensor product. I'll ping @Oliver Nash again because I think I convinced him that there's a real issue here a few months back.

Mainly I'm trying to avoid the need for us to refactor all the two-sided ideal theory again in a few months when we eventually want it for non-unital rings.

[Jireh Loreaux]

But this is why I want non-unital tensor products.

[Eric Wieser]

Jireh Loreaux said:

But this is why I want non-unital tensor products.

Do you mean where the central ring is non-unital, or where the two modules are only slightly rings?

[Eric Wieser]

(I am happy to build the latter, but I want to wrap up #6778 first so that I don't make it timeout in doing so)

[Jireh Loreaux]

Right, the latter is what I want. In particular, what I need is the tensor product of two non-unital algebras over a unital (semi)ring.

[Jireh Loreaux]

@Anatole Dedecker , @Kevin Buzzard I don't understand the reason for the fear emoji.

[Anatole Dedecker]

For me it’s the size of the refactor, and also the fact that algebraists had managed to convince me that everything was just submodules so didn’t even think about this being an issue

[Anatole Dedecker]

But I definitely agree we have to do it in some form at some point

[Johan Commelin]

I guess it's not fear for non-unital rings, but fear induced by the realization that if we aren't careful we will do a boatload of work and then realize that we need to do another boatload of work.

[Kevin Buzzard]

I was just shocked that ideals weren't the same as submodules :-)

[Jireh Loreaux]

Kevin, it's only for the stupid technical reason: you can't state docs#Module.one_smul because there is no 1. Ideals in non-unital rings are "non-unital submodules" (i.e., submodules where you delete all references to 1).

[Jireh Loreaux]

See also https://ncatlab.org/nlab/files/QuillenModulesOverRngs.pdf, where it is also mentioned that a non-unital module is just a unital module over the unitization.

[Anatole Dedecker]

Thinking again about this "ideal are not submodules" issue, I think we should just embrace non-unitality and define pseudo-modules (Bourbaki terminology) over non unital rings (which Bourbaki calls pseudo-rings, should we rename docs#NonUnitalRing ?), and generalizing docs#Submodule to this situation. Fortunately enough the definition of Submodule doesn't mention ones, so we can just keep only one definition.
This sound to me like a safe refactor that wouldn't induce significantly more work when we want to move to left-right modules, does that sound good?

[Eric Wieser]

Submodule R M requires R to have a 1

[Eric Wieser]

Which means that you can't use it for Submodule R R over these pseudo-rings

[Yaël Dillies]

Eric Wieser said:

Submodule R M requires R to have a 1

Okay, but there's no need to, right?

[Anatole Dedecker]

My point is exactly that we don’t have to duplicate submodules and linear maps since they don’t mention 1. I think that makes this refactor significantly more manageable

[Eric Wieser]

Ah, in which case I attempted an easier version of this in !3#6642 and had performance issues

[Eric Wieser]

Eric Wieser said:

Kevin Buzzard said:

It would be good to record these thoughts somewhere easy to find, because I'm sure they've come up before but Zulip is now very big to search

I'll make a mathlib4 issue to summarize the changes that went into the mathlib3 PR, and why we need them

#7152 is that issue

[Anatole Dedecker]

Oh right it even works for DistribMulAction

[Eric Wieser]

DistribMulAction still requires 1 : R

[Jireh Loreaux]

Note that still doesn't solve the unital issue: even a MulAction requires a 1. We have no non-unital smul actions in mathlib (except for just the data SMul). So, in order to solve this problem, you either need to make it work over the unitization, or you need to define an entire hierarchy of non-unital actions. This was the conclusion I came to with Oliver months ago.

[Eric Wieser]

Presumably the same comment applies to non-associative actions? Or are those nonsense?

[Yaël Dillies]

Is there any problem with non-unital actions?

[Eric Wieser]

The fact we have no lemmas about them

[Jireh Loreaux]

I have never worked with non-associative actions, so :shrug:

[Jireh Loreaux]

The tricky bit about using the unitization is that you need different ones depending on whether you have a semiring or a ring (\N vs \Z), which is super annoying.

[Anatole Dedecker]

Oh I didn’t realize the issue was that deep. I think there’s no point of trying to rely on the unitization at the level of the actions, we should just rename MulAction to MonoidAction and remove the unit for MulAction. It will take some time, but imo that’s clearly the right approach here. Really the only thing I’m worried about is performance issues

[Johan Commelin]

If non-unital rings are pseudorings, will semigroup actions be called pseudoactions?

[Jireh Loreaux]

I would prefer not to change the name to pseudo at all.

[Jireh Loreaux]

That prefix is overused in general, not used for this in the literature I read, and NonUnital is more informative.

[Anatole Dedecker]

I am not strongly attached to Pseudo, but NonUnitalModule sounds a bit weird to me

[Antoine Chambert-Loir]

Non-something is almost always bad terminology, especially when a something stuff can be Non-something.

[Jireh Loreaux]

Yeah, well I think my head would roll if I proposed we switch Ring to UnitalRing, but for sure my preference is to add the adjectives to the unital version.

[Jireh Loreaux]

I proposed we switch the notation for RingHom a while back and the poll was more than a little one-sided.

[Johan Commelin]

I think unital rings are extremely common in many parts of maths, so I wouldn't want to make Ring longer. We already have to live with CommRing even though it's a well-known folklore result that all rings are commutative. :stuck_out_tongue_wink: :see_no_evil:
@Jireh Loreaux I know that non-unital rings are sometimes called Rng, which I understand might be a bit tongue-in-cheek. But it does have the big advantage that it's a very short name. What do you think of it?

[Anatole Dedecker]

I hate Rng because I have to look very hard to see that there is no i. I guess it’s less of a problem with a mono space font, but I’m still not a big fan

[Eric Wieser]

In some of my slides I used NUNARing as shorthand for NonUnitalNonAssocRing; @Yaël Dillies thought this was a good idea to apply to mathlib, but I'm on the fence

[Jireh Loreaux]

I prefer to avoid acronyms wherever possible. Otherwise people are going to wonder "what's a NUNA ring? I've never heard of that?" I'm not saying for sure we shouldn't do it, but that's my concern. One advantage is that it shortens things everywhere, whereas if we use Rng we still need docs#NonUnitalSubalgebra.

[Eric Wieser]

NonUARing is possibly a slightly better compromise

[Ruben Van de Velde]

MaybeUnitalRing?

[Jireh Loreaux]

Johan, to answer your question explicitly, while Rng does have the advantage of being short, I've never been a fan because (a) it makes it hard to pronounce (b) it looks like an abbreviation of Range and (c) that trick doesn't generalize to other objects.

[Jireh Loreaux]

How do we feel about the following plan of attack for getting 2-sided ideals of non-unital rings? The idea would be to create a GitHub project to track all the substeps of this if we can agree on the general framework:

1. Develop the hierarchy of non-unital actions (or some subset thereof) parallel to the unital ones. Maybe even non-unital versions of MulAction and Module are enough for now.
2. Execute a renaming if desired after lots of bikeshedding.
3. Generalize the typeclass assumptions of Submodule.
4. Define the tensor product of non-unital rings (Eric has already done this I think).
5. Define two-sided ideals as subbimodules of this tensor product (over ℕ or ℤ).
6. Provide the natural equivalence between left ideals and 2-sided ideals in the commutative case.
7. Refactor quotients to use two-sided ideals so that it works for non-commutative rings.

[Johan Commelin]

That overall strategy looks solid to me.

I have one question: should the definition of two-sided ideal really depend on tensor products? Or can we just give a hands-on definition?

[Eric Wieser]

Note we already have docs#Subbimodule.mk, but to use it on commutative rings we need #7152 which is not on your list.

[Eric Wieser]

But indeed, defining things via tensor products worries me; not only does it require a non-canonical typeclass instance, but I worry it will be harder on TC performance too

[Jireh Loreaux]

If we're not going to define it through tensor products and we're just going to hand roll it, then there's not much point to the above plan.

[Jireh Loreaux]

I would have hand-rolled a long time ago but the consensus was: wait for Subbimodule

[Eric Wieser]

I think the claim was that we should hand-roll Subbimodule

[Eric Wieser]

Not the special case of two-sided ideals

[Jireh Loreaux]

ah, okay

[Eric Wieser]

I'm a little surprised we have Subbimodule.mk but not an abbrev for the type itself

[Johan Commelin]

Right, I suggest moving 4 to the end of the list. (It's good to do it, but it shouldn't block 5-7.)

[Jireh Loreaux]

Wait, Johan, you mean move step 4 to the end of the list and put a new step 4' in its place which is: "redefine subbimodules to be hand-rolled as opposed to using the tensor product." Correct?

[Eric Wieser]

I think we still need "Make algebras bimodules" before that step

[Eric Wieser]

(It can of course happen in parallel with this action refactor)

[Eric Wieser]

Though I suspect the action refactor can't happen until we improve elaboration of with in instances, due to performance problems

[Eric Wieser]

Eric has already done this I think

Yes, the tensor product of non-unital rings is in #7106

[Eric Wieser]

The writing on the wall here: that change makes Mathlib/RingTheory/Kaehler time out

[Jireh Loreaux]

What doesn't? :laughing:

[Jireh Loreaux]

But point taken

[Jun Yoshida]

Do we have any special notation for MulOpposite.op r • x, or any plan?

[Eric Wieser]

The notation x <• r has been discussed before

[Eric Wieser]

I think one or two files use it locally

[Jun Yoshida]

Are they in Mathlib? grep couldn't find them.

[Jireh Loreaux]

I can't find it in either mathlib3 or mathlib4. I remember it being proposed, but not adopted. Maybe a few files used it at one time but don't any longer?

[Eric Wieser]

Eric Wieser said:

My claim is that the obstacles are, in order:

• making algebras imply right actions without diamonds
• refactoring tensor products to actually be meaningful on left/right modules
• documentation and reducing verbosity

Note that I consider getting this notation working as much lower priority than making algebras imply right actions. There's no point having nice notation if we still can't use it for anything (without breaking other users)

[Eric Wieser]

Some examples of where I'd like to use right actions:

• docs#Derivation
• docs#QuadraticForm

In both cases, adding the notation and switching to using right actions with it would make those types unusable on things like the complex numbers as a real-vector space!

[Jireh Loreaux]

I've created https://github.com/orgs/leanprover-community/projects/11/views/1

[Eric Wieser]

I added my previous issue to that page

[Jun Yoshida]

I understand the plan. Anyway, I'm glad to know the pre-official notation; I'll use it locally in my project.

[Anatole Dedecker]

I'm late to the party, but a few comments:

• I agree that using tensor product as a base ring, while it was a nice trick, doesn't seem scalable enough to make that much things depend on it
• I was surprised by Eric's claim that making algebras bi-modules is the first thing to do, but having a look at the issue I undestand that thing are worse than I expected. Still, I think this doesn't completely block starting to develop the theory of bi-modules and so on, but it means that we can't apply this theory to algebras for now.

[Eric Wieser]

Still, I think this doesn't completely block starting to develop the theory of bi-modules and so on, but it means that we can't apply this theory to algebras for now.

My impression was that in a lot of places, we don't actually want to develop new theory, but instead generalize existing theory. And that's what we can't do until algebras are bimodules, otherwise we're not actually making a true generalization.

[Anatole Dedecker]

Okay I get your point

[Eric Wieser]

Eric Wieser said:

Eric has already done this I think

Yes, the tensor product of non-unital rings is in #7106

This has some pretty bizarre benchmark results. Everything got faster except the total build time which is almost 1.5x what it was before!

[Eric Wieser]

  Benchmark                                           Metric         Change
  =========================================================================
- build                                               wall-clock      37.1%
+ lint                                                wall-clock      -6.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange   instructions    -6.3%
+ ~Mathlib.LinearAlgebra.Coevaluation                 instructions    -8.5%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite       instructions   -23.4%
+ ~Mathlib.RingTheory.MatrixAlgebra                   instructions   -25.1%

[Eric Wieser]

wat

[Jireh Loreaux]

Re-run it. It's probably a fluke thing.

[Eric Wieser]

That didn't help, but merging master did

[Eric Wieser]

So overall this actually seems to have made performance better!

[Kevin Buzzard]

While we're waiting for a two-sided ideal type, would this definition be considered harmful?

import Mathlib.RingTheory.Ideal.Basic

def Ideal.IsTwoSided {R : Type _} [Semiring R] (I : Ideal R) : Prop :=
  ∀ (r i : R), i ∈ I → i * r ∈ I

We could then make definitions such as

def Ring.IsSimple {R : Type _} [Semiring R] [Nontrivial R] : Prop :=
  ∀ I : Ideal R, I.IsTwoSided → I = ⊥ ∨ I = ⊤

and then go on to define central simple algebras, do quaternion algebras properly etc (our current definition of quaternion algebra is wrong in the sense that, like our definition of elliptic curve, it makes sense in more generality than the collection of rings for which it gives the correct answer)

[Eric Wieser]

Can we already write the following?

def Ring.IsSimple {R : Type _} [Semiring R] [Nontrivial R] : Prop :=
  ∀ I : RingCon R, I = ⊥ ∨ I = ⊤

[Eric Wieser]

(ah, this needs !3#18588, but that should be easy enough to send through mathport)

[Kevin Buzzard]

Eric Wieser said:

Can we already write the following?

def Ring.IsSimple {R : Type _} [Semiring R] [Nontrivial R] : Prop :=
  ∀ I : RingCon R, I = ⊥ ∨ I = ⊤

Sure, if we're happy to have a definition which will completely bamboozle essentially all readers.

[Kevin Buzzard]

(I guess our definition of group completely banboozles essentially all readers, so it's not like there's no precedence here...)

[Kevin Buzzard]

A back of an envelope calculation indicates that these two definitions of IsSimple might give different answers in the semiring case (which I definitely don't care about).

[Riccardo Brasca]

Yes, for Semiring not all equivalence relations that respect the operations come from ideals, I think @Damiano Testa know an example.

[Damiano Testa]

Maybe I am wrong, but if you take the "pre-cyclic" semiring where addition by 1 results in 0 --> 1 --> 2 --> 1 (loop), then the natural map from Nat to this semiring is not the quotient by an ideal.

[Damiano Testa]

(I guess that the relation in this case is "being at least 2 and congruent modulo 2". All algebraic failures are usually due to analysis messing things up, typically in the form of inequalities. :upside_down: )

[Eric Wieser]

Eric Wieser said:

(ah, this needs !3#18588, but that should be easy enough to send through mathport)

Done, #8313

[Eric Wieser]

Damiano Testa said:

Maybe I am wrong, but if you take the "pre-cyclic" semiring where addition by 1 results in 0 --> 1 --> 2 --> 1 (loop), then the natural map from Nat to this semiring is not the quotient by an ideal.

Well, docs#Ideal.instHasQuotientIdealToSemiringToCommSemiring doesn't even let you take a quotient by an ideal in a semiring, so I don't know if that claim is meaningful to lean!

[Eric Wieser]

The natural map is (maybe?) still a quotient by a RingCon

[Kevin Buzzard]

right, that's the point of a RingCon, surjections between semirings are precisely RingCons.

[Eric Wieser]

If we want to maximize bamboozling, arguably we should drop Ideals entirely and work only with RingCon!

[Antoine Chambert-Loir]

Even a type of two-sided ideals would be OK, I feel. For rings, they describe exactly the equivalence relations which are compatible with the ring structure, hence define all quotients. For semirings, this is more complicated, it is not even true that the equivalence class of 0 characterizes the equivalence relation.

[Eric Wieser]

Eric Wieser said:

Done, #8313

Hopefully should land soon, since it's already maintainer-merged

[Eric Wieser]

Eric Wieser said:

Note that I consider getting this notation working as much lower priority than making algebras imply right actions. There's no point having nice notation if we still can't use it for anything (without breaking other users)

I caved and the notation is now in #8909. I stand by algebras implying right actions being the next step though.

[Utensil Song]

2D6223CB-A04C-40A5-BFBA-2F25483FB09B.jpg

The last 2 notations are not displayed on iPhone.

[Eric Wieser]

Hence "has font issues"!