Stream: Is there code for X?

Topic: G-module maps

Kevin Buzzard (Mar 06 2021 at 19:02):

We have G-modules (which seem to be called distrib_mul_action) and G-submodules (sub_mul_action) but do we have morphisms of G-modules?

import group_theory.group_action.defs

structure G_module_map (G A B : Type*) [monoid G]
[distrib_mul_action G A] [distrib_mul_action G B] :=
(to_fun : A →+ B)
(map_smul (g : G) (a : A) : to_fun (g • a) = g • to_fun a)


If not, then can someone recommend a wacky name for it (experience seems to indicate that G_module_map isn't going to fly -- how about distrib_mul_action_hom?) and also wacky notation (→+ᵍ?) (Or is someone going to tell me that we should not have this structure at all? My instinct is that I need it for this week's lecture. Edit: actually we don't seem to have submodules -- sub_mul_action isn't preserved under +. So sub_distrib_mul_action? :-/

Johan Commelin (Mar 06 2021 at 19:06):

@Kenny Lau did you do those?

Kevin Buzzard (Mar 06 2021 at 19:26):

Should to_fun really be called to_add_monoid_hom? Or should I have A -> B and is_add_monoid_hom to_fun? Does it matter?

Johan Commelin (Mar 06 2021 at 19:30):

Don't you want to extends A →+ B?

Kevin Buzzard (Mar 06 2021 at 19:46):

I dunno, I'm no good at definitions. That's why I want someone else to have done it :-) If you say so!

Kevin Buzzard (Mar 06 2021 at 19:46):

All this stuff about structure projections and type class inference issues goes straight over my head.

Eric Wieser (Mar 06 2021 at 19:47):

Am I missing something? Isn't that just linear_map with weaker assumptions?

Eric Wieser (Mar 06 2021 at 19:47):

And if so, can we just weaken the assumptions on what we already have?

Eric Wieser (Mar 06 2021 at 19:48):

(c.f. monoid_hom, which also works as a group hom)

Kevin Buzzard (Mar 06 2021 at 19:49):

I don't have a clue if I'm supposed to be doing this

instance : has_coe_to_fun (distrib_mul_action_hom G A B) :=
{ F := _,


or making a coercion to add_monoid_hom or what.

Kevin Buzzard (Mar 06 2021 at 19:50):

Eric there's no ring. Aah, but there is mul_action_hom.

Eric Wieser (Mar 06 2021 at 19:50):

Why do you need a ring?

Eric Wieser (Mar 06 2021 at 19:50):

The actual fields of your proposed structure are identical to those of linear_map

Eric Wieser (Mar 06 2021 at 19:51):

So just remove the assumptions from src#linear_map that are overly strict!

Aah I found it!

Kevin Buzzard (Mar 06 2021 at 19:52):

It was indeed called distrib_mul_action_hom, I need to import algebra.group_action_hom even though this has nothing to do with algebras.

Eric Wieser (Mar 06 2021 at 19:52):

How bad an idea is changing linear_map to this?

structure linear_map (R : Type u) (M : Type v) (M₂ : Type w) [monoid R] [add_monoid M] [add_monoid M₂] [distrib_mul_action R M] [distrib_mul_action R M₂] extends add_hom M M₂, M →[R] M₂


Kevin Buzzard (Mar 06 2021 at 19:54):

That was silly of me, I have never used this stuff before and I searched mathlib without having the name. Once I realised they should be called distrib_mul_action_hom I should have searched again. Thanks #Is there code for X? for making me organise my thoughts!

Kevin Buzzard (Mar 06 2021 at 19:56):

I guess I'm still looking for G-stable subgroups but they're less important.

Eric Wieser (Mar 06 2021 at 20:03):

I guess extends sub_mul_action, add_subgroup is the best you can get right now

Last updated: May 07 2021 at 20:11 UTC