## Stream: new members

### Topic: notation for a family of mul_actions

#### Chris Birkbeck (Sep 15 2021 at 15:41):

For each integer k I've defined a mul_action of some group G on some set S (with G and S indep. of k). Now I wanted to use some notation for this like the usual smul notation • but perhaps something like •ₖ. Is this possible? I tried playing around with infixr's but it didnt like the dependence on k.

#### Yaël Dillies (Sep 15 2021 at 15:48):

Small ₖ and k aren't related at all as unicode characters, so you won't be able to do that. What you can do is not making it small.

#### Yaël Dillies (Sep 15 2021 at 15:49):

To avoid any confusion, I would advise •[k]

#### Eric Wieser (Sep 15 2021 at 15:49):

One option would be to use a type alias:

abbreviation with_k (k) (G) [group G] := G

instance : mul_action (with_k k G) S := ...


#### Eric Wieser (Sep 15 2021 at 15:50):

Can you give a precise definition of what you want has_scalar to mean for your action?

#### Chris Birkbeck (Sep 15 2021 at 15:51):

Yaël Dillies said:

Small ₖ and k aren't related at all as unicode characters, so you won't be able to do that. What you can do is no making it small.

Ah interesting I didnt know this!

#### Chris Birkbeck (Sep 15 2021 at 15:58):

Eric Wieser said:

Can you give a precise definition of what you want has_scalar to mean for your action?

So I wanted the notation, for each k to behave just the the usual smul notation. I dont think I want some has_scalar to be ℤ → G → S → S. Is that what you are asking? Sorry, maybe I'm misunderstanding your question.

#### Eric Wieser (Sep 15 2021 at 16:00):

I'm asking for you to give an example of the kind of action you have in mind; that is, fill in the blanks in:

-- I assume you meant S was a Type not a set
def my_smul {G : Type*} [group G] {S : Type*} (k : ℤ) (g : G) (s : S) : S := sorry


#### Eric Wieser (Sep 15 2021 at 16:01):

The reason I ask is you might be able to express the k-indexed family of actions in terms of stuff we already have

#### Chris Birkbeck (Sep 15 2021 at 16:11):

Ah sorry I see what you mean. The thing I have is something like

variables (G : Type*) (α  : Type*) (β : Type*) [group G] [mul_action G α] [mul_action G β]

def my_smul (k : ℤ) : G → (α → β) → (α → β):=
λ g f, (λ (x : α), g^k • f (g⁻¹ • x)    )


(also technically I'd like this to behave like a right action, but it seems most of the things are for left actions, so I'm using inverses to make it a left action).

#### Eric Wieser (Sep 15 2021 at 16:16):

Hmm, I guess I can only reuse one existing action there:

variables (G α β : Type*) [group G] [mul_action G α] [mul_action G β]

def my_smul (k : ℤ) (g : G) (f : α → β) : (α → β) := g^k • λ x, f (g⁻¹ • x)


#### Eric Wieser (Sep 15 2021 at 16:17):

I would probably still recommend the type alias approach that I suggested with with_k above, and then maybe add some special notation for that

#### Eric Wieser (Sep 15 2021 at 16:17):

Which is roughly how I recommended doing right actions

#### Chris Birkbeck (Sep 15 2021 at 16:20):

So, let me see if I understand how this works. With the type alias, I'm storing the information of G and k both under the name G? and when I want to change the k in some specific instance I use the with_k parameter?

#### Eric Wieser (Sep 15 2021 at 16:25):

Something like this:

variables {G α β : Type*} [group G] [mul_action G α] [mul_action G β]

@[derive group]
def with_k  (k : ℤ) (G : Type*) [group G] := G

def with_k.mk (k : ℤ) : G →* with_k k G := monoid_hom.id _
def with_k.out {k : ℤ} : with_k k G →* G := monoid_hom.id _

instance with_k.has_scalar (k : ℤ) : has_scalar (with_k k G) (α → β) :=
{ smul := λ g f, g.out ^ k • λ x, f (g.out⁻¹ • x) }

local notation g •ₖ[:73 k:0 ] f:72 := with_k.mk k g • f

-- I panicked, unit.star is the only group I could think of
#check unit.star •ₖ[2] id


#### Eric Wieser (Sep 15 2021 at 16:25):

You're storing the k in a copy of the type G

#### Chris Birkbeck (Sep 15 2021 at 16:28):

Ah I see that looks like it'll work as I want it to. Thank you!

#### Eric Wieser (Sep 15 2021 at 16:29):

Your other option is not to make it an action at all, and just make it a mul_equiv

#### Chris Birkbeck (Sep 15 2021 at 16:33):

Ah interesting, I hadn't thought about that. I'll have a think about which will work best. Thanks.

#### Eric Wieser (Sep 15 2021 at 16:36):

Your action isn't actually a mul_equiv unless comm_group G, right?

#### Johan Commelin (Sep 15 2021 at 16:36):

I'm a bit worried that the with_k will create a new barrier that many things cannot see through.

#### Eric Wieser (Sep 15 2021 at 16:37):

Yes, it might become as arduous as having all the instances for docs#opposite is

#### Johan Commelin (Sep 15 2021 at 16:37):

Wouldn't it be better to just make •[k] a local notation for λ g f, g ^ k • λ x, f (g⁻¹ • x)?

#### Johan Commelin (Sep 15 2021 at 16:37):

@Chris Birkbeck this is for modular forms, isn't it?

#### Eric Wieser (Sep 15 2021 at 16:37):

If you do that you can't use any existing smul lemmas

#### Chris Birkbeck (Sep 15 2021 at 16:38):

Eric Wieser said:

Your action isn't actually a mul_equiv unless comm_group G, right?

maybe, I just made this up quickly as an example.

#### Johan Commelin (Sep 15 2021 at 16:38):

Eric Wieser said:

If you do that you can't use any existing smul lemmas

can they not see through the notation?

#### Yaël Dillies (Sep 15 2021 at 16:38):

You can have both, so that the type synonym with_k gets only used when needed for smul lemmas.

#### Eric Wieser (Sep 15 2021 at 16:38):

Well they won't apply to the action as a whole

#### Chris Birkbeck (Sep 15 2021 at 16:38):

Johan Commelin said:

Chris Birkbeck this is for modular forms, isn't it?

Yeah its for the ∣ₖ action on modular forms

#### Yaël Dillies (Sep 15 2021 at 16:39):

What about defining has_ssmul.ssmul := (ssmul : α → β → γ → δ)? :upside_down:

#### Johan Commelin (Sep 15 2021 at 16:40):

I think we'll need a bunch of API lemmas anyway. The question is whether the def with_k will be a net help.

#### Eric Wieser (Sep 15 2021 at 16:41):

If it's not a net help, I'd recommend going with a mul_equiv instead.

#### Johan Commelin (Sep 15 2021 at 16:41):

Probably defining a new notation, and proving a bunch of lemmas for it is easier.

#### Eric Wieser (Sep 15 2021 at 16:41):

Something like docs#mul_action.to_perm_hom

#### Johan Commelin (Sep 15 2021 at 16:41):

Yael's suggestion might also work

#### Yaël Dillies (Sep 15 2021 at 16:42):

Yaël Dillies said:

You can have both, so that the type synonym with_k gets only used when needed for smul lemmas.

This one, you mean?

#### Johan Commelin (Sep 15 2021 at 16:43):

Yaël Dillies said:

What about defining has_ssmul.ssmul := (ssmul : α → β → γ → δ)? :upside_down:

No, I was thinking of this one... :oops:

#### Chris Birkbeck (Sep 15 2021 at 16:43):

Johan Commelin said:

Probably defining a new notation, and proving a bunch of lemmas for it is easier.

This is what I was originally going to do. I just thought it would maybe be good to make it link the existing mul_action framework. But perhaps this is the best thing to do.

#### Chris Birkbeck (Sep 15 2021 at 16:45):

Yaël Dillies said:

What about defining has_ssmul.ssmul := (ssmul : α → β → γ → δ)? :upside_down:

where does it end though? how long until we have has_sssssssssssmul?? :stuck_out_tongue:

#### Johan Commelin (Sep 15 2021 at 16:45):

The group in your application will not be commutative, right?

Oh

#### Chris Birkbeck (Sep 15 2021 at 16:46):

Johan Commelin said:

The group in your application will not be commutative, right?

Yeah its some matrix group.

#### Yaël Dillies (Sep 15 2021 at 16:46):

I'll stop joking because one day you'll actually implement my stupid ideas :grinning:

#### Johan Commelin (Sep 15 2021 at 16:46):

That's not a good reason not to joke (-;

#### Reid Barton (Sep 15 2021 at 16:53):

Eric Wieser said:

One option would be to use a type alias:

abbreviation with_k (k) (G) [group G] := G

instance : mul_action (with_k k G) S := ...


In this case (modular forms) it might be mathematically natural to do it the other way, i.e., make separate copies of S for each k (= sections of some $\omega^{\otimes k}$).

Last updated: Dec 20 2023 at 11:08 UTC