Product of Group Actions

Stream: general

[Yiming Xu]

I want to prove the category of right actions of a monoid M has exponentials. I wrote:

import Mathlib

import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.CategoryTheory.SingleObj
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
import Mathlib.CategoryTheory.Limits.Preserves.Basic
import Mathlib.CategoryTheory.Adjunction.Limits
import Mathlib.CategoryTheory.Conj
set_option autoImplicit false
set_option diagnostics true
open CategoryTheory Limits

universe u
variable {M : Type u} [Monoid M]



/-
Plan:
Start with (A : Action (Type u) (MonCat.of (MulOpposite M)))
construct the action A × M
construct the set of equivariant maps A × M → B, for any
(B : Action (Type u) (MonCat.of (MulOpposite M)))
then bundle these maps as a type.

construct an action of M on this type, make it an M action

use Action.ofMulAction.
-/


instance AtoB (A: Action (Type u) (MonCat.of (MulOpposite M)))
         (B: Action (Type u) (MonCat.of (MulOpposite M))):
Action (Type u) (MonCat.of (MulOpposite M)) :=
{V :=  (Action.Hom (A × M) B) }

Lean complains by adding a red underscore under "V := (Action.Hom (A × M) B)", and says:

application type mismatch
  Prod A
argument
  A
has type
  Action (Type u) (MonCat.of Mᵐᵒᵖ) : Type (u + 1)
but is expected to have type
  Type ?u.1041 : Type (?u.1041 + 1)

Seems to be a universe problem. May I please ask for the reason and how to fix that? Thanks!

[Eric Wieser]

This doesn't look like a universe problem to me, the issue is that × works on Type not Action _ _

[Yiming Xu]

But as Actions has products, as I can have instance:

instance : HasFiniteProducts ((Action (Type u) (MonCat.of (MulOpposite M)))) := inferInstance

The product should work as well I think? Or am I naive?

[Yiming Xu]

How should I construct product action then? And how can I check if the notion of product of actions is what I need? i.e. componentwise?

[Edward van de Meent]

i imagine you can choose a product using HasFiniteProducts.out 2 ...?

[Yiming Xu]

Thanks for brining up this issue! I went to talk to colleagues and got the problem solved.

What is happening here is that:
1.My notation is wrong: it should be \otimes or \ox, instead of \times, for monoidal products.
2.I should open MonoidalCategory to get it work.

So in this case the error message is not helpful. Now the following works.

import Mathlib

import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.CategoryTheory.SingleObj
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
import Mathlib.CategoryTheory.Limits.Preserves.Basic
import Mathlib.CategoryTheory.Adjunction.Limits
import Mathlib.CategoryTheory.Conj
set_option autoImplicit false
set_option diagnostics true
open CategoryTheory Limits
open MonoidalCategory
universe u
variable {M : Type u} [Monoid M]


instance : Category (Action (Type u) (MonCat.of (MulOpposite M))) := inferInstance
#synth HasFiniteProducts ((Action (Type u) (MonCat.of (MulOpposite M))))
instance : HasFiniteProducts ((Action (Type u) (MonCat.of (MulOpposite M)))) := inferInstance


/-
Start with (A : Action (Type u) (MonCat.of (MulOpposite M)))
construct the action A × M
construct the set of equivariant maps A × M → B, for any
(B : Action (Type u) (MonCat.of (MulOpposite M)))
then bundle these maps as a type.

construct an action of M on this type, make it an M action

use Action.ofMulAction.
-/

/-instance (A: Action (Type u) (MonCat.of (MulOpposite M)))
         (B: Action (Type u) (MonCat.of (MulOpposite M))):
   MulAction (MulOpposite M) (Action.Hom (A × M) B) := sorry-/

variables  (A: Action (Type u) (MonCat.of (MulOpposite M)))
           (B: Action (Type u) (MonCat.of (MulOpposite M)))
#check  (Action.leftRegular (MulOpposite M))
#check A
#check MulOpposite M
#check  (Action.leftRegular (MulOpposite M)) ⊗ A
#check (Action.Hom (A ⊗ (Action.leftRegular (MulOpposite M))) B)
instance AtoB (A: Action (Type u) (MonCat.of (MulOpposite M)))
         (B: Action (Type u) (MonCat.of (MulOpposite M))):
Action (Type u) (MonCat.of (MulOpposite M)) :=
{V :=  (Action.Hom (A ⊗ (Action.leftRegular (MulOpposite M))) B)
 ρ := sorry
}

[Yiming Xu]

As for the issue for chosen product, there is an instance saying that the forgetful functor from actions to sets reflects limits. That is saying the choice of product structure should be up to isomorphism. So the choice does not matter. It is still important to know, since HasFiniteProducts only gives the product, in which case you can still use \otimes, and Lean will choose a product for you. But ChosenFiniteProduct has the product encoded as a part of the structure.

[Johan Commelin]

As you can see, this requires you to write a lot of MonCat.of etc... If what you are doing is not directly category theoretic in nature, it might be smoother to work in the unbundled world.

[Yiming Xu]

Johan Commelin said:

As you can see, this requires you to write a lot of MonCat.of etc... If what you are doing is not directly category theoretic in nature, it might be smoother to work in the unbundled world.

Thanks for this suggestion, I am indeed considering this. Maybe one way of doing that would be working with the unbundled world first and search for "transporting" to the bundled world. I would appreciate if there is some existing work on how to do this kind of transfer uniformly.

[Johan Commelin]

Hmmz, I don't think we have a tutorial on that.
What exactly would you like to do with products of group actions?

[Yiming Xu]

Johan Commelin said:

Hmmz, I don't think we have a tutorial on that.
What exactly would you like to do with products of group actions?

Thanks so much for trying to help!

I want to prove the category of right actions of a monoid has exponentials. My aim in the recent weeks is to get myself familiarized with Lean and the category theory part of the library as well.

[Yiming Xu]

image.png

[Yiming Xu]

This is the exercise I am doing. I was originally only would like a practice. But since it is not in mathlib yet. It might be better if it can be made to connectable with Mathlib.

[Johan Commelin]

I see. So yes, I think it would be good to first do think in the language of monoids and actions without category theory.

[Johan Commelin]

So just use (M : Type*) [Monoid M] instead of (M : MonCat)

[Yiming Xu]

Johan Commelin said:

I see. So yes, I think it would be good to first do think in the language of monoids and actions without category theory.

Thanks! I will do it this way first. I do need to familiarize myself with the category theory library as well, but I can do it in parallel and try to put them together later.

[Yiming Xu]

Johan Commelin said:

I see. So yes, I think it would be good to first do think in the language of monoids and actions without category theory.

So I have defined the bijection and now to get access to the Lean definition of exponential, I am afraid that I do need to deal with MonCat. The exercise above uses a fixed finite product action, namely the pointwise one. But I failed to find out a precise definition of the product on (Action (Type u) (MonCat.of (MulOpposite M))). I can only get hat it has finite products.

instance : HasFiniteProducts (Action (Type u) (MonCat.of (MulOpposite M))) := inferInstance --fine

instance : ChosenFiniteProducts (Action (Type u) (MonCat.of (MulOpposite M))) := inferInstance --error

[Yiming Xu]

As products are unique up to isomorphism, it might be fine to construct an explicit product pointwisely, and then prove that it should be equivalent to the witness in HasFiniteProduct. But it would take a while to construct the product according to the definition, since the definition of product in Lean is in terms of limit. I will have to deal with the limit cone, like this...:

instance (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y : Action (Type u) (MonCat.of (MulOpposite M))):
         Limits.LimitCone (Limits.pair X Y) where
           cone := {
             pt := PairwiseAction X Y
             π := {
               app := fun
                 | .mk as =>
                    match as with
                    | WalkingPair.left => {
                      hom := fun
                        | .mk fst snd => fst
                    }
                    | WalkingPair.right => {
                      hom := fun
                        | .mk fst snd => snd
                    }
               naturality := by
                simp
                intros l r f
                ext p
                dsimp [PairwiseV_def' X Y] at p
                --rw [PairwiseV_def' X Y] at p
                --rw [show ((PairwiseAction X Y).V = (X.V × Y.V)) by rfl] at p
                --rw [PairwiseV_def X Y] at p
                cases' r with as
                cases' as
                simp
                cases' l with as
                cases' as
                · dsimp
              -- have a : f = 𝟙 ({ as := WalkingPair.left }: Discrete WalkingPair) := rfl
                  have a : f = 𝟙 (Discrete.mk WalkingPair.left) := rfl
                  simp[a]
                · dsimp
                  nomatch f
                · cases' p with x y
                  cases' l with as
                  cases as
                  · nomatch f
                  · dsimp
                    have a : f = 𝟙 (Discrete.mk WalkingPair.right) := rfl
                    simp[a]
             }
           }
           isLimit := {
             lift := sorry
             fac := sorry
             uniq := sorry
           }

So does it seem like I have to do it that way?

[Yiming Xu]

I can indeed define the bijection, and prove the definition is indeed a bijection, purely in the unbundled world, like this:

import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.CategoryTheory.SingleObj
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
import Mathlib.CategoryTheory.Limits.Preserves.Basic
import Mathlib.CategoryTheory.Adjunction.Limits
import Mathlib.CategoryTheory.Conj
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

--TODO maybe creat a class RSMul, for right action,and prove that
--for each left action, the property for the right action

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



def OntoFun {X : Type*} {Y:Type*} (k : MulOpposite M) (e : M × X → Y) : M × X → Y :=
  fun (g,x) => e ((unop k) * g, x)

theorem OntoFun_def (k : MulOpposite M) (e : M × X → Y) :
 OntoFun M k e = fun (g,x) ↦ e ( (unop k) * g, x) :=by rfl

instance EquivariantMaps.SMul (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]:
  SMul (MulOpposite M) (EquivariantMaps (MulOpposite M) (M × X) Y) where
 smul k e := {
   toFun := OntoFun M k e.toFun
   comm_square := by
     intros p opm
     cases' p with m x
     simp
     simp[OntoFun_def]
     simp [e.comm_square (unop k * m, x) opm]
     simp[mul_assoc]
 }

theorem smul_EquivariantMaps
 (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (k: MulOpposite M) (e : EquivariantMaps (MulOpposite M) (M × X) Y) (g : M) (x : X):
 (k • e).toFun (g,x) = e.toFun ( (unop k) * g, x) := rfl


instance (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y] :  MulAction (MulOpposite M) (EquivariantMaps (MulOpposite M) (M × X) Y)
 where
   smul k e := (EquivariantMaps.SMul M X Y).smul k e
   one_smul := by
     intros e
     ext ⟨g,x⟩
     simp[smul_EquivariantMaps]
   mul_smul := by
    intros k1 k2 e
    ext ⟨g,x⟩
    simp[smul_EquivariantMaps]
    simp[mul_assoc]


--Hom(Z×X,Y)∼=Hom(Z,Hom(M×X, Y )).

def ActionTransposefun (Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: Z × X → Y) (z : Z) : M × X → Y := fun
   | .mk m x => f ⟨op m • z, x⟩


theorem ActionTransposefun_def
 (Z : Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: Z × X → Y) (z : Z) (m : M) (x: X) :
 ActionTransposefun M Z X Y f z ⟨m,x⟩  = f ⟨op m • z, x⟩ := rfl

 def ActionTransposeEquivariantMap
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M) (Z × X) Y) (z : Z) :
 EquivariantMaps (MulOpposite M) (M × X) Y where
   toFun := ActionTransposefun M Z X Y f.toFun z
   comm_square := by
     intros mx mop
     cases' mx with m x
     simp
     simp[ActionTransposefun_def]
     simp[f.comm_square]
     simp[mul_smul] --how to invoke it on Z? I think I have an answer

theorem ActionTransposeEquivariantMap_toFun
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M) (Z × X) Y) (z : Z):
 (ActionTransposeEquivariantMap M Z X Y f z).toFun =
 ActionTransposefun M Z X Y f.toFun z := rfl


def ActionTransposeEquivariantMapHom
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M) (Z × X) Y):
 EquivariantMaps (MulOpposite M)
 Z
 (EquivariantMaps (MulOpposite M) (M × X) Y) where
   toFun z := ActionTransposeEquivariantMap M Z X Y f z
   comm_square := by
     intros z m
     simp
     ext ⟨m1,x⟩
     simp[smul_EquivariantMaps]
     simp[ActionTransposeEquivariantMap_toFun]
     simp[ActionTransposefun_def]
     simp[mul_smul]

theorem ActionTransposeEquivariantMapHom_toFun
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M) (Z × X) Y):
 (ActionTransposeEquivariantMapHom M Z X Y f).toFun =
 fun z => ActionTransposeEquivariantMap M Z X Y f z := rfl

 def ActionTransposefunr (Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: Z → EquivariantMaps (MulOpposite M) (M × X) Y) : Z × X → Y := fun
   | .mk z x => (f z).toFun ⟨ 1 , x⟩



theorem ActionTransposefunr_def
 (Z : Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: Z → EquivariantMaps (MulOpposite M) (M × X) Y) (z : Z) (x: X):
 ActionTransposefunr M Z X Y f ⟨ z,x⟩  = (f z).toFun ⟨1, x⟩ := rfl

theorem ActionTransposeEquivariantMapr_lemma
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M)
     Z (EquivariantMaps (MulOpposite M) (M × X) Y))
 (mop : Mᵐᵒᵖ) (z : Z) (x : X) :
 (f.toFun (mop • z)).toFun (1, x) =
              (f.toFun z).toFun (unop mop, x) := by
   have h0 : f.toFun (mop • z) = mop • f.toFun z := by
                   simp[f.comm_square]
   simp[h0]
   simp[smul_EquivariantMaps]

def ActionTransposeEquivariantMapr
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M)
     Z (EquivariantMaps (MulOpposite M) (M × X) Y)):
   EquivariantMaps (MulOpposite M) (Z × X) Y where
   toFun := ActionTransposefunr M Z X Y f.toFun
   comm_square := by
     intros zx mop
     cases' zx with z x
     simp
     simp[ActionTransposefunr_def]
     simp[(f.toFun z).comm_square]
     have a : (f.toFun (mop • z)).toFun (1, mop • x) =
              (f.toFun z).toFun (unop mop, mop • x) := by
              have h0 : f.toFun (mop • z) = mop • f.toFun z := by
                   simp[f.comm_square]
              simp[h0]
              simp[smul_EquivariantMaps]
     simp[a]

theorem ActionTransposeEquivariantMapr_toFun
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M)
     Z (EquivariantMaps (MulOpposite M) (M × X) Y)):
 (ActionTransposeEquivariantMapr M Z X Y f).toFun =
 ActionTransposefunr M Z X Y f.toFun := rfl

lemma ActionTransposeInverse
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M) (Z × X) Y):
 ActionTransposeEquivariantMapr M Z X Y
 (ActionTransposeEquivariantMapHom M Z X Y f) = f := by
 ext ⟨z,x⟩
 simp[ActionTransposeEquivariantMapr_toFun]
 simp[ActionTransposefunr_def]
 simp[ActionTransposeEquivariantMapHom_toFun]
 simp[ActionTransposeEquivariantMap_toFun]
 simp[ActionTransposefun_def]


lemma ActionTransposeInverse'
(Z:Type*) (X : Type*) (Y:Type*)
 [MulAction (MulOpposite M) Z]
 [MulAction (MulOpposite M) X]
 [MulAction (MulOpposite M) Y]
 (f: EquivariantMaps (MulOpposite M)
     Z (EquivariantMaps (MulOpposite M) (M × X) Y)):
  ActionTransposeEquivariantMapHom M Z X Y
   (ActionTransposeEquivariantMapr M Z X Y f) = f := by
   ext z mx
   cases' mx with m x
   simp[ActionTransposeEquivariantMapHom_toFun]
   simp[ActionTransposeEquivariantMap_toFun]
   simp[ActionTransposefun_def]
   simp[ActionTransposeEquivariantMapr_toFun]
   simp[ActionTransposefunr_def]
   simp[ActionTransposeEquivariantMapr_lemma]

[Yiming Xu]

The remaining is about the construction of adjoint functors and refers to the category library.

[Yiming Xu]

I think maybe one thing I can do is to define a product functor myself (instead of converting the existing product structure on MonCat into a functor of "taking product with"), and then construct the exponential functor, prove they are adjoints, and transfer along an isomorphism between "the product functor I defined" and "the product functor obtained via the instance HasFiniteProduct".

[Yiming Xu]

(This is just something I set up for myself to get used to the standard algebra library and the category theory library and connect concrete examples to the categorical world. The plan is to first do the algebra world, then deal with the functors to prove it is indeed an exponential in the categorical world. Then prove presheaf categories are Cartesian closed and see if it will imply the algebraic version...). If the middle step sounds very messy, I may try the presheaf stuff first as well.