Ideal and RingQuot

Stream: mathlib4

[Robert Maxton]

So, I'm running into a bit of an issue regarding outstanding technical debt in Mathlib's handling of Ideals...

• Ideal itself is defined in a very general way, with only sufficient structure and assumptions to represent left ideals of semirings.
• However, most of the actual API interfacing with Ideal assumes not only Ring but in fact CommRing.
• RingQuot permits noncommutative semirings, but implicitly builds two-sidedness into its definition.
• As such, all existing methods of making ring quotients are less general than the original definition of Ideal, as well as the the level at which TensorProduct, PiTensorProduct, and now FreeProduct, among others, are written.
• Worse, they're less general in different directions, there is no simple 'inclusion' hierarchy here.

[Robert Maxton]

I had originally thought proving the equivalence between FreeProduct and PiTensorProduct in the case of commutative (semi)rings would be easy, but in fact it has been quite difficult in part for this reason. I'm not entirely sure where I should go from here as a result.

[Kevin Buzzard]

See also https://github.com/orgs/leanprover-community/projects/11 . This is all basically my fault; I wanted to get started on commutative algebra in 2017 when there were literally 0 people in the Lean community interested in noncommutative ring theory (there were only about 40 people in the Lean community in total, and most of them were computer scientists), so we just developed a bunch of theory for commutative rings (in order to define schemes) and then others built on that.

[Robert Maxton]

ooof.

[Jireh Loreaux]

Note: we are currently in a period of transition regarding ideals in non-commutative rings. We have docs#TwoSidedIdeal now, but the API is still under development.

[Robert Maxton]

Speaking as a physicist who is mostly interested in noncommutative operator algebras, that's very unfortunate for me personally :p.

[Ruben Van de Velde]

Well, look at it from the bright side

[Ruben Van de Velde]

Now there's a cool project for you to work on!

[Jireh Loreaux]

Fear not Robert Maxton , I'm a C⋆-algebraist, and there are a few people working hard to fix this and other issues. Note that we now have the docs#ContinuousFunctionalCalculus, and we're making good progress in many directions.

[Kevin Buzzard]

For RingQuot if you want to quotient out by a left ideal you could just quotient out by the corresponding additive subgroup, the quotient won't be a ring if the ideal isn't a 2-sided ideal, right? The quotient is probably even an R-module I would imagine.

[Robert Maxton]

@Jireh Loreaux Oh good!

[Jireh Loreaux]

That being said, we'd definitely love your help, if you're willing to get involved!

[Kevin Buzzard]

In fact I'm a bit confused about what you're talking about above, if you quotient out a ring by an ideal which isn't two-sided then you don't get a quotient ring, so all existing methods of making ring quotients won't apply mathematically because they'll give you rings.

[Jireh Loreaux]

Kevin, I think Robert's point is that we don't currently have anyway to build a Ring instance on the quotient of a (non-commutative) ring by a two-sided ideal, but of course that's something we're working on now.

[Kevin Buzzard]

Oh ok, but this is on the way! I would imagine that the people working on Brauer groups have this already and are slowly porting it over.

[Kevin Buzzard]

Yeah, two-sided ideals are quite new.

[Robert Maxton]

@Kevin Buzzard so actually I'm writing up my List of Approaches

• I could ignore the problem, write a third competing quotient structure at the appropriate level of generality, and use that to provide the proof and the isomorphism theorems. This seems obviously Bad, as it increases the technical debt further while kicking the problem down the road.
• I could simply restrict my concern to two sided ideals. For actual Rings, this is fine, but for Semirings this is very not fine; while losing subtraction introduces other conditions on what counts as a subobject beyond "ideal", two-sidedness falls away, so I'd end up writing a fairly unnatural API.
• I could try and refactor RingQuot so that it produces left ideals. I think RingQuot.lean itself would be fairly easy to refactor in this way, but I have no idea how widely RingQuot is used in Mathlib, so this might turn into a particularly dramatic bit of yak shaving.
• I could focus on Rings to the exclusion of Semirings entirely. This seems somewhat reasonable, though there are a number of useful applications of Semirings even already, but seems like it could very much end up turning into approach 1, i.e. adding technical debt to Mathlib and departing even further from the path of "correct level of generality".

[Jireh Loreaux]

Hmm... now it seems my assessment above of your desires may have been incorrect?
Robert Maxton said:

• I could focus on Rings to the exclusion of Semirings entirely.

As far as ideals go, I would advocate for this. Despite the fact that useful Semirings exist, I'm not so sure how useful their ideal structure (or worse: quotients) actually ends up begin.

[Robert Maxton]

I mean, there's the thing I actually want to work on in the end, which is probably going to involve quite a lot of category theory/Grothendieck sieves and noncommutative algebra and would benefit from both
but as the specific thing I would like to work on is self-admittedly pretty specific, I would prefer to do things in a way that would be generally useful to Mathlib rather than leaving a trail of overly-narrow libraries built in a straight line between me and my actual project :p

[Kevin Buzzard]

If R is a (non-commutative) ring then to give a surjection R -> A of rings up to isomorphism is to give its kernel, which is a two-sided ideal. But in the semiring case there are more quotients than there are two-sided ideals, e.g. there's an obvious surjection from the naturals to the semiring {0,1,2,3} with a+b and a*b defined to be the right answer if it's < 3, and 3 otherwise (i.e. 3="overflow") and this map has trivial kernel in the sense that only 0 gets mapped to 0. So two-sided ideals don't tell the full story of quotients in the semiring case. In the presence of negation this phenomenon doesn't happen.

[Jireh Loreaux]

Robert, sure, and that's appreciated. But in this case, if all you (personally) care about is quotients of non-commutative Rings (or NonUnitalRings) by TwoSidedIdeals, then that's already an appropriate level of generality, and hopefully we'll have all that working soon.

[Kevin Buzzard]

In particular I don't understand what you mean by "I could try and refactor RingQuot so that it produces left ideals". I am still confused about what you actually want at this point, I see your list of approaches but I don't know what you're approaching yet. Can you write some concrete Lean code indicating something which you want which isn't there yet?

[Jireh Loreaux]

If you're interested in contributing things though, we can definitely coordinate to find something useful!

[Robert Maxton]

Kevin Buzzard said:

So two-sided ideals don't tell the full story of quotients in the semiring case. In the presence of negation this phenomenon doesn't happen.

Yeah, I ended up having to go track down a textbook on Semirings and it seems it boils down to "being a kernel is not sufficient, you need to be a kernel of a particularly 'nice') (Golan calls them 'tame') semiring hom
A category theorist would probably say something like "SRing has 'fewer' epis than Ring, so the natural choice of quotient and subobject for a given arrow is similarly unfamiliar"

[Robert Maxton]

Kevin Buzzard said:

In particular I don't understand what you mean by "I could try and refactor RingQuot so that it produces left ideals". I am still confused about what you actually want at this point, I see your list of approaches but I don't know what you're approaching yet. Can you write some concrete Lean code indicating something which you want which isn't there yet?

Specifically, I recently contributed docs#LinearAlgebra.FreeProduct , and one of the TODOs left is to show that when dealing with commutative (semi)rings the free product reduces to PiTensorProduct

[Robert Maxton]

And since FreeProduct and PiTensorProduct are both written for Semirings I would kinda prefer to write the equivalence for Semirings as well, but doing so without a robust quotient API has turned out to be a pain in its own right

[Robert Maxton]

(The issue is that PiTensorProduct doesn't actually have its universal property implemented, which I would rather like to fix as well -- PiTensorProduct will let you lift a MultilinearMap to the tensor product, but it won't work from an indexed family of LinearMaps, never mind an indexed family of AlgHoms)

[Robert Maxton]

(Which, to be fair, it's not actually the categorical coproduct/neither of those lifts even exist except in the presence of a CommRing R instance, but)

[Eric Wieser]

Where do left-ideals feature in writing down this equivalence?

[Robert Maxton]

Good question. I have in fact gotten pretty far afield in my yak-shaving, huh.

[Kevin Buzzard]

Just looking at PR #14858 now. One answer to the question "why is lift slow" is "you use aesop twice and non-squeezed simps twice". You get a 30% speedup by changing all of them to the relevant simp only calls. But it's still annoyingly slow even after those changes.

[Robert Maxton]

Basically, whether my approach is to first construct the relevant universal-coproduct API and then prove the equivalence or just build a special case into my proof, either way I'll probably want to reduce things down to DirectSum, which is the "previous" coproduct in the hierarchy and the last one that has a proper coproduct-lift defined. (It has a few features for the DirectSum of Rings and Algebras, but they're all written assuming a graded structure that doesn't apply in general).

[Robert Maxton]

(As a side note, I should really remove the "same as FreeAlgebra from the TODOs, it's not actually true because FreeProduct imposes some extra substructure on the sum type.)

[Robert Maxton]

Unfortunately, by definition DirectSum involves finitely supported functions, and PiTensorProduct does not have such a requirement. While any given element of the tensor product is still a sum of finitely many terms, each term is an infinite product over potentially a proper class, and to be honest my math chops aren't quite up to figuring out how to handle that directly yet :v.

The easiest method of glossing over the various issues with infinities is probably to stick to a categorical approach all the way through, focusing on families of arrows and functional properties without getting bogged down into the details of what the terms are doing. (Nothing in PiTensorProduct is computable anyway lol.) As such, my current approach is to attempt to prove

RingHom.ker (algebraMap R (⨂[R] i, A i)) = ⨆ i, RingHom.ker (algebraMap R (A i))

which I believe directly implies that PiTensorProduct is indeed the categorical coproduct once you assume commutativity

[Kevin Buzzard]

Robert Maxton said:

(As a side note, I should really remove the "same as FreeAlgebra from the TODOs, it's not actually true because FreeProduct imposes some extra substructure on the sum type.)

That would be a nice short easily-reviewable PR.

[Robert Maxton]

Sure. And while I'm at it, should I fix the aesops or do that in a separate PR?

[Robert Maxton]

which I believe directly implies that PiTensorProduct is indeed the categorical coproduct once you assume commutativity

Which lets me write

def liftAlgHom' [DecidableEq ι] [∀ {i} (a : A i), Decidable (a ≠ 0)] {S : Type*} [CommSemiring S] [Algebra R S]:
  (⦃i : ι⦄ → A i →ₐ[R] S) ≃ ((⨂[R] i, A i) →ₐ[R] S) where ...

[Robert Maxton]

Once I have that it's easy, because FreeProduct already has its lift defined, so I can just lift the identity going both ways and call it a day. (Which is basically just the Lean-formalized version of "categorical coproducts are unique up to isomorphism" anyway)

[Eric Wieser]

Robert Maxton said:

(Nothing in PiTensorProduct is computable anyway lol.)

I think this is just because the Lean compiler is silly and sends itself on a wild goose chase (which does eventually conclude). For now we don't actually care about the computation, so we told it not to waste that time.

[Eric Wieser]

I would guess the right approach here is just to build the appropriate universal properties in each direction, and then the isomorphism will follow without much work

[Robert Maxton]

Well, yes. The issue is making the universal property for PiTensorProduct.

... Though, now that I think about it, my problem was in part "ugh all the Ideal and ker stuff is written for commutative rings", but actually I'm in a commutative setting right now... Oh, but it also assumes actual Rings and not just Semirings, so I'd still be narrowing from my original PR if I used most of it.

[Kevin Buzzard]

OK so my understanding of your issue is the following: you would like to write down an R-algebra isomorphism between LinearAlgebra.FreeProduct R A and PiTensorProduct R A. If they are isomorphic then I'm a bit confused about why we want LinearAlgebra.FreeProduct at all, given that we have a semiring structure on PiTensorProduct R A if A is taking values in semirings, and we also have the R-algebra structure in docs#PiTensorProduct.instAlgebra . What is the maths proof that they're isomorphic? And if they are isomorphic, why did you want to make FreeProduct at all?

[Robert Maxton]

They are isomorphic in the presence of [CommRing R]; they are distinct if R is not commutative

[Robert Maxton]

I made FreeProduct as step one in filling in CategoryTheory/Ring/FilteredColimits.lean and CategoryTheory/Algebra/FilteredColimits.lean, neither of which actually exist yet and whose absence I came across while trying to use Lean to help teach myself category theory

[Kevin Buzzard]

I don't understand -- both FreeProduct and PiTensorProduct require commutativity of R so "they are distinct if R is not commutative" seems like a meaningless statement. I am still confused about a precise statement of something you want which we don't currently have, and also confused about why FreeProduct exists at all.

[Robert Maxton]

.... Sorry, I got my letters mixed up. They are distinct if the A i are not commutative, not R!

[Kevin Buzzard]

Furthermore, neither of the files you mention above seem to exist.

[Kevin Buzzard]

Aah OK so perhaps I finally understand something: you want to prove

import Mathlib.LinearAlgebra.FreeProduct.Basic

variable {I : Type*} [DecidableEq I] {i : I}
  (R : Type*) [CommSemiring R]
  (A : I → Type*) [∀ i, CommSemiring (A i)] [∀ i, Algebra R (A i)]

example : LinearAlgebra.FreeProduct R A ≃ₗ[R] PiTensorProduct R A := sorry

?

[Robert Maxton]

And yeah, I mentioned that :p. I don't even remember what I was trying to study at the time, but I noticed that we didn't have a proof that RingCat and AlgebraCat are cocomplete or even have all filtered colimits, so I decided to fill in that gap. The relevant proofs are relatively straightforward and even close to boilerplate, as the exact same technique works for reducing all the way down to from AlgebraCat, through ModuleCat, down to Type

[Robert Maxton]

Kevin Buzzard said:

Aah OK so perhaps I finally understand something: you want to prove

import Mathlib.LinearAlgebra.FreeProduct.Basic

variable {I : Type*} [DecidableEq I] {i : I}
  (R : Type*) [CommSemiring R]
  (A : I → Type*) [∀ i, CommSemiring (A i)] [∀ i, Algebra R (A i)]

example : LinearAlgebra.FreeProduct R A ≃ₗ[R] PiTensorProduct R A := sorry

?

Yes, at least that's my immediate goal for now!

[Kevin Buzzard]

I find it much easier to understand if people state what they're trying to do in Lean, rather than in words.

[Kevin Buzzard]

Yes, at least that's my immediate goal for now!

And what's the maths proof? And what's the problem stopping you from solving this goal in Lean?

[Robert Maxton]

The maths proof is that FreeProduct R A is the universal coproduct in $R$-Alg unconditionally, and PiTensorProduct is the universal coproduct in $R$-CAlg or however you want to refer to the category-of-commutative-$R$-algebras, and universal objects are unique up to isomorphism, QED

[Kevin Buzzard]

I don't follow that proof. The universal properties are different in the two categories.

[Robert Maxton]

Sure, but $R$-CAlg is a full subcategory of $R$-Alg, so FreeProduct R A can validly lift arrows in $R$-CAlg

[Kevin Buzzard]

I don't even see why FreeProduct R A is commutative if all the A i are.

[Kevin Buzzard]

Surely the free product of $\R[x]$ and $\R[y]$ over $\R$ is a polynomial ring in two non-commuting variables, and the PiTensorProduct is a polynomial ring in two commuting variables?

[Robert Maxton]

No, because the tensor product itself is only commutative up to isomorphism; matrices aren't equal to their transposes

[Robert Maxton]

But yes, the underlying structure (especially as implemented in Lean) is pretty different, so I think working through the nuts and bolts of what the isomorphism is doing to each element would be correspondingly difficult.

[Kevin Buzzard]

I need to go now but I'm still very confused. I don't know what matrices have to do with anything.

[Kevin Buzzard]

Are you claiming that the free product of the one-variable polynomial rings $\R[x]$ and $\R[y]$ over $\R$ is commutative?

[Robert Maxton]

Kevin Buzzard said:

I need to go now but I'm still very confused. I don't know what matrices have to do with anything.

Just an example. Every entry in a matrix represents a component of the form a ⨂ b, and trying to commute the tensor product would send every such entry to b ⨂ a, i.e. transposing the matrix; but matrices aren't equal to their transposes even though taking the transpose is an isomorphism, so the tensor product isn't commutative, so PiTensorProduct is a polynomial ring in two noncommuting variables, I believe.

[Kevin Buzzard]

So what do you make of docs#PiTensorProduct.instCommRing ?

[Kevin Buzzard]

You claimed above that PiTensorProduct is the universal coproduct in the category of commutative R-algebras and hence surely it is a commutative R-algebra?

[Robert Maxton]

The polynomial ring as a whole has quite a lot of symmetry built into its operations, so multiplication is commutative
So we have ∀ (a b : A₁ ⨂ A₂), a * b = b * a, even though "under the hood", each of those elements are written as sums of noncommuting products

[Robert Maxton]

Basically, I'm arguing that "PiTensorProduct is a commutative algebra built out of fundamentally noncommutative components, so it shouldn't surprise us that FreeProduct R A can be the same."

[Robert Maxton]

Which is not a proof, the actual proof is the categorical argument I outlined earlier

[Robert Maxton]

here, actually...

[Robert Maxton]

Mm, my current Mathlib environment isn't in a convenient place for this, so this is just psuedocode, but

def LinearAlgebra.FreeProduct R A ≃ₐ[R] PiTensorProduct R A :=
  ⟨ lift (AlgEquiv.refl R (PiTensorProduct R A)),
    PiTensorProduct.liftAlgHom' (AlgEquiv.refl R (FreeProduct R A)),
    by sorry, by sorry⟩

[Robert Maxton]

Something like this is probably going to be the full proof when I'm done

[Robert Maxton]

And the fundmantal issue is that PiTensorProduct.liftAlgHom' doesn't exist yet

[Jireh Loreaux]

you can always just use the live environment temporarily. Just click the button in the top right of the code block you just wrote.

[Robert Maxton]

Good thought. Here, it "works" other than the missing function

import Mathlib.LinearAlgebra.FreeProduct.Basic
import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.RingTheory.PiTensorProduct
import Mathlib.Algebra.Algebra.Equiv

open LinearAlgebra FreeProduct PiTensorProduct TensorProduct

variable {I : Type u_1} [DecidableEq I] {R : Type u_3} {A : I → Type u_4}
         [CommRing R] [(i : I) → CommRing (A i)] [(i : I) → Algebra R (A i)]

def equivPiTensorProduct : FreeProduct R A ≃ₐ[R] (⨂[R] i, A i)  :=
  ⟨ FreeProduct.lift R A (fun {i} ↦ PiTensorProduct.singleAlgHom i),
    PiTensorProduct.liftAlgHom' (fun {i} ↦ FreeProduct.ι R A i),
    by sorry, by sorry⟩

[Robert Maxton]

Basically, once you have two objects that can both validly lift the same morphisms in a way that makes all diagrams commute, then you can just lift each others' canonical injections

[Robert Maxton]

At which point you have your isomorphism

[Robert Maxton]

Which is the Lean version of "universal objects are unique"

[Eric Wieser]

You'd do better to go via docs#AlgEquiv.ofAlgHom, because then ext can take you home for the sorries

[Robert Maxton]

Ah, yes, that's what I meant to use rather than the anonymous constructor. Thanks though.

[Eric Wieser]

You might find a couple ext lemmas are missing too: you can usually recover them from an Injective lemma about the universal property (if you didn't end up proving them first)

[Kevin Buzzard]

So how are you dealing with my claim that the free product of $\R[x]$ and $\R[y]$ is not commutative, but the tensor product is, and hence they can't be isomorphic?

[Kevin Buzzard]

In my current mental model, the free product is the vector space with basis $1,x,y,xx,xy,yx,yy,xxx,xxy,xyx,xyy,yxx,...$ and the tensor product is the vector space with basis $1,x,y,xx,xy,yy,xxx,xxy,xyy,yyy,xxxx,...$.

[Kevin Buzzard]

My current mental model is that your abstract categorical argument doesn't work because the free product is not even an object of the category of commutative R-algebras, so the universal property of the tensor product in that category tells you nothing about the free product (because it can't be applied to the free product).

[Robert Maxton]

Mm.

[Robert Maxton]

I think you're right.

[Robert Maxton]

I thought I had a diagrammatic argument, but upon reflection all it actually demonstrates is that there's some nice subobject inside the free product that has a hom from the tensor product

[Robert Maxton]

Which we already knew, it's the subring of polynomials symmetric under permutation of terms of the same degrees in each component algebra

[Antoine Chambert-Loir]

Could you summary your plan? There's an obvious definition of the equivalence relations that give rise to quotient (semi) rings (just be compatible with + and *) and then you just take the quotient type, which will be a semiring. For rings, these equivalence relations are described by two sided ideals.

[Antoine Chambert-Loir]

I believe it is easy to get this generality, except that one needs a nice API to access the standard quotients (by twosided ideals for rings, resp ideals fir commutative rings).

[Eric Wieser]

Antoine Chambert-Loir said:

There's an obvious definition of the equivalence relations that give rise to quotient (semi) rings (just be compatible with + and *) and then you just take the quotient type, which will be a semiring.

This is precisely docs#RingCon and docs#RingCon.Quotient

[Antoine Chambert-Loir]

A model for this already exists in Mathlib for algebras.

[Eric Wieser]

RingQuot predates RingCon, and the port got in the way before I could finish merging them

[Antoine Chambert-Loir]

Robert Maxton said:

Which we already knew, it's the subring of polynomials symmetric under permutation of terms of the same degrees in each component algebra

If I understand things correctly, that subring is not isomorphic to the polynomial ring except for Q-algebras.

[Antoine Chambert-Loir]

Eric Wieser said:

RingQuot predates RingCon, and the port got in the way before I could finish merging them

By the way, one also needs a notion of ‘ModuleCon‘.

[Eric Wieser]

I claim that's the wrong approach, since you often want a congruence relation that respects multiple modules simultaneously

[Eric Wieser]

At least, it's the wrong approach if you want to work with quotients. If you want to work with the lattice structure then I agree.

[Eric Wieser]

I believe #8658 solves the quotient case, but it's been a while

[Antoine Chambert-Loir]

Am I right in understanding that the the issue is the one that you suggest here?
"that wouldn't work because a single congruence relation can inherit multiple simultaneous actions"

https://github.com/leanprover-community/mathlib4/pull/8658#issuecomment-1862974245

[Antoine Chambert-Loir]

Then a solution could be similar to what's done for localization. One needs some construction of quotient types that work for some action, and one could add a property that it inherits the required SMul actions (if they pass to the quotient), or that it is universal for these.

[Robert Maxton]

Antoine Chambert-Loir said:

Could you summary your plan? There's an obvious definition of the equivalence relations that give rise to quotient (semi) rings (just be compatible with + and *) and then you just take the quotient type, which will be a semiring. For rings, these equivalence relations are described by two sided ideals.

Mm... I see, essentially the problem is that only subtractive ideals correspond to a relation with transitivity, but if you focus on an equivalence relation from the beginning the problem is moot. I think partitioning ideals are mooted similarly?

In that case, I might just use @Eric Wieser 's nice docs#RingCon.Quotient. My goal is just to get the isomorphism theorems for rings and semirings; then I'll use those to provide a liftAlgHom for PiTensorProduct as a coproduct in CRing /$R$-CAlg. The isomorphism isn't actually true so obviously I'll stop there.

[Robert Maxton]

Antoine Chambert-Loir said:

If I understand things correctly, that subring is not isomorphic to the polynomial ring except for Q-algebras.

Well, I've been wrong once this thread already :p, but I think this one works? Basically, as @Kevin Buzzard said, the tensor product of two algebras $A, B$ can be described by sums of terms of the form $r \prod_i^n \prod_j^m a_i b_j$ for $r \in R$, $\forall i < n, a_i \in A$ and $\forall j <m, b_j \in B$. Meanwhile the free product can be described by sums of words with letters ranging over all $A, B$ and again coefficients in $r$.

So, suppose you look at an element $x$ of the free product, and you see that for every term $r a_0 b_0 a_1 a_2 b_1 ...$, if you permute the entries however you like, the resulting term is also present in $x$ with the same coefficient $r$. I claim that the set of such elements form a subring and that the resulting subring is isomorphic with the tensor product.