Ideals for semigroups/monoids

Stream: Is there code for X?

[Xavier Xarles]

Is it defined already?
https://ncatlab.org/nlab/show/ideal+in+a+monoid
Do you find it interesting to be in there? It could be defined with the sub_mul_action structure, and it has many applications in semi-groups and monoids.

[Yaël Dillies]

Those are all questions for @Eric Wieser

[Jireh Loreaux]

No, I'm fairly certain we don't have that (EDIT: for semigroups). However, there is a planned project (whenever I or someone else gets around to it) to define two-sided ideals (for even non-unital rings). Not sure off the top of my head whether or not these should be merged.

[Yaël Dillies]

This seems pretty separate though. A monoid ideal need not be closed under addition (in fact, there may well be no ambient addition!)

[Eric Wieser]

Isn't a monoid ideal just SubMulAction M M?

[Eric Wieser]

(or SubMulAction (MulOpposite M) M for the right- monoid ideal)

[Eric Wieser]

I don't think we have anything beyond that

[Jireh Loreaux]

Sorry, I meant for semigroups we don't. The answer is basically that we don't have any actions of non-unital (i.e., without identity) types on other types.

[Eric Wieser]

docs#SubMulAction works for semigroups, because it only assumes SMul not MulAction

[Jireh Loreaux]

Ah, is that a recent change? (nevermind, I can blame). Answer: apparently not.