Coset definition?

Stream: Is there code for X?

[Edison Xie]

I noticed that we have definition for cosets, but do we have definitions and APIs about two-sided cosets like aRb for a, b in R? Btw this is for the criterion for morita equivalence between R and S iff exist n : ℕ and a full idempotent e in R such that S ≃+* eMₙ(R)e.

[Andrew Yang]

#20531

[Yaël Dillies]

You can write the double coset aRb as a •> R <• b using open scoped RightActions

[Edison Xie]

thanks and also do we have definitions for full idempotent, i.e ReR =R?

[Junyan Xu]

"Coset" would not quite make sense in a semiring. ReR=R could be phrased as the TwoSidedIdeal generated by e is \top. (But I think TwoSidedIdeal should not be defined to be RingCon, but rather Ideal+IsTwoSided to accommodate semirings.) Eventually I'd like to generalize materials on Morita equivalence to semirings following this paper.

[Edison Xie]

Ok thanks! Do you wanna make PRs about other idempotents?

[Junyan Xu]

What are the "other idempotents"?
I'm not actively working on Morita equivalence at the moment. For the semiring version I'd at least need to introduce SemimoduleCat that takes an AddCommMonoid instead of AddCommGroup. And I'd need to generalize materials around AddCon, finite presentation and flatness to be able to work comfortably with (semi)modules over semirings. I do have plans to revive my PR on tensor products over noncommutative semirings, because that offers an important viewpoint towards Morita equivalence.
More on dobule cosets: they are called docs#Doset.doset in mathlib, but they are of the form HaK, not of the form aHb, and they are only defined when you have a (multiplicative) group (in which case you have a decomposition of the whole group into disjoint double cosets). I should say it's the lack of multiplicative inverse, rather than additive inverse, that is the reason why the Doset API isn't appropriate here (certainly not for aRb, but also not for ReR). However aRb is also used in the definition of a prime ideal over noncommutative (semi)rings, so it would be appropriate to define it as a AddSubmonoid/group.

[Edison Xie]

Screenshot 2025-01-19 at 08.12.40.png
Other idempotents like this page shows?

[Kevin Buzzard]

Edison you mean "predicates on idempotents" not "other idempotents". Junyan why do you care so much about advanced algebra over semirings? Is there an application you have in mind?

[Junyan Xu]

The paper Facets of module theory over semirings talks about an algebraic number theory application on page 5. It also develops the theory of faithfully flat descent
and shows results like GL_n isn't flat over Nat. Of course the tropical school is also major enterprise.

I think proofs that generalize are more "correct" and are what mathlib should epitomize, especially if they are not much more difficult. That said, it's not my intention to block anyone from developing the theory only for Rings, especially given that many infrastructure for Semirings are not there. But keeping the generalization in mind would help you choose proofs that generalize most easily.

In the context of Morita equivalence, It's interesting to think whether certain properties of modules are categorical; it turns out many still are over a semiring. I was unsure for some days about projectivity (which is defined to mean lifting property w.r.t. surjective linear maps, not all epimorphisms, since w.r.t. non-surjective linear maps like the inclusion Nat -> Int, even free modules do not satisfy the lifting property), but then the paper on Morita equivalence points out that surjections agree with regular epimorphisms (which I guess is common knowledge since I recall seeing it before after being reminded by the paper). Finite presentation is characterized by Hom(M,-) preserving all directed colimits, and finite generation is characterized by preserving directed colimits of monomorphisms (=injective linear maps). It's still true that finitely presented flat modules are projective, and finitely generated projective modules are finitely presented, but they may not be Zariski-locally free over a comm. semiring. The current definition docs#Module.FinitePresentation is unfortunately wrong over a semiring for the purpose of these statements.