saturated submonoids, kernels and beyond

Stream: Is there code for X?

[Xavier Xarles]

A natural notion that there exists for monoids (or any time do you have an binary operation) are the subobjects that can appear as "kernels" (in the "tradicional" sense) of maps f preserving the operation: so comaps f ⊥. There is however a caracterization without using maps and so on. The definition for monoids can be something like

import group_theory.submonoid.operations

structure saturated_submonoid (M : Type*) [monoid M] extends submonoid M :=
(saturate_left {a b}:  a ∈ carrier → a * b ∈ carrier → b ∈ carrier)
(saturate_right {a b}:  b ∈ carrier → a * b ∈ carrier → a ∈ carrier)

Does it exists already in lean?
This notion is important in the theory of ideals in comm_semirings, and in general for semimodules over semirings.

[Eric Wieser]

I don't thing this exists today. Presumably if it did exist there would be a coercion from subgroup to saturated_submonoid by using mul_mem on a * b and inv b

[Mario Carneiro]

why a coercion? That seems likely to loop

[Xavier Xarles]

In case you have inverse, like for groups, all subobjects are saturated.
Do you think it is interesting if I try to do some code on this? How about the name? Some call it "substractive" instead of saturated, at least in semiring theory, but I am not sure if it has a name in monoid theory, as I am not an expert.

[Eric Wieser]

I don't see why it would loop, but I guess a .to_whatever projection is fine too - whatever we already do for conversion from subgroups to submonoids

[Eric Wieser]

Presumably you'd want a version of this for submodules too?

[Eric Wieser]

And 2 versions for subsemirings (saturation of addition and multiplication), and one for subring (saturation of multiplication)

[Mario Carneiro]

"cancellative" also comes to mind, because it's sort of analogous to being closed under subtraction/division

[Eric Wieser]

Is substractive a typo of subtractive?

[Xavier Xarles]

Eric Wieser said:

Is substractive a typo of subtractive?

Yeap, sorry. Substractive. A version for submodules also. And for add_monoids, etc.

[Xavier Xarles]

@Mario Carneiro I think "cancelative" is a bad name, because cancelative_monoid denotes some special monoids, where one can cancels like for integral domains for commutative rings: ab=ac implies b=c (if the monoid has a zero, then one asks for a not to be zero, of course).

[Eric Wieser]

It looks like you made the same typo again!

[Eric Wieser]

But yes, we already have docs#cancel_monoid and docs#cancel_monoid_with_zero, which use a slightly different meaning of cancel to what Mario is proposing.

[Kevin Buzzard]

Soustraire. Patrick also occasionally talks about substraction. It's a bit like how positif != positive. Being bilingual must be hard work!

[Eric Wieser]

I was wondering where that misspelling originated - maybe it's the english who are wrong!

[Eric Wieser]

Regarding "saturated", the wikipedia definition seems stronger and does not regard {1, 4, 4^2, ...} as saturated as it does not contain 2 or its closure - whereas your definition does.

[Patrick Massot]

Yes, I'm definitely in favor of reforming that subtraction spelling into substraction!

[Damiano Testa]

As far as I can tell, the Latin root is "sub", so the English version is closer to the original. In French, the word "sub" became "sous" giving rise to soustraire. So my hunch would be to either have the "b" or the "s", but not both!
;-)

[Damiano Testa]

In Italian, the "bt" merged into a double "t", producing sottrarre.

[Mario Carneiro]

Xavier Xarles said:

Mario Carneiro I think "cancelative" is a bad name, because cancelative_monoid denotes some special monoids, where one can cancels like for integral domains for commutative rings: a*b=a*c implies b=c (if the monoid has a zero, then one asks for a not to be zero, of course).

Yes, we already have that definition. I think this is in much the same spirit as your submonoid definition, hence cancellative_submonoid

[Mario Carneiro]

I think the only other possible meaning for such a term would be something like a * b \in S -> b \in S without the assumption on a, which gets into the difference between an ideal and a subring

[Eric Wieser]

What do you call a submodule where r smul m in S -> m in S?

[Mario Carneiro]

I don't know. "downward closed" (in the divisibility order)?

[Kevin Buzzard]

PS @Xavier Xarles my answer to your question of whether it is interesting to write some code on this is "definitely -- and it should be on a branch of mathlib rather than an independent project"

[Xavier Xarles]

I must say that the condition I wrote is the one that appears as "kernels of congruences" only for commutative monoids. For non-commutative ones needs more conditions, like for subgroups one needs the "normal subgroup condition".