Zulip Chat Archive

Stream: maths

Topic: overloading \bu


view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 16:58):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Nov 29 2019 at 17:00):

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

view this post on Zulip 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.

view this post on Zulip 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