Submonoids under which mul_action.smul is closed

Stream: Is there code for X?

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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]

Right, but "g-submodule" translates quite nicely to submodule G - so I don't think that's a problem

[Reid Barton]

Doesn't submodule G mean a submodule of G?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

shouldn't it be "subsets"?

[Eric Wieser]

Because they're submonoids but not add_submonoids

[Reid Barton]

oh dear

[Adam Topaz]

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]

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]

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

[Adam Topaz]

If we call it G-foo then the correct answer is subfoo G M.

[Eric Wieser]

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]

Or is the correct answer submul_action G M? mul_subaction G M (for consistency with add_submonoid not subadd_monoid)?

[Reid Barton]

I don't understand any of your objects

[Reid Barton]

can you use $\LaTeX$?

[Adam Topaz]

what's the group action?

[Eric Wieser]

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

[Adam Topaz]

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

[Adam Topaz]

(it's a monoid with 0)

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Yes

[Reid Barton]

it's just an additive subgroup in this case

[Adam Topaz]

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]

oh

[Adam Topaz]

What's the degree of $0$?

[Adam Topaz]

is it $-\infty$?

[Eric Wieser]

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]

(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]

How about just a submonoid?

[Reid Barton]

that maybe contains the integers or the nonzero integers or something

[Eric Wieser]

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]

but smul is just mul by constants

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Adam Topaz]

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]

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]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Adam Topaz]

I'm confused...

[Adam Topaz]

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

[Reid Barton]

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]

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]

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]

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]

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

[Reid Barton]

but, I guess we could use sub_mul_action anyways

[Eric Wieser]

That seems like the simplest naming rule

[Eric Wieser]

PR at #4996

[Eric Wieser]

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

[Lars Ericson]

I just learned a new word.