Beginner formalizing group actions

Stream: new members

[Yiming Xu]

Hi everyone. I am starting to get my hands dirty by doing a little exercise in Lean. I would like mature users to make comments and suggestions during my attempt to the proof. This post would be updated in the next few days, with very stupid and naive newbie questions. I appreciate everyone who may come by and say something.

I think the point that I mostly need help is on the "structures" and "instances". There seems to be a whole bunch of black technologies here, but at the beginning, I would appreciate if you might teach me in a rather elementary way.

My goal is to prove the category of group actions has exponential (it may already be in mathlib, but even if it is the case, I just would like to re-prove it to get the practice).

The category has objects set $X$ with $X\times M\to X$ a right action, and a map $X\to Y$ is an $M$-equivarient map.

Given $X,Y$ such $M$-sets, the exponential consists of the following information:

The set $[M\times X, Y]$ of equivarient maps $M\times X \to Y$, with the action map $[M\times X , Y]\times M\to [M\times X,Y]$ defined by $(e,k)\mapsto e\cdot k$, where $e\cdot k$ is the map $[M\times X,Y]$ defined by $e\cdot k(g,x) = e(kg,x)$, where $kg$ is the product taken in the monoid $M$.

Background:
I have read some chapters of Hitchhiker's Guide:
https://github.com/lean-forward/logical_verification_2024/blob/main/hitchhikers_guide_2024_desktop.pdf
and some of "mathematics in Lean". They are my main text references. But I have not tried all the exercises. In particular, I think things start getting complicated after chapter 7. Hopefully, I can get more sense of it by practicing . My memory is not very good so sorry if I forget things.

If you intend to help me better using analogy, thanks for your attempt! Comparision with HOL4, Isabelle, and Standard ML would make sense to me, but I would not understand it if you were speaking about Coq/Haskell/C/java/Python.etc, and programming languages in general(unless you are willing to teach me the background story as well.).

Helpful suggestions include, but are far from being limited to:
Alternative presentation of definitions/theorems (not necessarily better maybe, but let me see some alternative approaches.)
Specific tactics/functions that may be helpful(or just eye-opening for a beginner).
Point to similar examples that I can look up. (Ideally in "mathematics in Lean", but not necessary).

In MIL Chapter8 https://leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html I see the example:

variable {G : Type*} [Group G]

lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
  sorry

instance : MulAction G (Subgroup G) where
  smul := conjugate
  one_smul := by
    sorry
  mul_smul := by
    sorry

end GroupActions

where "Subgroup" is a "structure", not a "class". I will need to construct the type of all equivariant maps of an action, should it be a structure or a class? What are the differences if any?

[Yiming Xu]

I quickly wrote a piece of (wrong!) instance, and have question about it. here it is:

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ one_smul := sorry,
 mul_smul := sorry}

It is wrong, because I should not use the whole type M × X -> Y, but the subtype consisting only the equivariant maps instead.

[Yiming Xu]

I am curious that why Lean still parses it, the above piece of wrong code does not report any error. But here I even have not specified the action yet! It should report an error and ask me for the field smul. What is Lean guessing in this case?

[Yiming Xu]

If I ignore the wrongness of this instance, and want to specify the smul, I get confused again. I wrote the smul in {}, it asks for a term:

X : Type u_2
Y : Type u_3
M : Type u_1
inst✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : MulAction M Y
⊢ M → (M × X → Y) → M × X → Y

and I wrote:

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ ⟨fun (g,x) ↦ e (M.smul k g,x)⟩,
  one_smul := sorry,
  mul_smul := sorry}

I see it reports an error, as in:
image.png

[Yiming Xu]

May I please ask why is the error? Am I wrong with the syntax?

[Ruben Van de Velde]

Please share a #mwe with all code, including imports, that we need to see that error in the web editor

[Yiming Xu]

import Mathlib.Algebra.Group.Action.Defs


instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ ⟨fun (g,x) ↦ e (M.smul k g,x)⟩,
  one_smul := sorry,
  mul_smul := sorry}

[Yiming Xu]

Thanks! This parses in the web editor, with an error that I would like to know the reason and fix.

[Yiming Xu]

Yiming Xu said:

I quickly wrote a piece of (wrong!) instance, and have question about it. here it is:

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ one_smul := sorry,
 mul_smul := sorry}

It is wrong, because I should not use the whole type M × X -> Y, but the subtype consisting only the equivariant maps instead.

I tried

import Mathlib.Algebra.Group.Action.Defs


instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ one_smul := sorry,
  mul_smul := sorry}

reports the error of missing smul, and I expected, in the web editor, but not in VScode. What happens there?

[Yiming Xu]

This one does not work

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (M.mul k g, x),
  one_smul := sorry,
  mul_smul := sorry}

[Yiming Xu]

But that one works.

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (@Mul.mul M _ k g, x),
  one_smul := sorry,
  mul_smul := sorry}

[Yiming Xu]

Anyone know why?

[Kevin Buzzard]

What's the error?

[Kevin Buzzard]

Why not just use k * g?

[Yiming Xu]

Kevin Buzzard said:

What's the error?

Weird! The web version does not give any error for this piece of code

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (M.mul k g, x),
  one_smul := sorry,
  mul_smul := sorry}

but my local lean reports on the same piece of code reports:

invalid field notation, type is not of the form (C ...) where C is a constant
  M
has type
  Type u_1

.

[Yiming Xu]

Kevin Buzzard said:

Why not just use k * g?

Thanks! It simply works.

[Yiming Xu]

Another question: If I delete the {M : Type*} from

instance X2Y {M : Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (k * g, x),
  one_smul := sorry,
  mul_smul := sorry}

then it does not report any error, so does it make any practical difference if I write {M : Type*} in the statement or not? I guess maybe it only makes some difference if the type M is required to be in some universe level, say, the level has to be non-zero?

[Kevin Buzzard]

Probably you have set_option autoImplicit set to true. You can just compare the types of the declarations before and after the change by hovering over X2Y to see if there is any difference. Having autoImplicit true is a bit of a footgun so beware.

[Yiming Xu]

Thanks! I checked according your instruction just now.

Before the change, I have:

X2Y.{u_1, u_2, u_3} {X : Type u_2} {Y : Type u_3} {M : Type u_1} [Monoid M] [MulAction M X] [MulAction M Y] :
  MulAction M (M × X → Y)

and after the change, I see:

X2Y.{u_1, u_2, u_3} {M : Type u_1} {X : Type u_2} {Y : Type u_3} [Monoid M] [MulAction M X] [MulAction M Y] :
  MulAction M (M × X → Y)

Seems no difference except for the order of arguments.

But if I write set_option autoImplicit false, then Lean is unhappy until I wrote:

instance X2Y {M : Type*} {X : Type*} {Y:Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (k * g, x),
  one_smul := sorry,
  mul_smul := sorry}

.

[Yiming Xu]

Kevin Buzzard said:

Probably you have set_option autoImplicit set to true. You can just compare the types of the declarations before and after the change by hovering over X2Y to see if there is any difference. Having autoImplicit true is a bit of a footgun so beware.

I conceive it as "I should have autoImplicit false" so I should write like:

instance X2Y {M : Type*} {X : Type*} {Y:Type*} [Monoid M]  [MulAction M X] [MulAction M Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (k * g, x),
  one_smul := sorry,
  mul_smul := sorry}

instead. Thank you!

[Yiming Xu]

It seems like MulAction is designed for left action, is there already something done with right action as well? Existing examples in mathlib would be very helpful.(Since the proof I wrote uses right action. )

[Eric Wieser]

For right actions, you can use MulAction (MulOpposite _) _

[Yiming Xu]

Thanks for the swift reply! Let me look it up.

[Yiming Xu]

I tried

import Mathlib.Algebra.Group.Action.Defs

instance X2Y {M : Type*} {X : Type*} {Y:Type*} [Monoid M]  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] : MulAction M (M × X -> Y):=
{ smul:= fun k e ↦ fun (g,x) ↦ e (k * g, x),
  one_smul := sorry,
  mul_smul := sorry}

and it reports error under [MulAction (MulOpposite M) X] .

[Yiming Xu]

It is complaining about

failed to synthesize
  Monoid Mᵐᵒᵖ

I think I should use Monoid.toOpposite for that, as in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Action/Opposite.html#Monoid.toOppositeMulAction.

[Kevin Buzzard]

Yes, you're not importing enough. The problem with the Defs files is that they contain only definitions, no theorems (like the theorem you need).

[Kevin Buzzard]

When developing, I just import Mathlib and then cut things down at the end. With import Mathlib your code works fine.

[Yiming Xu]

Ah yes after importing the error under [MulAction (MulOpposite M) X] goes away. Thanks for the swift reply!

[Yiming Xu]

Kevin Buzzard said:

When developing, I just import Mathlib and then cut things down at the end. With import Mathlib your code works fine.

Just tried it locally with import Mathlib and it works fine.

[Yiming Xu]

In this case, there is obviously only one instance for M to be a monoid, but M can have multiple monoid structures, so there might be multiple instances. In the case that I want to provide the instance by hand, what should I write in ??? for the instance that M^mop is a monoid?

variable {M : Type*} [Monoid M] {X : Type*}
#check @Monoid.toOppositeMulAction M ???

Does the instance [Monoid M] has a name?

#check @Monoid.toOppositeMulAction M  [Monoid M]

reports error.

[Kevin Buzzard]

Mathlib is designed with the assumption that a type will only have one monoid structure. If it has more than one then x * y is ambiguous for x y : M. There are ways to work around this but you'll have to say more about your use case. If you have multiple instances then basically all but the last one will be ignored.

[Kevin Buzzard]

If you want to give the instance a name you can name it with [h : Monoid M] but the design of mathlib is such that this should not really be necessary most of the time. You can look in the infoview to see what the system calls it when you don't give it a name yourself, it's probably called _inst_37 or something.

[Yiming Xu]

Thanks for the elaboration! Great! I checked that

variable {M : Type*} [h:Monoid M] {X : Type*}
#check @Monoid.toOppositeMulAction M h

works. And the fact that there is only one instance explains my confusion that why instances do not have a name.

[Yiming Xu]

By "multiple structures on one type" I basically mean, e.g. $\Bbb Z$ can be a mulgroup or/and an addgroup. But I guess in this case we would have one instance for mulgroup and another instance for addgroup, instead of having two instances for the structure : group.

[Kevin Buzzard]

Yes that's right, Z is both a multiplicative and an additive monoid and this is of course important for mathematics, which is why we have both Monoid and AddMonoid.

Here are some other tricks:

import Mathlib

variable {M : Type*} [Monoid M] {X : Type*}

#check @Monoid.toOppositeMulAction M ‹Monoid M›
#check @Monoid.toOppositeMulAction M inferInstance

[Yiming Xu]

I see. Instead of giving it a name, I can just use the term ‹Monoid M› for the instance term. (Aha, that looks similar to the counterpart in Isabelle: we have the option of giving it a name, or quote the statement in triangular brackets).

[Mario Carneiro]

fun fact, this syntax was borrowed from isabelle

[Yiming Xu]

Mario Carneiro said:

fun fact, this syntax was borrowed from isabelle

Funny! Then maybe also the "from" syntax.

[Yiming Xu]

Had some hard time trying to get the "MulOpposite" correct.
Bugged a colleague and got a pieces of suggestion:
1.Helpful to prove lemmas about the operations like:

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e (k * g, x)

theorem Test.smul_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : M) (e : M × X → Y) : k • e = fun (g,x) ↦ e (k * g, x) :=by rfl

and write smul:= Test.smul.smul as the field, instead of expanding the explicit definition.
2.If I have variables and instances declared as

variable {M : Type*} [Monoid M] {X : Type*} {Y:Type*}

then I should omit them from my definition X2Y, and have:

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] : MulAction (MulOpposite M) (M × X -> Y)

instead.

I have trouble getting the MulOpposite work. Recall I want $M$ to act on maps $M\times X \to Y$ as: for $e:M\times X\to Y$ and $k\in M$, $e\cdot k (g,x) = e(kg,x)$, where $kg$ is taken in $M$ (instead of $M^{mop}$), as a right action.

I want to write:

import Mathlib

set_option autoImplicit false
set_option diagnostics true

variable {M : Type*} [Monoid M] {X : Type*} {Y:Type*}

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e (k * g, x)

Lean complains and tells me:

failed to synthesize
  HMul Mᵐᵒᵖ M ?m.546

Seems that it is asking for an instance for $M^{mop}$?

But for the e (k * g, x), I do not want it to be taken in $M^{mop}$, but in $M$ instead. How should I tell Lean?

[Yiming Xu]

The broken attempt up to now:

import Mathlib
set_option autoImplicit false
set_option diagnostics true

variable {M : Type*} [Monoid M] {X : Type*} {Y:Type*}

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e (k * g, x)

theorem Test.smul_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : M) (e : M × X → Y) : k • e = fun (g,x) ↦ e (k * g, x) :=by rfl

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] : MulAction (MulOpposite M) (M × X -> Y):=
{ smul:= Test.smul.smul
  one_smul := by
   intro b
   rw [Test.smul_def]
   simp


  mul_smul := by
    intros k1 k2 e
    simp_rw [Test.smul_def]
    ext x
    congr 2
    ac_rfl}

[Kevin Buzzard]

op : α → αᵐᵒᵖ and unop : αᵐᵒᵖ → α are the maps you need to use (in the MulOpposite namespace).

[Kevin Buzzard]

import Mathlib
set_option autoImplicit false
set_option diagnostics true

variable {M : Type*} [Monoid M] {X : Type*} {Y:Type*}

open MulOpposite -- make namespace available

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e (unop k * g, x)

[Kevin Buzzard]

You shouldn't think of Mᵐᵒᵖ and M as being equal. If they were, then a * b would be ambiguous. You need to pass between them using functions. They encode the same information in Lean, but they are not equal.

[Yiming Xu]

Thanks a lot! I see. You have just told me that there can be only one instance for one underlying type. op passes to another monoid structure, so we have to change the underlying type as well, otherwise, it does not even get type-checked.

[Yiming Xu]

But let me check if this is what I want...

I think so. Now k is now from MulOpposite M, and what we are taking is unop k * g, it is sends k back to M and then multiply with g in M.

Okay nice!

[Yiming Xu]

Then the lemma should be

theorem Test.smul_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : MulOpposite M) (e : M × X → Y) : k • e = fun (g,x) ↦ e ( (unop k) * g, x) :=by rfl

[Yiming Xu]

And here is the instance:

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] : MulAction (MulOpposite M) (M × X -> Y):=
{ smul:= Test.smul.smul
  one_smul := by
   intro b
   rw [Test.smul_def]
   simp
  mul_smul := by
    intros k1 k2 e
    simp_rw [Test.smul_def]
    ext x
    congr 2
    simp
    ac_rfl }

[Kevin Buzzard]

Here is a golfed version where I get simp to do all the work:

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] :
    MulAction (MulOpposite M) (M × X -> Y) where
  smul := Test.smul.smul
  one_smul b := by
   simp [Test.smul_def]
  mul_smul k1 k2 e := by
    ext ⟨m, x⟩
    simp [Test.smul_def, mul_assoc]

[Yiming Xu]

Nice! From here I also see the {} is not necessary, and I can give arguments for one_smul to get rid of the intros.

[Kevin Buzzard]

In fact I had to get rid of the {}s to use the arguments trick :-(

[Eric Wieser]

Yiming Xu said:

You have just told me that there can be only one instance for one underlying type

Note that you unfortunately have a new problem here: mathlib already provide a solution to MulAction (MulOpposite M) (M × X -> Y), which you can find as Pi.mulAction Mᵐᵒᵖ:

-- put this before X2Y
variable [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] in
#synth  MulAction (MulOpposite M) (M × X -> Y)

Unfortunately Pi.mulAction Mᵐᵒᵖ ≠ X2Y in general, so now you have the same issue you had with worrying about multiple monoid structures on M

[Yiming Xu]

Kevin Buzzard said:

In fact I had to get rid of the {}s to use the arguments trick :-(

I see. That is good to know.

[Yiming Xu]

Eric Wieser said:

Yiming Xu said:

You have just told me that there can be only one instance for one underlying type

Note that you unfortunately have a new problem here: mathlib already provide a solution to MulAction (MulOpposite M) (M × X -> Y), which you can find as Pi.mulAction Mᵐᵒᵖ:

-- put this before X2Y
variable [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] in
#synth  MulAction (MulOpposite M) (M × X -> Y)

Unfortunately Pi.mulAction Mᵐᵒᵖ ≠ X2Y in general, so now you have the same issue you had with worrying about multiple monoid structures on M

Wow that seems fatal... So maybe I can try to, instead, create a type class of right action instead? Or is there any suggestions on how would I solve this clash?

[Kevin Buzzard]

The issue is not left/right action, the issue is that mathlib has taken the decision that if G acts on X, then G acts on functions from anything to X in the obvious way. If you want to make G act on functions in a different way, then you need to give your function space a new name. Giving it a new name will stop typeclass inference (the system which is finding all the actions) from finding the mathlib standard axiom.

[Kevin Buzzard]

import Mathlib

variable (x : ℤˣ) (f : ℕ → ℤ)

#check x • f -- action defined by obvious action on the target

def NewType := ℕ → ℤ -- `NewType` is *equal* to `ℕ → ℤ`

variable (g : NewType)

#check x • g -- error

[Notification Bot]

rzeta0 has marked this topic as resolved.

[Kevin Buzzard]

Equality is a very subtle concept in a theorem prover. NewType and ℕ → ℤ are equal, but they could be more equal! In particular typeclass inference doesn't notice that they are equal. So now you are free to define any action of ℤˣ on NewType that you like, without any problems.

[Notification Bot]

rzeta0 has marked this topic as unresolved.

[Yiming Xu]

Kevin Buzzard said:

Equality is a very subtle concept in a theorem prover. NewType and ℕ → ℤ are equal, but they could be more equal! In particular typeclass inference doesn't notice that they are equal. So now you are free to define any action of ℤˣ on NewType that you like, without any problems.

So it reports an error because it does not find any instance on NewType, I see. But in which sense are they more equal?

[Yiming Xu]

[I just recalled that I want my action not on the whole $M\times X\to Y$! Only on the set of $M$-equivariant maps, hopefully Lean do not have already an instance on this set... But that is important to know how to resolve the clash.]

[Kevin Buzzard]

Aah, but this is great: if you only care about M-equivariant maps then your problem is solved because that definitely won't be equal to the space of all maps.

To learn about the levels of equality being talked about here, you need to understand when Lean unfolds a definition. I can't remember the exact definitions, but I know that typeclass inference will not unfold a def but will unfold an abbrev.

import Mathlib

variable (x : ℤˣ) (f : ℕ → ℤ)

#check x • f -- action defined by obvious action on the target

abbrev NewType := ℕ → ℤ -- now they are a bit more equal

variable (g : NewType)

#check x • g -- no error

I think there are three levels of reducibility for definitions: reducible, semireducible and irreducible, and different parts of the system will check different levels of reducibility. This is some technicality about how the system works internally which I never learnt (or more likely, learnt and then forgot, and I think it might even have changed recently). But the thing to remember is that typeclass inference sees through abbrevs and not through defs, this is what I use in practice when writing Lean code, and it informs which of the two choices I want to make for a new definition.

[Yiming Xu]

That makes a lot of sense! In Isabelle, abbrev is purely notational, i.e. for pretty-printing only. The parser conceive them as the same, so, if we write abbrev A = B, then the parser really read A as B, and the kernel that manipulates the logic never know what A is, because it get access to B only, and never sees A. A can only be seen by the parser, so it is impossible to "unfold" A.

I guess maybe Lean does something similar, so abbrev is just notational. Unfortunately I cannot read C and hence the source code of Lean...

[Eric Wieser]

Kevin Buzzard said:

If you want to make G act on functions in a different way, then you need to give your function space a new name

Or give G a new name. It would be tempting to spell your action MulAction (DomMulAct (Prod.FstAct M) (M × X -> Y) instead, where you would then need to implement MulAction (Prod.FstAct M) (M × X) which would give you the instance you want for free.

But this then runs into trouble when X := M × M, because this then conflicts with the instance saying that actions on products are induced by actions on both elements... (Edit: nevermind, this can't actually happen in this specific case). There is a short section in my thesis about the troubles that arise with docs#DomMulAct and similar patterns, but none of the solutions are very appealing.

[Yiming Xu]

Eric Wieser said:

Kevin Buzzard said:

If you want to make G act on functions in a different way, then you need to give your function space a new name

Or give G a new name. It would be tempting to spell your action MulAction (DomMulAct (Prod.FstAct M) (M × X -> Y) instead, where you would then need to implement MulAction (Prod.FstAct M) (M × X) which would give you the instance you want for free.

But this then runs into trouble when X := M × M, because this then conflicts with the instance saying that actions on products are induced by actions on both elements... (Edit: nevermind, this can't actually happen in this specific case). There is a short section in my thesis about the troubles that arise with docs#DomMulAct and similar patterns, but none of the solutions are very appealing.

Do you mean like this?

import Mathlib

variable (x : ℤˣ) (f : ℕ → ℤ)

#check x • f -- action defined by obvious action on the target

def NewType := ℤˣ -- `NewType` is *equal* to `ℕ → ℤ`

variable (x : NewType)

#check x • f -- error

[Yiming Xu]

But what is the DomMulAct and Prod.FstAct stuff? I am afraid I do not get this part.

[Yiming Xu]

For another question I am confused: The following code does not have any error:

import Mathlib
set_option autoImplicit false
set_option diagnostics true

variable {M : Type*} [Monoid M] {X : Type*} {Y:Type*}

open MulOpposite -- make namespace available

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e (unop k * g, x)

theorem Test.smul_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : MulOpposite M) (e : M × X → Y) : k • e = fun (g,x) ↦ e ( (unop k) * g, x) :=by rfl

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] : MulAction (MulOpposite M) (M × X -> Y):=
{ smul:= fun k ↦ fun e↦  fun (g,x) ↦ e ( (unop k) * g, x)
  one_smul := by
   intro b
   rw [Test.smul_def]
   simp
  mul_smul := by
    intros k1 k2 e
    simp_rw [Test.smul_def]
    ext x
    congr 2
    simp
    ac_rfl }

My questions are:
1.Note that the definition of smul is written by hand here, why does the rw [Test.smul_def] give the rw? I did not tell Lean that the dot here is the smul above. Is it again because it only accepts one structure, and just found the one above?
2.If I omit the definition of Test.smul and Test.smul_def, and want to just write something like (note that the tactic does not work anymore), what should I type after intro b to unfold 1 • b = b, where \cdot is defined as fun k ↦ fun e↦ fun (g,x) ↦ e ( (unop k) * g, x) . (Bugged a colleague in Lean, tried that simp[ (_ \cdot _)] does not work.)

import Mathlib
set_option autoImplicit false
set_option diagnostics true

variable {M : Type*} [Monoid M] {X : Type*} {Y:Type*}

open MulOpposite -- make namespace available

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] : MulAction (MulOpposite M) (M × X -> Y):=
{ smul:= fun k ↦ fun e↦  fun (g,x) ↦ e ( (unop k) * g, x)
  one_smul := by
   intro b
   rw [Test.smul_def]
   simp
  mul_smul := by
    intros k1 k2 e
    simp_rw [Test.smul_def]
    ext x
    congr 2
    simp
    ac_rfl }

[Yiming Xu]

I think I have difficulty defining the action only on equivariant maps. I have tried asking around but have not found a satisfactory solution. Firstly, code up to now, for copying and pasting:

import Mathlib


set_option autoImplicit false
set_option diagnostics true
#check MulOpposite
variable (M : Type*) [Monoid M] {X : Type*} {Y:Type*}
--#check @Monoid.toOppositeMulAction M h
#check ‹Monoid M›
#check Mul (Mᵐᵒᵖ)
#check @Monoid.toOppositeMulAction M ‹Monoid M›
#check @Monoid.toOppositeMulAction M inferInstance

open MulOpposite
instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e ((unop k) * g, x)


theorem Test.smul_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : MulOpposite M) (e : M × X → Y) : k • e = fun (g,x) ↦ e ( (unop k) * g, x) :=by rfl

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] :
    MulAction (MulOpposite M) (M × X -> Y) where
  smul := (Test.smul M).smul
  one_smul b := by
   simp [Test.smul_def]
  mul_smul k1 k2 e := by
    ext ⟨m, x⟩
    simp [Test.smul_def,mul_assoc]

/-

class MulAction (α : Type*) (β : Type*) [Monoid α] extends SMul α β where
  /-- One is the neutral element for `•` -/
  protected one_smul : ∀ b : β, (1 : α) • b = b
  /-- Associativity of `•` and `*` -/
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b
-/
/-
1. is it fine to declare variable and use this to declare a class?
2.class vs structure, which one to choose?
-/
class Equivariant (E: Type*) [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] [FunLike E X Y] where
 comm_square : ∀ (f: E) (x : X) (m : Mᵐᵒᵖ), m • f x = f (m • x)

@[ext]
structure Eqvariant_struct (X : Type*) (Y:Type*) [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] where
 toFun: X → Y
 comm_square : ∀ (x : X) (m : Mᵐᵒᵖ), m • (toFun x) = toFun (m • x)


variable (f:X → Y)

instance Test.smul1 [MulAction (MulOpposite M) X]: SMul (MulOpposite M) (M × X) where
  smul a  := fun ⟨m, x⟩ ↦ (a • m, a • x)


instance Msmul : SMul (MulOpposite M) M where
  smul m0 m :=  m * (unop m0)


theorem Msmul_def (m0 : MulOpposite M) (m : M) : m0 • m = m * (unop m0) :=by rfl


instance : MulAction (MulOpposite M) M where
  smul m0 m:= m * (unop m0)
  one_smul := by simp[Msmul_def]
  mul_smul m1 m2 m := by
    simp[Msmul_def,mul_assoc]

theorem Test.smul1_def
   [MulAction (MulOpposite M) X]
    (a: MulOpposite M) (mx : M× X): (a • mx = (a • mx.1, a • mx.2)) := by rfl




instance foo [MulAction (MulOpposite M) X] : MulAction (MulOpposite M) (M × X) where
 smul a:= (Test.smul1 M).smul a
 one_smul b := by simp [Test.smul1_def]
 mul_smul k1 k2 mx := by
    simp [Test.smul1_def]
    simp [mul_assoc, mul_smul k1 k2 mx.2]


/-action on equivariant function e: M × X → Y by

class Equivariant (E: Type*) [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] [FunLike E X Y] where
 comm_square : ∀ (f: E) (x : X) (m : Mᵐᵒᵖ), m • f x = f (m • x)

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e ((unop k) * g, x)

always give an equivariant function
 -/

def smul_eqv [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
            (k : (MulOpposite M))
             (e: Eqvariant_struct M (M × X) Y)
             : Eqvariant_struct M (M × X) Y where
  toFun := k • e.toFun
  comm_square mx m0 := by
    cases mx with
    | mk m x =>
    --want m0 • ((k • e.toFun) (m, x)) = (k • e.toFun) (m0 • (m, x))
    --the left m0 acts on the element in Y. unfold the definition of k on e first
      simp[Test.smul_def]
    -- reduce to m0 • e.toFun (unop k * m, x) = e.toFun (unop k * (m * unop m0), m0 • x)
    -- e is equivariant says m0 • e.toFun (unop k * m, x) is equal to the thing
    -- when we move the m0 to act on the pair first, invoke comm_square on this pair
      simp [e.comm_square (unop k * m, x) m0]
    --e.toFun (unop k * m * unop m0, m0 • x) = e.toFun (unop k * (m * unop m0), m0 • x)
    --curiously, automatically unfold the action of m0 is pairewise
      simp[mul_assoc]

/-
lemma Action_Equivariant (E: Type*)
[MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] [FunLike E (M × X) Y]
(f: E) :
-/

instance [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
         : MulAction (MulOpposite M) (Eqvariant_struct M (M × X) Y) where
 smul k e := smul_eqv M k e
 one_smul b:= by
   ext mx
   cases' mx with m x --put cursor here to see my issue

   simp[smul_eqv]

I am on my way to construct the group action on the structures of equivariant maps. I am stuck on the goal looks like:

M : Type u_1
inst✝² : Monoid M
X : Type u_2
Y : Type u_3
f : X → Y
inst✝¹ : MulAction Mᵐᵒᵖ X
inst✝ : MulAction Mᵐᵒᵖ Y
b : Eqvariant_struct M (M × X) Y
m : M
x : X
⊢ (1 • b).toFun (m, x) = b.toFun (m, x)

Here 1 \smul b is not parsed as a function M \times X \to Y, but as a structure, and I would like to tell Lean to unfold the definition of the action on maps, so the LHS is equal to b.toFun (1 * m, x). May I please ask how would I do it?

[Yiming Xu]

I believe I have solved it. But more help is needed for the exponential proof. I will ask in more detail in a separate post. (okay, maybe I am over-confident?)

[Eric Wieser]

You shouldn't need

instance Msmul : SMul (MulOpposite M) M where
  smul m0 m :=  m * (unop m0)

this is builtin to mathlib

[Yiming Xu]

Let me try to delete it.

[Yiming Xu]

You are right. Thank you!

[Yiming Xu]

I will have to prove the construction makes equivariant maps $M\times X\to Y$ an exponential.

[Yiming Xu]

Is Cartesian.lean the correct file to look at?

[Eric Wieser]

I think your Equivariant is docs#MulActionHom with φ := id

[Yiming Xu]

import Mathlib


set_option autoImplicit false
set_option diagnostics true
#check MulOpposite
variable (M : Type*) [Monoid M] {X : Type*} {Y:Type*}
--#check @Monoid.toOppositeMulAction M h
#check ‹Monoid M›
#check Mul (Mᵐᵒᵖ)
#check @Monoid.toOppositeMulAction M ‹Monoid M›
#check @Monoid.toOppositeMulAction M inferInstance

open MulOpposite
instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e ((unop k) * g, x)


theorem Test.smul_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : MulOpposite M) (e : M × X → Y) : k • e = fun (g,x) ↦ e ( (unop k) * g, x) :=by rfl

instance X2Y  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] :
    MulAction (MulOpposite M) (M × X -> Y) where
  smul := (Test.smul M).smul
  one_smul b := by
   simp [Test.smul_def]
  mul_smul k1 k2 e := by
    ext ⟨m, x⟩
    simp [Test.smul_def,mul_assoc]

/-

class MulAction (α : Type*) (β : Type*) [Monoid α] extends SMul α β where
  /-- One is the neutral element for `•` -/
  protected one_smul : ∀ b : β, (1 : α) • b = b
  /-- Associativity of `•` and `*` -/
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b
-/
/-
1. is it fine to declare variable and use this to declare a class?
2.class vs structure, which one to choose?
-/
class Equivariant (E: Type*) [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] [FunLike E X Y] where
 comm_square : ∀ (f: E) (x : X) (m : Mᵐᵒᵖ), m • f x = f (m • x)

@[ext]
structure Eqvariant_struct (X : Type*) (Y:Type*) [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] where
 toFun: X → Y
 comm_square : ∀ (x : X) (m : Mᵐᵒᵖ), m • (toFun x) = toFun (m • x)


variable (f:X → Y)

instance Test.smul1 [MulAction (MulOpposite M) X]: SMul (MulOpposite M) (M × X) where
  smul a  := fun ⟨m, x⟩ ↦ (a • m, a • x)



theorem Test.smul1_def
   [MulAction (MulOpposite M) X]
    (a: MulOpposite M) (mx : M× X): (a • mx = (a • mx.1, a • mx.2)) := by rfl




instance foo [MulAction (MulOpposite M) X] : MulAction (MulOpposite M) (M × X) where
 smul a:= (Test.smul1 M).smul a
 one_smul b := by simp [Test.smul1_def]
 mul_smul k1 k2 mx := by
    simp [Test.smul1_def]
    simp [mul_assoc, mul_smul k1 k2 mx.2]


/-action on equivariant function e: M × X → Y by

class Equivariant (E: Type*) [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] [FunLike E X Y] where
 comm_square : ∀ (f: E) (x : X) (m : Mᵐᵒᵖ), m • f x = f (m • x)

instance Test.smul : SMul (MulOpposite M) (M × X → Y) where
  smul k e := fun (g,x) ↦ e ((unop k) * g, x)

always give an equivariant function
 -/

def smul_eqv [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
            (k : (MulOpposite M))
             (e: Eqvariant_struct M (M × X) Y)
             : Eqvariant_struct M (M × X) Y where
  toFun := k • e.toFun
  comm_square mx m0 := by
    cases mx with
    | mk m x =>
    --want m0 • ((k • e.toFun) (m, x)) = (k • e.toFun) (m0 • (m, x))
    --the left m0 acts on the element in Y. unfold the definition of k on e first
      simp[Test.smul_def]
    -- reduce to m0 • e.toFun (unop k * m, x) = e.toFun (unop k * (m * unop m0), m0 • x)
    -- e is equivariant says m0 • e.toFun (unop k * m, x) is equal to the thing
    -- when we move the m0 to act on the pair first, invoke comm_square on this pair
      simp [e.comm_square (unop k * m, x) m0]
    --e.toFun (unop k * m * unop m0, m0 • x) = e.toFun (unop k * (m * unop m0), m0 • x)
    --curiously, automatically unfold the action of m0 is pairewise
      simp[mul_assoc]

/-
lemma Action_Equivariant (E: Type*)
[MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] [FunLike E (M × X) Y]
(f: E) :
-/

theorem smul_eqv_def_toFun
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : MulOpposite M) (e: Eqvariant_struct M (M × X) Y) :
    k • e.toFun = fun (g,x) ↦ e.toFun ( (unop k) * g, x) :=by rfl

instance [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] :
    SMul (MulOpposite M) (Eqvariant_struct M (M × X) Y) where
  smul k e := smul_eqv M k e

theorem smul_eqv_def
   [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
    (k : MulOpposite M) (e: Eqvariant_struct M (M × X) Y) :
    k • e = smul_eqv M k e :=by rfl


instance [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
         : MulAction (MulOpposite M) (Eqvariant_struct M (M × X) Y) where
 smul k e := smul_eqv M k e
 one_smul b:= by
   ext mx
   cases' mx with m x
   rw [smul_eqv_def, smul_eqv]
   simp
 mul_smul := by
  intros m m' e
  repeat rw [smul_eqv_def, smul_eqv]
  ext ⟨m, x⟩
  simp
  repeat rw [Test.smul_def]
  simp[mul_assoc]

Things up to now.

[Yiming Xu]

Eric Wieser said:

I think your Equivariant is docs#MulActionHom with φ := id

Thanks and let me take a look! Maybe I should try to use it to get myself familiarize with how to connect to mathlib before going further.

[Yiming Xu]

I agree with you on that. Thanks for the information!

[Yiming Xu]

I would like to make an abbreviation to for the maps I want. Why is:

abbrev Equivariant [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] :=
  MulActionHom id X Y

not working?

[Yiming Xu]

I would like to make MulAction a category, how would we call the whole collection of MulActions?

[Eric Wieser]

Yiming Xu said:

I would like to make an abbreviation to for the maps I want. Why is:

abbrev Equivariant [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y] :=
  MulActionHom id X Y

not working?

This doesn't work because you need to write (@id (MulOpposite M)) instead of id; but mathlib already has notation for this, X →[MulOpposite M] Y

[Yiming Xu]

So given X and Y types and instances that X and Y has actions, then X →[MulOpposite M] Y is the type for all equivariant maps between X and Y?

[Yiming Xu]

I see, I can check it by

variables  [MulAction (MulOpposite M) X] [MulAction (MulOpposite M) Y]
#check (X →[MulOpposite M] Y)

[Yiming Xu]

Is there also a notion of "the category of actions" existing in mathlib already?

[Eric Wieser]

docs#Action might be what you want

[Yiming Xu]

Thank you! This is very helpful. I think what I should investigate is:

#check Action (Type u_1) (MonCat.of (MulOpposite M))

where the Type u_1 is often left out as _.

Please correct me if I am wrong!

[Yiming Xu]

Why do I have a red underscore under Category reporting error when I type:

#check Category (Action (Type u_1) (MonCat.of (MulOpposite M)))

Lean complains:
unknown identifier 'Category'

But I have already imported mathlib.

[Yaël Dillies]

Have you done open CategoryTheory?

[Yiming Xu]

Yaël Dillies said:

Have you done open CategoryTheory?

No! Thank you! After opening CategoryTheory it works!

[Yiming Xu]

May I please ask if there exists any example proving some category has exponentials? The definition of exponential is very nested.

[Yiming Xu]

Confused again, I think I should start from:

instance HasFiniteProducts (Category (Action (Type u_1) (MonCat.of (MulOpposite M)))) := sorry

Lean refused to accept the statement. I wrote:

import Mathlib
open CategoryTheory

variables {M : Type*} [Monoid M]

instance HasFiniteProducts (Category (Action (Type u_1) (MonCat.of (MulOpposite M)))) := sorry

And it complains

unexpected token '('; expected ')'

[Yiming Xu]

I believe my parentheses match up...

[Yaël Dillies]

You should replace instance HasFiniteProducts ... with instance : HasFiniteProducts ...

[Yiming Xu]

Thanks for the swift reply! And good point for mentioning the ":", this is not the first time I missed it...

Tried in web Lean. It is still complaining if I have:

import Mathlib
open CategoryTheory

variables {M : Type*} [Monoid M]

instance : HasFiniteProducts (Category (Action (Type u_1) (MonCat.of (MulOpposite M)) )) := sorry

[Yiming Xu]

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQEwCmAdnAMIoEDm0AngCqoG044BuSUwSW6BAznADeCOAC44dGoQBUAXzgBtBBCIRgAE0QBdFsCJ8YSIgGMCYuAAkkfAGJ7gMAgAUoEdQFdjMAQApyj6igaOB8AQS9gFRDJQjh3AH0ARgBKEOUifwA6CAAzNPd0AHkwSD4HMwRk1KqxAF4gA

[Edward van de Meent]

use set_option autoImplicit false

[Yaël Dillies]

You don't have to copy-paste the link to the playground :wink: If you hover over a code block on Zulip, you will see
image.png

[Edward van de Meent]

looking at docs#CategoryTheory.Limits.HasFiniteProducts , it seems you're missing an open Limits

[Yiming Xu]

Edward van de Meent said:

use set_option autoImplicit false

Let me try.

[Yiming Xu]

Yaël Dillies said:

You don't have to copy-paste the link to the playground :wink: If you hover over a code block on Zulip, you will see
image.png

Wow that's good to know!

[Edward van de Meent]

additionally, you don't need the Category inside the HasFiniteProducts

[Yiming Xu]

Edward van de Meent said:

looking at docs#CategoryTheory.Limits.HasFiniteProducts , it seems you're missing an open Limits

Still complaining.

import Mathlib
open CategoryTheory
open Limits
set_option autoImplicit false
variables {M : Type*} [Monoid M]

instance : HasFiniteProducts (Category (Action (Type u_1) (MonCat.of (MulOpposite M)) )) := sorry

BTW Limits live in CategoryTheory, so I assume if I open CategoryTheory, then I open everything there. Is that wrong?

[Edward van de Meent]

that is indeed wrong. Limits is a namespace inside the CategoryTheory namespace

[Yiming Xu]

Edward van de Meent said:

looking at docs#CategoryTheory.Limits.HasFiniteProducts , it seems you're missing an open Limits

Oh this takes me back to the world of love and peace. Silly me. Lean is happy now.

[Yiming Xu]

Edward van de Meent said:

that is indeed wrong. Limits is a namespace inside the CategoryTheory namespace

So, once we have nested namespace, we need to open them layer by layer?

[Yiming Xu]

I tried. Discovered that I cannot delete any line of:

open CategoryTheory
open Limits

[Edward van de Meent]

you can smush them together tho: open CategoryTheory Limits

[Yiming Xu]

Tried! Thanks. And the order matters. Have to do it like opening a Matryoshka.