## Stream: Is there code for X?

### Topic: saturated submonoids, kernels and beyond

#### Xavier Xarles (Jan 31 2021 at 10:04):

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 (Jan 31 2021 at 10:16):

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 (Jan 31 2021 at 10:17):

why a coercion? That seems likely to loop

#### Xavier Xarles (Jan 31 2021 at 10:23):

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 (Jan 31 2021 at 10:25):

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 (Jan 31 2021 at 10:25):

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

#### Eric Wieser (Jan 31 2021 at 10:27):

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

#### Mario Carneiro (Jan 31 2021 at 10:28):

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

#### Eric Wieser (Jan 31 2021 at 10:29):

Is substractive a typo of subtractive?

#### Xavier Xarles (Jan 31 2021 at 10:56):

Eric Wieser said:

Is substractive a typo of subtractive?

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

#### Xavier Xarles (Jan 31 2021 at 11:00):

@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 (Jan 31 2021 at 11:03):

It looks like you made the same typo again!

#### Eric Wieser (Jan 31 2021 at 11:05):

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 (Jan 31 2021 at 11:14):

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

#### Eric Wieser (Jan 31 2021 at 11:18):

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

#### Eric Wieser (Jan 31 2021 at 11:23):

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 (Jan 31 2021 at 11:23):

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

#### Damiano Testa (Jan 31 2021 at 11:26):

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 (Jan 31 2021 at 11:27):

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

#### Mario Carneiro (Jan 31 2021 at 11:28):

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 (Jan 31 2021 at 11:30):

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 (Jan 31 2021 at 11:42):

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

#### Mario Carneiro (Jan 31 2021 at 11:47):

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

#### Kevin Buzzard (Jan 31 2021 at 13:08):

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 (Jan 31 2021 at 17:51):

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".

Last updated: May 19 2021 at 02:10 UTC