# Zulip Chat Archive

## 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