# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Submonoids under which mul_action.smul is closed

#### Eric Wieser (Nov 09 2020 at 11:50):

Does this exist? If not, what should it be called?

#### Kevin Buzzard (Nov 09 2020 at 12:19):

I guess if a group G is acting on a module, then a submodule which is G-stable is called a G-submodule.

#### Eric Wieser (Nov 09 2020 at 12:31):

Right, but in this case I don't have a module, only a `mul_action`

- my ~~objects don't have~~ carrier set is not closed under addition

#### Kevin Buzzard (Nov 09 2020 at 13:56):

My point is that, rather irritatingly, the name mathematicians give to this idea in a related situation involves using the actual name of the object which is acting :-/

#### Eric Wieser (Nov 09 2020 at 14:02):

Right, but "g-submodule" translates quite nicely to `submodule G`

- so I don't think that's a problem

#### Reid Barton (Nov 09 2020 at 14:13):

Doesn't `submodule G`

mean a submodule of G?

#### Kevin Buzzard (Nov 09 2020 at 14:16):

Right -- in the common situation that we have an R-module M with an action of a group G, then we would talk about submodules of M (any R-submodule) and also G-submodules of M (R-submodules fixed by G). A G-action on an R-module M makes M naturally into a module for the group ring R[G] so one could also talk about R[G]-submodules.

#### Eric Wieser (Nov 09 2020 at 14:19):

Ah, so you're talking about the case when we have both `mul_action G M`

and `mul_action R M`

?

#### Kevin Buzzard (Nov 09 2020 at 14:24):

To make it simpler we could have just an abelian group A (this would correspond to a Z-module). Then there's no R, and if G acts on A then we call A a G-module and we would talk about subgroups of A if they're not necessarily G-stable, and G-submodules if they are.

#### Eric Wieser (Nov 09 2020 at 14:32):

Right, so there are four cases over an `add_group A`

:

- not stable under G, not stable under addition:
`set A`

(has no interesting properties) - not stable under G, stable under addition:
`add_subgroup A`

- stable under G, stable under addition:
`submodule G A`

- stable under G, not stable under addition: ???

It's this last case I'm asking about

#### Reid Barton (Nov 09 2020 at 14:39):

why is the first word of the topic "submonoids" then?

#### Reid Barton (Nov 09 2020 at 14:40):

shouldn't it be "subsets"?

#### Eric Wieser (Nov 09 2020 at 14:40):

Because they're submonoids but not add_submonoids

#### Reid Barton (Nov 09 2020 at 14:40):

oh dear

#### Adam Topaz (Nov 09 2020 at 14:40):

It would be nice to have a good api around G-sets (sets with a G-action). I don't have a good name for what you want, except `subset G M`

as Reid suggests

#### Eric Wieser (Nov 09 2020 at 14:41):

I suspect the only thing @Kevin Buzzard will dislike more than `set G`

meaning "subset of G" is `subset G`

meaning something different...

#### Adam Topaz (Nov 09 2020 at 14:42):

I guess the question is what should we call `G-sets`

?

#### Adam Topaz (Nov 09 2020 at 14:42):

If we call it `G-foo`

then the correct answer is `subfoo G M`

.

#### Eric Wieser (Nov 09 2020 at 14:43):

As a concrete example of the type of thing I want to describe - I have a type `A`

satisfying `algebra ℤ A`

which is the multivariate polynomials over the variables `x y z`

with integer coefficients, and the obvious group action of integer multiplication. I want both of these things

- An object that describes the set of all monomials, which is closed under multiplication and the group action
`sub_mul_action_monoid ℤ A`

?

- An object that describes the set of all monomials of order n, which is closed under only the group action
`subset ℤ A`

?`sub_mul_action ℤ A`

?

#### Eric Wieser (Nov 09 2020 at 14:44):

Or is the correct answer `submul_action G M`

? `mul_subaction G M`

(for consistency with `add_submonoid`

not `subadd_monoid`

)?

#### Reid Barton (Nov 09 2020 at 14:45):

I don't understand any of your objects

#### Reid Barton (Nov 09 2020 at 14:45):

can you use $\LaTeX$?

#### Adam Topaz (Nov 09 2020 at 14:47):

what's the group action?

#### Eric Wieser (Nov 09 2020 at 14:47):

The one that we already have on the polynomials, multiplication by an integer

#### Adam Topaz (Nov 09 2020 at 14:47):

$(\mathbf{Z},\times)$ is not a group

#### Adam Topaz (Nov 09 2020 at 14:47):

(it's a monoid with 0)

#### Eric Wieser (Nov 09 2020 at 14:47):

Sorry, perhaps this isn't clear - I asked about a mul_action, not a group action

#### Eric Wieser (Nov 09 2020 at 14:48):

I think the word "group action" was put into my mouth by accident, and I cluelessly kept using it

#### Adam Topaz (Nov 09 2020 at 14:48):

Oh ok, so you just want the multiplicative action of the integers on the monomials in $\mathbf{Z}[X,Y,Z]$?

#### Eric Wieser (Nov 09 2020 at 14:48):

Yes

#### Reid Barton (Nov 09 2020 at 14:49):

it's just an additive subgroup in this case

#### Adam Topaz (Nov 09 2020 at 14:49):

And I guess by monomial you mean something of the form $n \cdot X^{a} \cdot Y^{b} \cdot Z^{c}$ where $n \in \mathbf{Z}$ and $a,b,c \in \mathbf{N}$.

#### Reid Barton (Nov 09 2020 at 14:49):

oh

#### Adam Topaz (Nov 09 2020 at 14:50):

What's the degree of $0$?

#### Adam Topaz (Nov 09 2020 at 14:50):

is it $-\infty$?

#### Eric Wieser (Nov 09 2020 at 14:50):

~~No, it's 0~~ - I don't really care what it is - I'm happy to put `0`

in any / all of my "order n" subsets

#### Eric Wieser (Nov 09 2020 at 14:51):

(Strictly I want the larger set that is $\prod_i(\alpha_{ix} X + \alpha_{iy} Y + \alpha_{iz} Z), \alpha_{i(\cdot)} \in \mathbb{Z}$, but your example is simpler and easier to describe)

#### Reid Barton (Nov 09 2020 at 14:51):

How about just a `submonoid`

?

#### Reid Barton (Nov 09 2020 at 14:52):

that maybe contains the integers or the nonzero integers or something

#### Eric Wieser (Nov 09 2020 at 14:52):

Sure, a submonoid is a start - but then I have to carry around a separate proof that the submonoid is closed under smul. I'm asking for a bundling of the submonoid with that proof.

#### Reid Barton (Nov 09 2020 at 14:53):

but `smul`

is just `mul`

by constants

#### Reid Barton (Nov 09 2020 at 14:53):

As I think you can tell we don't have a word for this

#### Reid Barton (Nov 09 2020 at 14:54):

I think the reason we're all confused here is that it's not common to think of a multiplicative monoid "acting" multiplicatively on another multiplicative monoid

#### Reid Barton (Nov 09 2020 at 14:55):

because a monoid acting on another monoid should satisfy a law $m(a+b) = ma + mb$

#### Reid Barton (Nov 09 2020 at 14:55):

but you instead have $m(ab) = (ma)b$

#### Adam Topaz (Nov 09 2020 at 14:56):

And a monoid has `1`

, so you have a map from the acting monoid to the acted-upon monoid by sending `m`

to `m \smul 1`

.

#### Reid Barton (Nov 09 2020 at 14:56):

right, so a submonoid which is stable under multiplication of the acting monoid is the same as one which contains the image of this map

#### Adam Topaz (Nov 09 2020 at 14:57):

It's even awkward to discuss these things :rofl:

#### Eric Wieser (Nov 09 2020 at 14:57):

because a monoid acting on another monoid should satisfy a law ...

Right, thats `distrib_mul_action`

, which is one level more specific than my question about `mul_action`

.

#### Reid Barton (Nov 09 2020 at 14:57):

I'm just saying this is what the math word "action" means

#### Eric Wieser (Nov 09 2020 at 14:58):

I think I should point out that my only exposure to most of these "math words" has been through lean

#### Eric Wieser (Nov 09 2020 at 14:58):

I will resist the temptation in future to use words that aren't `backticked`

when I'm not certain they match the real meaning :)

#### Reid Barton (Nov 09 2020 at 15:00):

so the situation here is that you have a monoid acting on a set (`mul_action`

), and the set is also a monoid, but the first monoid doesn't act on the second monoid

#### Reid Barton (Nov 09 2020 at 15:03):

(curiously, I have the same setup in my branch on Ore localization)

#### Adam Topaz (Nov 09 2020 at 15:03):

I'm confused...

#### Adam Topaz (Nov 09 2020 at 15:03):

The action of the integers on monomials is "compatible" with multiplication.

#### Reid Barton (Nov 09 2020 at 15:05):

Eric Wieser said:

I will resist the temptation in future to use words that aren't

`backticked`

when I'm not certain they match the real meaning :)

I wasn't trying to fault your usage and I think mathematicians will assume that words mean what they are used to regardless of your backtick-related efforts :upside_down:

I was just trying to explain how the confusion arose, and why Kevin started talking about group rings and stuff.

#### Reid Barton (Nov 09 2020 at 15:05):

Adam Topaz said:

The action of the integers on monomials is "compatible" with multiplication.

Compatible in some sense, but not the usual one (well not the one for an action anyways). Namely, $n \times \cdot$ isn't a monoid homomorphism

#### Eric Wieser (Nov 09 2020 at 15:06):

In this particular case I think I made the confusion worse by assuming that the math words and lean words were the same. No offence taken.

#### Eric Wieser (Nov 09 2020 at 15:14):

Stating the problem purely in lean, we current have definitions that give the following

```
import algebra.algebra.subalgebra
variables (A R : Type*)
example [add_monoid A] (S : add_submonoid A) :
add_monoid S := infer_instance
example [semiring A] (S : subsemiring A) :
semiring S := infer_instance
example [comm_semiring R] [add_comm_monoid A] [semimodule R A] (S : submodule R A) :
add_comm_monoid S × semimodule R S := (infer_instance, infer_instance)
example [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
add_comm_monoid S × algebra R S := (infer_instance, infer_instance)
```

But not any objects `subTODO`

that allow us to define

```
example [monoid R] [mul_action R A] (S : subTODO R A) :
mul_action R S := sorry
example [monoid R] [add_monoid A] [distrib_mul_action R A] (S : subTODO R A) :
add_monoid S × distrib_mul_action R S := sorry
```

or the confusing case that I was asking about here

```
example [monoid R] [mul_action R A] [monoid A] (S : subTODO R A) :
monoid S × mul_action R S := sorry
```

#### Reid Barton (Nov 09 2020 at 16:07):

The awkward thing is that the word "action" doesn't refer to the thing being acted on but the action itself

#### Reid Barton (Nov 09 2020 at 16:07):

but, I guess we could use `sub_mul_action`

anyways

#### Eric Wieser (Nov 09 2020 at 16:12):

That seems like the simplest naming rule

#### Eric Wieser (Nov 13 2020 at 15:14):

PR at #4996

#### Eric Wieser (Nov 19 2020 at 16:45):

There's some bikeshedding going on about naming in the PR, which might be worth deciding on here.

#### Lars Ericson (Nov 20 2020 at 04:21):

I just learned a new word.

Last updated: May 07 2021 at 18:19 UTC