Zulip Chat Archive
Stream: Is there code for X?
Topic: kernel of a semiring action
Michail Karatarakis (Oct 14 2022 at 12:07):
Hi, do we have the "kernel of an action" ?
Kevin Buzzard (Oct 14 2022 at 12:14):
(of a monoid on a type, presumably?)
Michail Karatarakis (Oct 14 2022 at 12:24):
Yes, that's right
Yaël Dillies (Oct 14 2022 at 12:24):
Surely of a monoid on a semiring, rather?
Michail Karatarakis (Oct 14 2022 at 12:25):
Sure, is there anything like that?
Michail Karatarakis (Oct 14 2022 at 12:28):
Currently, I have a semiring action of a group on a field and I want the kernel of that action.
Eric Rodriguez (Oct 14 2022 at 12:38):
what's your definition of the kernel of the action?
Eric Rodriguez (Oct 14 2022 at 12:38):
a member of the monoid that stabilises the whole type?
Michail Karatarakis (Oct 14 2022 at 12:41):
I want the set of all group elements which act as the identity
Michail Karatarakis (Oct 14 2022 at 12:42):
So not just a member
Eric Wieser (Oct 14 2022 at 13:26):
I think that will be (mul_semiring_action.to_ring_aut G R).ker once your PR goes through
Michail Karatarakis (Oct 14 2022 at 23:10):
Nice, thanks a lot
Eric Wieser (Oct 15 2022 at 12:43):
Although actually, I think you want docs#mul_action.stabilizer
Kevin Buzzard (Oct 15 2022 at 12:45):
No I don't think so -- that's the things which fix one element. Michail wants the Inf of all of these.
Eric Wieser (Oct 15 2022 at 12:54):
Aha, then it's (mul_action.to_perm_hom G R).ker (docs#mul_action.to_perm_hom) which doesn't need #16857 or R to be a ring
Eric Wieser (Oct 15 2022 at 12:54):
(but is propositionally equal to my suggestion above)
Michail Karatarakis (Oct 15 2022 at 14:41):
Yes, (mul_action.to_perm_hom G R).ker seems to work. Thank you
Last updated: Dec 20 2023 at 11:08 UTC