Zulip Chat Archive

Stream: Is there code for X?

Topic: Submonoids under which mul_action.smul is closed


view this post on Zulip Eric Wieser (Nov 09 2020 at 11:50):

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

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

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

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:13):

Doesn't submodule G mean a submodule of G?

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

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

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:39):

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:40):

shouldn't it be "subsets"?

view this post on Zulip Eric Wieser (Nov 09 2020 at 14:40):

Because they're submonoids but not add_submonoids

view this post on Zulip Reid Barton (Nov 09 2020 at 14:40):

oh dear

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

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:42):

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:42):

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

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:45):

I don't understand any of your objects

view this post on Zulip Reid Barton (Nov 09 2020 at 14:45):

can you use LaTeX\LaTeX?

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:47):

what's the group action?

view this post on Zulip Eric Wieser (Nov 09 2020 at 14:47):

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:47):

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:47):

(it's a monoid with 0)

view this post on Zulip Eric Wieser (Nov 09 2020 at 14:47):

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

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:48):

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

view this post on Zulip Eric Wieser (Nov 09 2020 at 14:48):

Yes

view this post on Zulip Reid Barton (Nov 09 2020 at 14:49):

it's just an additive subgroup in this case

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:49):

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:49):

oh

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:50):

What's the degree of 00?

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:50):

is it -\infty?

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

view this post on Zulip Eric Wieser (Nov 09 2020 at 14:51):

(Strictly I want the larger set that is i(αixX+αiyY+αizZ),αi()Z\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)

view this post on Zulip Reid Barton (Nov 09 2020 at 14:51):

How about just a submonoid?

view this post on Zulip Reid Barton (Nov 09 2020 at 14:52):

that maybe contains the integers or the nonzero integers or something

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:53):

but smul is just mul by constants

view this post on Zulip Reid Barton (Nov 09 2020 at 14:53):

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:55):

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:55):

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

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

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 14:57):

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 14:57):

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

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

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 15:03):

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

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:03):

I'm confused...

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:03):

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

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

view this post on Zulip 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×n \times \cdot isn't a monoid homomorphism

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

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

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

view this post on Zulip Reid Barton (Nov 09 2020 at 16:07):

but, I guess we could use sub_mul_action anyways

view this post on Zulip Eric Wieser (Nov 09 2020 at 16:12):

That seems like the simplest naming rule

view this post on Zulip Eric Wieser (Nov 13 2020 at 15:14):

PR at #4996

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

view this post on Zulip Lars Ericson (Nov 20 2020 at 04:21):

I just learned a new word.


Last updated: May 07 2021 at 18:19 UTC