## Stream: maths

### Topic: overloading \bu

#### Kevin Buzzard (Nov 29 2019 at 16:46):

A student of mine @Shenyang Wu has a G-module M, so an abelian group with a left action of a group G, with notation \bub or \bu, the blob thing. He also wants to have the usual action of int on M. Can he use \bub for this too?

We just had a torrid time getting add_gsmul to work, until I realised that now one has to put open_locale add_group. Is this what I'm supposed to be doing? The bub notation in algebra.group_power is "localized notation".

#### Floris van Doorn (Nov 29 2019 at 16:51):

It should work out of the box:

import algebra.module

variables {G : Type*} {M : Type*} [ring G] [add_comm_group M] [module G M]

example (g : G) (m : M) : g • m = g • m := rfl
example (n : ℤ) (m : M) : n • m = n • m := rfl


#### Floris van Doorn (Nov 29 2019 at 16:52):

I think all of the add_gsmul/localized notation is to bootstrap our way before we have declared the actual module instance? Not sure though.

#### Kevin Buzzard (Nov 29 2019 at 16:54):

import algebra.group_power

import algebra.module

theorem blah (A : Type*) [add_comm_group A] (a : A) (i j : ℤ) :
(i + j) • a = i • a + j • a :=
begin
rw add_gsmul, -- rewrite fails
end


Why does this fail though?

#### Kevin Buzzard (Nov 29 2019 at 16:55):

#check add_gsmul
-- add_gsmul : ∀ (a : ?M_1) (i j : ℤ), gsmul (i + j) a = gsmul i a + gsmul j a


It's defined using localised notation which doesn't make it out of the file

#### Kevin Buzzard (Nov 29 2019 at 16:55):

theorem add_gsmul : ∀ (a : β) (i j : ℤ), (i + j) • a = i • a + j • a :=
@gpow_add (multiplicative β) _


[from mathlib]

#### Floris van Doorn (Nov 29 2019 at 16:57):

They're not syntactically equal, but only definitionally equal. • is defined to be gsmul, but not syntactically the same as it. There should be a corresponding theorem in algebra.module though (probably called add_smul.

#### Kevin Buzzard (Nov 29 2019 at 16:57):

so here I can fix this with open_locale add_group. Is this what I'm supposed to be doing?

#### Kevin Buzzard (Nov 29 2019 at 16:58):

If I don't do this open_locale thing then add_gsmul is unusable (unless I constantly unfold the notation)

#### Kevin Buzzard (Nov 29 2019 at 16:58):

I just don't know if I'm asking too much here.

#### Floris van Doorn (Nov 29 2019 at 16:58):

import algebra.module

theorem blah (A : Type*) [add_comm_group A] (a : A) (i j : ℤ) :
(i + j) • a = i • a + j • a :=
begin
rw add_smul,
end


#### Kevin Buzzard (Nov 29 2019 at 16:59):

OK we'll press on with add_smul but I might be back here whining when the roof falls in. Thanks Floris.

#### Floris van Doorn (Nov 29 2019 at 17:00):

So if you do open_locale, the notation • is hijacked to mean gsmul instead of its usual definition (has_smul.smul). This is probably not a good idea, not in the least because you also want to write g • m with g : G.

#### Floris van Doorn (Nov 29 2019 at 17:00):

All theorems about gsmul should have a corresponding theorem about smul in algebra.module. Hopefully...

#### Floris van Doorn (Nov 29 2019 at 17:03):

well, that is not true... You might eventually want to use a lemma that i • a = gsmul i a (by rfl).
Perhaps algebra.group_power should be refactored: we want to use the operation • and not gsmul as much as possible.

#### Floris van Doorn (Nov 29 2019 at 17:06):

One other option you have is to open_locale smul. Then •ℤ will be the notation for gsmul, which means you can rewrite with all the gsmul-lemmas. It will be annoying though, since you might accidentally type • instead of •ℤ which will type-check, but might lead to errors down the road.

import algebra.module

variables {G : Type*} {M : Type*} [ring G] [add_comm_group M] [module G M]

open_locale smul
example (g : G) (m : M) : g • m = g • m := rfl
example (n : ℤ) (m : M) : n •ℤ m = n •ℤ m := rfl


Last updated: May 11 2021 at 16:22 UTC