G-module maps

Stream: Is there code for X?

[Kevin Buzzard]

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]
  [add_comm_monoid A] [add_comm_monoid B]
  [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]

@Kenny Lau did you do those?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

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 := _,
  coe := add_monoid_hom.to_fun ∘ to_add_monoid_hom }

or making a coercion to add_monoid_hom or what.

[Kevin Buzzard]

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

[Eric Wieser]

Why do you need a ring?

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

Aah I found it!

[Kevin Buzzard]

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]

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]

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]

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

[Eric Wieser]

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