Taking quotient ring in non-commutative cases

Stream: mathlib4

[Wang Jingting]

I was trying to formalize the concept of symmetric algebra, which is basically the tensor algebra taking quotient by relations of the form $x \otimes y - y \otimes x$. So I came across this problem about, how should I take the quotient when the ring I started with is non-commutative.

There seems to be several approaches of doing this, either by using RingQuot or taking the quotient by a TwoSidedIdeal (but the HasQuotient instance seems to be missing until now). So I thought it would probably be better to come to zulip and ask for some advice from the more experienced ones. In which way should I formalize this (which presumably is more convenient when adding instances)? And when should I prefer RingQuot over the other way if provided the method of taking a quotient by a TwoSidedIdeal?

In addition, I'm also curious about how we should formalize taking quotients by TwoSidedIdeals. A few questions came up when I was discussing this with a friend of mine, such as, is it possible to make this DefEq to taking quotient by an Ideal in the commutative case, or even DefEq to taking RingQuot? Some ideas we came up with is:

1. Simply taking RingQuot of the RingCon inside the TwoSidedIdeal
   (which is not DefEq to anything, and isomorphisms would be used to do the conversions)

2. Defining it to be taking the quotient of a relation analogous of how quotients of ideals are defined, something like

import Mathlib

instance {R : Type*} [Ring R] : HasQuotient R (TwoSidedIdeal R) where
  quotient' I := Quotient (I.ringCon.toSetoid)

which makes it DefEq for R / I.toTwoSided and R / I for an ideal I in the case of commutative rings, and for a two-sided ideal J, R / J.asIdeal is propositionally equal to R / J.

3. Refactoring the definition of ideals so that the data of that RingCon is contained in the structure, and things would be DefEq in a rather simple way (but seems like a lot of work)

Which would you prefer among these ideas? Or probably you can suggest another better one?

P.S. I'm also curious about why RingQuot has been defined as a structure wrapped around some Quot, does anyone have some ideas on that?

Thanks in advance! I would really appreciate your help!

[Adam Topaz]

docs#RingQuot I think?

[Adam Topaz]

Yes, I personally think that the api aroud RingQuot is quite pleasant to use.

[Wang Jingting]

Adam Topaz said:

docs#RingQuot I think?

Sure that makes sense, but since we already have TwoSidedIdeal, probably taking quotient by that would be a better way? RingQuot seems to be designed in a way that's not DefEq to any other thing, so I'm curious about why had it been designed like this. (which the docs didn't say about?)

[Adam Topaz]

In general we use wrappers (such as one for RingQuot) to add a layer of separation between the "original" object and the new object being defined. With this approach there can be no confusion between types of Quot ... and types of RingQuot ..., but if we did def RingQuot ... := Quot ... there could be such a confusion.

[Adam Topaz]

I'm not sure why you have a two sided ideal. You could define an inductive relation for the symmetric algebra as

inductive SymmRel : R -> R -> Prop
  | mk (x y) : SymmRel (x * y) (y * x)

(untested) and use that in RingQuot.

[Wang Jingting]

Adam Topaz said:

In general we use wrappers (such as one for RingQuot) to add a layer of separation between the "original" object and the new object being defined. With this approach there can be no confusion between types of Quot ... and types of RingQuot ..., but if we did def RingQuot ... := Quot ... there could be such a confusion.

Yeah, I agree with that, but it occurred to me that when formalizing things on a type-theoretical basis, making things DefEq would often make life easier? Like, why wouldn't we wany this to be DefEq to something when taking quotient by an ideal (in the commutative case)?

[Junyan Xu]

Let me point to another approach at #17930 introducing a typeclass Ideal.IsTwoSided to generalize existing materials on CommRing quotient to the setting of Ring + IsTwoSided (and therefore the defeq with AddCommGroup/Module quotient is kept). The new typeclass and generalizations caused some slowdown, and even though I reduced the slowdown to 0.217/0.201%, I temporarily ran out of ideas to further reduce it. I think the new class is pretty reasonable since docs#Ideal.IsPrime and docs#Ideal.IsMaximal are already classes.

[Wang Jingting]

Adam Topaz said:

I'm not sure why you have a two sided ideal. You could define an inductive relation for the symmetric algebra as

inductive SymmRel : R -> R -> Prop
  | mk (x y) : SymmRel (x * y) (y * x)

(untested) and use that in RingQuot.

We were thinking the exact same thing when we started! We actually wrote a definition like this and already proved some properties, and this question came up when I was trying to give it a gradedAlgebra structure and start thinking about probably we should talk about taking quotients of homogeneous two-sided ideals more generally. So then I began to look at things about TwoSidedIdeals and I was really surprised to find that we're still unable to take quotients by them. (this makes another part of the background story)

[Junyan Xu]

Yeah mathlib has been pretty commutative-algebra focused, and I think the lack of more two-sided ideal support is a major roadblocker against the development of more noncommutative theory.

[Wang Jingting]

Junyan Xu said:

Let me point to another approach at #17930 introducing a typeclass Ideal.IsTwoSided to generalize existing materials on CommRing quotient to the setting of Ring + IsTwoSided (and therefore the defeq with AddCommGroup/Module quotient is kept). The new typeclass and generalizations caused some slowdown, and even though I reduced the slowdown to 0.217/0.201%, I temporarily ran out of ideas to further reduce it. I think the new class is pretty reasonable since docs#Ideal.IsPrime and docs#Ideal.IsMaximal are already classes.

I see your point on that, it seems reasonable to me, but since we already have a class called TwoSidedIdeal in mathlib, wouldn't developing them both in parallel cause some confusions? Or perhaps your idea is that we only take quotient by ideals, and the quotient is a ring only in the case we have [I.isTwoSided] on it?

[Junyan Xu]

Or perhaps your idea is that we only take quotient by ideals, and the quotient is a ring only in the case we have [I.isTwoSided] on it?

Yeah that's exactly the case.
More discussions at #PR reviews > #17908 Hopkins–Levitzki theorem @ 💬

[Junyan Xu]

Ideal is a special case (reducibly defeq) of Submodule, and there's already a HasQuotient instance for Submodules docs#Submodule.hasQuotient.

[Junyan Xu]

This is where I detail the reason why I'm not taking quotients by TwoSidedIdeals: #mathlib4 > two-sided ideals @ 💬

[Wang Jingting]

Junyan Xu said:

Or perhaps your idea is that we only take quotient by ideals, and the quotient is a ring only in the case we have [I.isTwoSided] on it?

Yeah that's exactly the case.
More discussions at #PR reviews > #17908 Hopkins–Levitzki theorem @ 💬

Thanks a lot! That seems to be a helpful related discussion. I'd say that's a reasonable idea (which seems a bit more natural then the current approach), but probably they're expecting something more on the performance? Anyway, thanks again!