notation for a family of mul_actions

Stream: new members

[Chris Birkbeck]

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]

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]

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

[Eric Wieser]

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]

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

[Chris Birkbeck]

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]

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]

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]

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]

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]

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]

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]

Which is roughly how I recommended doing right actions

[Chris Birkbeck]

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]

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]

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

[Chris Birkbeck]

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

[Eric Wieser]

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

[Chris Birkbeck]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Chris Birkbeck]

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]

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]

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

[Eric Wieser]

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

[Chris Birkbeck]

Johan Commelin said:

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

Yeah its for the ∣ₖ action on modular forms

[Yaël Dillies]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Eric Wieser]

Something like docs#mul_action.to_perm_hom

[Johan Commelin]

Yael's suggestion might also work

[Yaël Dillies]

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]

Yaël Dillies said:

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

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

[Chris Birkbeck]

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]

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]

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

[Yaël Dillies]

Oh

[Chris Birkbeck]

Johan Commelin said:

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

Yeah its some matrix group.

[Yaël Dillies]

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

[Johan Commelin]

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

[Reid Barton]

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}$).