Zulip Chat Archive
Stream: general
Topic: What is the purpose of `group_action` and `module`
Johan Commelin (Mar 23 2019 at 15:38):
There are certain classes which are defined to be exactly some other class, with the only difference that they make more assumptions on the carrier types. Examples: a group_action is exactly a monoid_action where the acting monoid is a group; a module is exactly a semimodule where the scalar semiring is a ring.
What is the purpose of such classes. Do they only exist for reasons of terminology, or are there also other benefits?
Chris Hughes (Mar 23 2019 at 16:04):
I did it like that because somebody complained about not having vector_space, and I thought they might complain about this as well.
Johan Commelin (Mar 23 2019 at 17:41):
I understand. But maybe it does complicate the type class graph. Leading to more complicated instance searches, etc... So we might also just have a class called action.
Johan Commelin (Mar 23 2019 at 18:05):
@Johannes Hölzl @Sebastian Ullrich What do you think? Are these issues, or is this irrelevant?
Johan Commelin (Mar 23 2019 at 18:05):
Creating the extra class does mean restating lots of lemmas etc...
Kevin Buzzard (Mar 23 2019 at 18:54):
What if an undergraduate asks "where are vector spaces?" and you reply "oh, just use modules" and they say "what is a module"?
Johan Commelin (Mar 23 2019 at 18:57):
What if an undergrad uses vector spaces, and he has to prove 0 \in V, and you say, oh that's module.zero_mem.
Johan Commelin (Mar 23 2019 at 18:57):
Or whatever...
Johan Commelin (Mar 23 2019 at 18:57):
The hierarchy is leaking through everywhere. I don't think we can really avoid that.
Kevin Buzzard (Mar 23 2019 at 18:58):
We can't just define vector_space.zero_mem? What's the problem with this approach?
Johan Commelin (Mar 23 2019 at 18:58):
That it is a duplication of effort, and harder to maintain
Johan Commelin (Mar 23 2019 at 18:58):
Because it will go out of sync
Kevin Buzzard (Mar 23 2019 at 18:59):
Maybe a tactic?
Johan Commelin (Mar 23 2019 at 18:59):
Maybe...
Johan Commelin (Mar 23 2019 at 19:00):
Anyway, I'm fine with making an exception for vector_space for pedagogical reasons. Note that I didn't mention vector_space in my first post. I purposefully chose group_action and module.
Kevin Buzzard (Mar 23 2019 at 19:02):
Modules are different to vector spaces, I think it's inevitable that one should expect submodule.zero_mem and subspace.zero_mem and subring.zero_mem and subgroup.zero_mem and all sorts of other zero_mems
Johan Commelin (Mar 23 2019 at 19:25):
I don't how often I've written apply is_add_subgroup.add_mem. Lean still doesn't know what I mean...
Kevin Buzzard (Mar 23 2019 at 19:26):
you could fix it ;-)
Johan Commelin (Mar 23 2019 at 19:29):
I don't know if it should be fixed...
Chris Hughes (Mar 24 2019 at 14:20):
I'd be very happy to get rid of group actions. I'd also be happy to rename the is_monoid_action theorems to whatever they're called for vector spaces, one_smul or whatever. module should probably extend monoid_action, or at least there should be an instance saying every module is a monoid action.
Kevin Buzzard (Mar 24 2019 at 14:29):
In group cohomology one has groups acting on abelian groups (with group law +). The definition is that the group acts on the underlying type by morphisms which preserve addition. This definition extends to monoid actions on abelian groups (although I don't think I've ever seen it being used for monoids which are not either groups or rings).
Johan Commelin (Mar 25 2019 at 05:34):
@Chris Hughes I suggest merging the current PR first, and then changing those names etc... in a follow-up PR.
Johan Commelin (Mar 25 2019 at 05:35):
That keeps the PR's nice and small
Johan Commelin (Mar 25 2019 at 07:31):
@Johannes Hölzl @Mario Carneiro @Sebastian Ullrich Are there CS reasons for having these type classes? Do they help type class search, or do they hamper it?
Sebastian Ullrich (Mar 25 2019 at 08:28):
The usual downside of such trivial classes is that implicit coercion only works in one direction: If you have an is_monoid_action on a group, it's not automatically an is_group_action. You have to explicitly declare an instance for that. That may not be an issue, but if it is, is_group_action could be defined as an abbreviation (i.e. reducible) so that type class search treats it as equivalent to is_monoid_action.
Sebastian Ullrich (Mar 25 2019 at 08:28):
I don't see any upsides other than terminology
Johan Commelin (Mar 25 2019 at 08:33):
Ok, I could imagine that you would shortcut some type class searches this way...
Johan Commelin (Mar 25 2019 at 08:33):
But I think that the downside you mention is enough reason to do away with this class.
Johan Commelin (Mar 26 2019 at 08:31):
Should we also generalise is_ring_hom to only assume semiring instances? (I would vote for not changing the name... even if it is not exactly accurate.)
Johan Commelin (Mar 26 2019 at 11:53):
Nevermind... the difference is of course that you need to make map_zero explicit for semirings
Last updated: Dec 20 2023 at 11:08 UTC