overloading \bu

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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]

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

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

[from mathlib]

[Floris van Doorn]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Floris van Doorn]

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]

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]

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]

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

[Floris van Doorn]

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]

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