## 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: ???

#### 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

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]$?

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}$.

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 mto 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)

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):

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 [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


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

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