Action of permutations on functions.

Stream: Is there code for X?

[Wrenna Robson]

Do we have this, or anything like this?

import Mathlib.GroupTheory.GroupAction.Group

instance Equiv.Perm.applySymmPiMulAction (α β : Type*) : MulAction (Equiv.Perm α) (α → β) where
  smul π f := f ∘ π.symm
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

  instance Equiv.Perm.applyPiMulAction (α β : Type*) : MulAction (Equiv.Perm β) (α → β) where
  smul π f := π ∘ f
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

In particular I want to understand how to talk about a symmetric group acting on tuples, but this seems to me to be the natural way to do it.

(Also: MulAction is specifically left actions? Do we have right actions?)

[Eric Wieser]

I believe the first one is docs#DomMulAct

[Eric Wieser]

Equiv.Perm.applyPiMulAction already exists, inferInstance should find it

[Eric Wieser]

Note that you should see an immediate red flag here that you can't have both instances as declared without a type synonym, as you might have alpha = beta

[Wrenna Robson]

Indeed.

[Wrenna Robson]

How do I use inferInstance?

[Wrenna Robson]

instance Equiv.Perm.applyPiMulAction (α β : Type*) : MulAction (Equiv.Perm β) (α → β) := inferInstance

This doesn't work - it can't find it.

[Wrenna Robson]

It's very similar to Pi.mulAction - I mean it virtually is that - but it can't actually make the link?

[Eric Wieser]

import Mathlib

instance Equiv.Perm.applyPiMulAction (α β : Type*) : MulAction (Equiv.Perm β) (α → β) := inferInstance

works for me

[Eric Wieser]

If you're looking for an instance, always use import Mathlib

[Eric Wieser]

Or a little more clearly:

import Mathlib

variable (α β : Type*) in
#synth MulAction (Equiv.Perm β) (α → β) -- Pi.mulAction

[Wrenna Robson]

Aha yeah it'll be an import thing. Does that tell me also where it comes from?

[Wrenna Robson]

DomMulAct is I guess what I want. Seems a little unwieldy to use in practice.

[Wrenna Robson]

@Eric Wieser What I'm not clear on, right, is what you call the thing that does take some f : α → β and pi : Equiv.Perm α and produces f \comp pi. Effectively I guess it's like, the DomMulAct, but for the op? I suppose the equivalent is some
pi : Equiv.Perm β and producing pi.symm \comp f. Which you could do!

I think that is the same is saying: why do the first two of these work, and the second two we don't have

import Mathlib

variable (α β : Type*) in
#synth MulAction (Equiv.Perm β) (α → β)

variable (α β : Type*) in
#synth MulAction (Equiv.Perm α)ᵈᵐᵃ (α → β)

variable (α β : Type*) in
#synth MulAction (Equiv.Perm β)ᵐᵒᵖ (α → β)

variable (α β : Type*) in
#synth MulAction ((Equiv.Perm α)ᵐᵒᵖ)ᵈᵐᵃ (α → β)

[Eric Wieser]

ᵈᵐᵃ already has the reversed multiplication you want

[Wrenna Robson]

Hmm - I am not sure it does, if I'm understanding this right. Or rather it is reversed but I want it not to be.

Let me concretise this a bit. Let's take a : Fin n -> α, which we concieve of as an n-tuple, and I have some π which is a permutation on n points. So "a is the tuple where a i is in the ith place". I want to act on a with π in some natural way to get a permuted tuple b.

There's two obvious ways to permute this tuple, in a sense:
"The permuted tuple b is the tuple where a i is in the π i-th place."
"The permuted tuple b is the tuple where a (π i) is in the ith place."

[Wrenna Robson]

I believe that the action of DomMulAct gives me the first of these (because for this new tuple, the ith place will contain a (π.symm i), i.e. this is "composing on the right by the inverse").

[Wrenna Robson]

In other words, I can define b i = a (π.symm i), that's the first option, or b i = a (π i) - that is the second.

Now I think when you want to start composing permutations it does end up with the first one being a little more natural - that is precisely the DomMulAct thing - but I do think they are both sensible concepts.

[Eric Wieser]

Wrenna Robson said:

In other words, I can define b i = a (π.symm i), that's the first option, or b i = a (π i) - that is the second.

Only one of these two is a left-action, which is what MulAction describes

[Wrenna Robson]

Right, but my understanding is that if one wants to talk about right actions of M, one can talk about left-actions of Mᵐᵒᵖ?

[Wrenna Robson]

So is the second one of these a left-action of anything at all? And if so, what?

[Eric Wieser]

Ah, I understand your question now. Indeed, MulAction (Equiv.Perm β)ᵐᵒᵖ β is the msising piece here, with that in place everything should follow

[Wrenna Robson]

Right - and we don't seem to have that?

[Wrenna Robson]

Yes - I see what you mean. If we had that, then everything else would be inferred.

[Wrenna Robson]

(Thanks for sticking with me there - got a bit twisty.)

[Eric Wieser]

There's a massive family of such actions, and I think I'm the only one that's been adding them. #8396 and #8395 are some more missing ones from the non-opposite family

[Eric Wieser]

I think MulOpposite versions of all those instances for automorphisms is fine; we just need to convince ourselves that they don't form any diamonds

[Eric Wieser]

docs#Function.End.applyMulAction lists most of the instances we already have

[Eric Wieser]

@Henrik Böving, do you know why the auto-linker on that page is not finding docs#LinearEquiv.applyDistribMulAction, and is instead just linking the last fragment of the name?

[Wrenna Robson]

Yeah - it feels like systematically adding them so that you don't miss any is really tricky! And I'm not sure exactly what needs adding (those PRs will presumably be useful for identifying that).

I got to this because I was reading this paper I've been extending DJB's formalisation on, about a representation of permutations as a sequence of bits, and I realised actually in some ways thinking about things in terms of actions is clarifying.

[Eric Wieser]

I think you should make a PR that takes every automorphism in the docs for docs#Function.End.applyMulAction, and creates an opApply*Action that is just TheActionType.compHom MulEquiv.inv' (docs#MulEquiv.inv')

[Henrik Böving]

Eric Wieser said:

Henrik Böving, do you know why the auto-linker on that page is not finding docs#LinearEquiv.applyDistribMulAction, and is instead just linking the last fragment of the name?

Sadly not from the top of my head.

That said I'm kinda holding my breath on the doc improvements by David which will hopefully standartize the way that doc-strings are to be interpreted. Once that happens I am hoping I can just use the APIs the compiler (or wherever it is implemented) will provide in order to process doc-strings.

[Wrenna Robson]

That sounds sensible. I'll have to do it when I have some free time (at the moment I can't really justify spending work time on things that don't get me directly closer to a finished thesis). But I think I can write a bit about this in the thesis, so that is nice!

[Wrenna Robson]

by opApply*Action, do you use the * to mean "AddAction or MulAction as appropriate"?

[Eric Wieser]

at the moment I can't really justify spending work time on things that don't get me directly closer to a finished thesis

Arguably same, but the trick is to avoid having to justify it

[Eric Wieser]

Wrenna Robson said:

by opApply*Action, do you use the * to mean "AddAction or MulAction as appropriate"?

No, they're all multiplicative; I mean MulAction or DistribMulAction or stronger

[Wrenna Robson]

Oh right yes.

[Wrenna Robson]

Yes I mean what I would like is funding to just tootle round in mathlib and do this kind of stuff for cash cash cash, but alas.

[Wrenna Robson]

Still, my supervisor has a funding application in to Amazon to give me a year to focus on implementing a code-based post-quantum scheme in Lean, and maybe that way I would have the time... not that we'll hear for a while.

[Wrenna Robson]

@Eric Wieser So if we had MulAction (Equiv.Perm β)ᵐᵒᵖ β, what would be the instance that would give the second interpretation as above?

[Eric Wieser]

Try it and see?

[Eric Wieser]

Just add that instance with a sorry in your file and see if Lean can find the rest

[Eric Wieser]

(I just tested; it finds instances with exactly the same head symbols as the non-opposite ones, as expected)

[Wrenna Robson]

As I say I feel like it ought to be an instance for MulAction ((Equiv.Perm α)ᵐᵒᵖ)ᵈᵐᵃ (α → β) or possibly MulAction ((Equiv.Perm α)ᵈᵐᵃ)ᵐᵒᵖ (α → β) (they should be the same, should they not?)

[Eric Wieser]

Indeed:

instance : MulAction (Equiv.Perm β)ᵐᵒᵖ β := sorry

variable (α β : Type*) in
#synth MulAction ((Equiv.Perm α)ᵐᵒᵖ)ᵈᵐᵃ (α → β) -- works

variable (α β : Type*) in
#synth MulAction ((Equiv.Perm α)ᵈᵐᵃ)ᵐᵒᵖ (α → β) -- fails

[Eric Wieser]

We have this problem for actions by opposites of units vs units of opposites too, I think

[Wrenna Robson]

It's tricky because I can see it's so you have nicely separated type synonyms. If you didn't have dma and just used mop, that wouldn't work either because of that ambiguity about whether you were acting on domain or codomain when they are the same.

[Wrenna Robson]

Presumably btw I should only add these instances when it makes sense, i.e. for endomorphisms on A acting on A, I can't really use MulEquiv.inv'

[Eric Wieser]

Sure you can, the MulEquiv.inv' is acting on the endomorphism group

[Eric Wieser]

Not onA

[Wrenna Robson]

Hang on, do endomorphisms form a group? I'm getting confused I think with terms.

[Eric Wieser]

No, my mistake, I thought you said automoprhisms

[Wrenna Robson]

Right

[Wrenna Robson]

instance Equiv.Perm.opApplyMulAction (α : Type*) : MulAction (Equiv.Perm α)ᵐᵒᵖ α where
  smul f a := ((MulEquiv.inv' (Equiv.Perm α)).symm f) a
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Does this look like the right sort of thing? I'm not sure about that .symm but the issue was that I don't want to go from
(Equiv.Perm α)ᵐᵒᵖ to (Equiv.Perm α)ᵐᵒᵖᵐᵒᵖ (though I could, and then use the opOp equivalence... not sure what is better).

[Eric Rodriguez]

Can't you use unop or something of the like?

[Wrenna Robson]

instance Equiv.Perm.opApplyMulAction (α : Type*) : MulAction (Equiv.Perm α)ᵐᵒᵖ α where
  smul f a := f.unop.symm a
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

[Wrenna Robson]

This works.

[Eric Wieser]

nstance Equiv.Perm.opApplyMulAction (α : Type*) : MulAction (Equiv.Perm α)ᵐᵒᵖ α :=
  MulAction.compHom _ (MulEquiv.inv' <| Equiv.Perm α).symm.toMonoidHom

[Eric Wieser]

Though your version is fine too

[Wrenna Robson]

That's better though. I think it also wants.

@[simp]
protected theorem Equiv.Perm.op_smul_def {α : Type*} (f : (Equiv.Perm α)ᵐᵒᵖ) (a : α) :
f • a = f.unop.symm a := rfl

And probably also

instance Equiv.Perm.opApplyFaithfulSMul (α : Type*) : FaithfulSMul (Equiv.Perm α)ᵐᵒᵖ α :=
  ⟨sorry⟩

(though I am having some difficulty with that, mainly because for some reason showing that f.symm = g.symm implies f = g is not something exact? can do??)

[Eric Wieser]

docs#Equiv.symm_bijective ... seems to be missing, though all the stronger versions exist

[Wrenna Robson]

Right that is the thing I was looking for and it just... isn't?

[Eric Wieser]

Make a PR with that lemma (and any others around docs#AddEquiv.symm_bijective that are also missing)?

[Eric Wieser]

Looks like it belongs right below docs#Equiv.symm_symm

[Wrenna Robson]

Yes. I see we have here docs#EquivLike.inv_apply_apply a "TODO" for a generic version of symm, and on some level probably you would want a generic version of that lemma too...

[Wrenna Robson]

theorem symm_bijective : Function.Bijective (Equiv.symm : α ≃ β → β ≃ α) :=
Equiv.bijective ⟨Equiv.symm, Equiv.symm, symm_symm, symm_symm⟩

This is what it wants to be I think (that's basically what all the others do that I've checked!)

[Yaël Dillies]

Eric Wieser said:

There's a massive family of such actions, and I think I'm the only one that's been adding them. #8396 and #8395 are some more missing ones from the non-opposite family

I've also added a few, and MulAction (Perm β)ᵐᵒᵖ β was on my todo list. But it's a very long list :upside_down:

[Wrenna Robson]

@Eric Wieser The problem was oddly pervasive and I have added a lemma everywhere we had a symm_symm. In one case we had a symm_injective but I haven't removed that, just changed it to be the obvious corollory of symm_bijective. I'm going to have to see if the build likes it and check any little issues as we go, as as you can imagine that invalidated a lot of the cache. https://github.com/leanprover-community/mathlib4/pull/8444