Zulip Chat Archive

Stream: Is there code for X?

Topic: saturated submonoids, kernels and beyond


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 31 2021 at 10:17):

why a coercion? That seems likely to loop

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 31 2021 at 10:25):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 31 2021 at 10:29):

Is substractive a typo of subtractive?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Eric Wieser (Jan 31 2021 at 11:03):

It looks like you made the same typo again!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Jan 31 2021 at 11:18):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 31 2021 at 11:23):

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

view this post on Zulip 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!
;-)

view this post on Zulip Damiano Testa (Jan 31 2021 at 11:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 31 2021 at 11:42):

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

view this post on Zulip Mario Carneiro (Jan 31 2021 at 11:47):

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

view this post on Zulip 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"

view this post on Zulip 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