Skip to content

Commit 3b5ca69

Browse files
robin-carlierrobin-carlier
committed
feat(CategoryTheory/Monoidal/Action): actions as monoidal functors to endofunctors (leanprover-community#25875)
Given a monoidal category `C` and a category `D`, we show that left actions of `C` on `D` correspond to monoidal functors `C ⥤ (D ⥤ D)ᴹᵒᵖ` by showing that the composition of `curriedAction C D` with `mopFunctor` is monoidal, and in the other direction by defining an action of `C` on `D` out of the data of such a monoidal functor. Similarly, we show that monoidal functors `C ⥤ (D ⥤ D)` correspond to right actions of `C` on `D`. We use this to define the "evaluation" right action of `(C ⥤ C)` (with the composition monoidal structure) on `C` as the action corresponding to the identity functor `(C ⥤ C) ⥤ (C ⥤ C)`.
1 parent 9c51fb9 commit 3b5ca69

4 files changed

Lines changed: 222 additions & 3 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2526,6 +2526,7 @@ import Mathlib.CategoryTheory.Monad.Monadicity
25262526
import Mathlib.CategoryTheory.Monad.Products
25272527
import Mathlib.CategoryTheory.Monad.Types
25282528
import Mathlib.CategoryTheory.Monoidal.Action.Basic
2529+
import Mathlib.CategoryTheory.Monoidal.Action.End
25292530
import Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
25302531
import Mathlib.CategoryTheory.Monoidal.Action.Opposites
25312532
import Mathlib.CategoryTheory.Monoidal.Bimod

‎Mathlib/CategoryTheory/Monoidal/Action/Basic.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,6 @@ on `d` is `d ⊙ᵣ c`, and the structure isomorphisms are of the form
2727
## TODOs/Projects
2828
* Equivalence between actions of `C` on `D` and pseudofunctors from the
2929
classifying bicategory of `C` to `Cat`.
30-
* Left actions as monoidal functors C ⥤ (D ⥤ D)ᴹᵒᵖ.
31-
* Right actions as monoidal functors C ⥤ D ⥤ D.
32-
* (Right) Action of `(C ⥤ C)` on `C`.
3330
* Left/Right Modules in `D` over a monoid object in `C`.
3431
Equivalence with `Mod_` when `D` is `C`. Bimodules objects.
3532
* Given a monad `M` on `C`, equivalence between `Algebra M`, and modules in `C`

‎Mathlib/CategoryTheory/Monoidal/Action/End.lean‎

Lines changed: 216 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,216 @@
1+
/-
2+
Copyright (c) 2025 Robin Carlier. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robin Carlier
5+
-/
6+
import Mathlib.CategoryTheory.Monoidal.Action.Basic
7+
import Mathlib.CategoryTheory.Monoidal.End
8+
import Mathlib.CategoryTheory.Monoidal.Opposite
9+
10+
/-! # Actions as monoidal functors to endofunctor categories
11+
12+
In this file, we show that given a right action of a monoidal category `C`
13+
on a category `D`, the curried action functor `C ⥤ D ⥤ D` is monoidal.
14+
Conversely, given a monoidal functor `C ⥤ D ⥤ D`, we can define a right action
15+
of `C` on `D`.
16+
17+
The corresponding results are also available for left actions: given a left
18+
action of `C` on `D`, composing
19+
`CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D` with
20+
`CategoryTheory.MonoidalCategory.MonoidalOpposite.mopFunctor (D ⥤ D)` is
21+
monoidal, and conversely one can define a left action of `C` on `D` from a monoidal
22+
functor `C ⥤ (D ⥤ D)ᴹᵒᵖ`.
23+
24+
-/
25+
26+
namespace CategoryTheory.MonoidalCategory
27+
28+
variable (C D : Type*)
29+
30+
variable [Category C] [MonoidalCategory C] [Category D]
31+
32+
attribute [local instance] endofunctorMonoidalCategory
33+
34+
attribute [local aesop safe apply (rule_sets := [CategoryTheory])]
35+
MonoidalOpposite.hom_ext
36+
37+
namespace MonoidalLeftAction
38+
39+
section
40+
41+
variable [MonoidalLeftAction C D]
42+
/-- A variant of
43+
`CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction`
44+
that takes value in the monoidal opposite of `D ⥤ D`. -/
45+
@[simps! obj_unmop_obj obj_unmop_map]
46+
def curriedActionMop : C ⥤ (D ⥤ D)ᴹᵒᵖ :=
47+
(curriedAction C D) ⋙ mopFunctor _
48+
49+
-- This simp lemma is necessary because the simps projection generated for
50+
-- unmop of a morphism is actually its underlying unmop field, rather than
51+
-- the application of `Quiver.Hom.unmop`.
52+
variable {C D} in
53+
@[simp]
54+
lemma curriedActionMop_map_unmop_app {c c' : C} (f : c ⟶ c') (d : D) :
55+
((curriedActionMop C D).map f).unmop.app d = f ⊵ₗ d :=
56+
rfl
57+
58+
open MonoidalOpposite in
59+
/-- When `C` acts on the left on `D`, the functor
60+
`curriedActionMop : C ⥤ (D ⥤ D)ᴹᵒᵖ` is monoidal, where `D ⥤ D` has the
61+
composition monoidal structure. -/
62+
@[simps!]
63+
instance curriedActionMopMonoidal : (curriedActionMop C D).Monoidal where
64+
ε := .mop <| (actionUnitNatIso C D).inv
65+
μ _ _ := .mop <| {app _ := αₗ _ _ _|>.inv}
66+
δ _ _ := .mop <| {app _ := αₗ _ _ _|>.hom}
67+
η := .mop <| (actionUnitNatIso C D).hom
68+
associativity c₁ c₂ c₃ := by
69+
apply (mopEquiv (D ⥤ D)).fullyFaithfulInverse.map_injective
70+
ext d
71+
simpa [-associator_actionHom] using
72+
(IsIso.inv_eq_inv.mpr <| associator_actionHom c₁ c₂ c₃ d).symm =≫
73+
(α_ c₁ c₂ c₃).hom ⊵ₗ d
74+
oplax_right_unitality x := by
75+
apply MonoidalOpposite.hom_ext
76+
ext t
77+
simpa [-rightUnitor_actionHom] using
78+
(ρ_ x).inv ⊵ₗ t ≫= rightUnitor_actionHom x t
79+
oplax_left_unitality x := by
80+
apply MonoidalOpposite.hom_ext
81+
ext t
82+
simpa [-leftUnitor_actionHom] using
83+
(λ_ x).inv ⊵ₗ t ≫= leftUnitor_actionHom x t
84+
85+
end
86+
87+
variable {C D}
88+
89+
/-- A monoidal functor `F : C ⥤ (D ⥤ D)ᴹᵒᵖ` can be thought of as a left action
90+
of `C` on `D`. -/
91+
@[simps!]
92+
def actionOfMonoidalFunctorToEndofunctorMop (F : C ⥤ (D ⥤ D)ᴹᵒᵖ) [F.Monoidal] :
93+
MonoidalLeftAction C D where
94+
actionObj c d := (F.obj c).unmop.obj d
95+
actionHomLeft f d := (F.map f).unmop.app d
96+
actionHomRight c _ _ f := (F.obj c).unmop.map f
97+
actionAssocIso c c' d := Functor.Monoidal.μIso F c c'|>.unmop.app d|>.symm
98+
actionUnitIso d := Functor.Monoidal.εIso F|>.unmop.app d|>.symm
99+
actionAssocIso_hom_naturality {c₁ c₁' c₂ c₂' c₃ c₃'} f g h := by
100+
have e := congrArg (fun t ↦ t.unmop.app c₃) <|
101+
Functor.OplaxMonoidal.δ_natural F f g
102+
dsimp at e
103+
simp [reassoc_of% e]
104+
whiskerRight_actionHomLeft {x y} c f d := by
105+
have e := congrArg (fun t ↦ t.unmop.app d) <|
106+
Functor.LaxMonoidal.μ_natural_left F f c
107+
dsimp at e
108+
simp [e, ← NatTrans.comp_app, ← unmop_comp]
109+
whiskerLeft_actionHomLeft c {x y} f d := by
110+
have e := congrArg (fun t ↦ t.unmop.app d) <|
111+
Functor.LaxMonoidal.μ_natural_right F c f
112+
dsimp at e
113+
simp [e, ← NatTrans.comp_app, ← unmop_comp]
114+
associator_actionHom c₁ c₂ c₃ d := by
115+
have e := congrArg (fun t ↦ t.unmop.app d) <|
116+
Functor.OplaxMonoidal.associativity F c₁ c₂ c₃
117+
dsimp at e
118+
simp only [Category.comp_id] at e
119+
simp [e]
120+
leftUnitor_actionHom c d := by
121+
have e := (F.map (λ_ c).hom).unmop.app d ≫=
122+
(congrArg (fun t ↦ t.unmop.app d) <|
123+
Functor.OplaxMonoidal.left_unitality F c)
124+
dsimp at e
125+
simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
126+
← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e
127+
simp [e]
128+
rightUnitor_actionHom c d := by
129+
have e := (F.map (ρ_ c).hom).unmop.app d ≫=
130+
(congrArg (fun t ↦ t.unmop.app d) <|
131+
Functor.OplaxMonoidal.right_unitality F c)
132+
dsimp at e
133+
simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
134+
← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e
135+
simp [e]
136+
137+
/-- If the (left) action of `C` on `D` comes from a monoidal functor
138+
`C ⥤ (D ⥤ D)ᴹᵒᵖ`, then `curriedActionMop C D` is naturally isomorphic to that
139+
functor. -/
140+
@[simps!]
141+
def curriedActionActionOfMonoidalFunctorToEndofunctorMopIso
142+
(F : C ⥤ (D ⥤ D)ᴹᵒᵖ) [F.Monoidal] :
143+
letI := actionOfMonoidalFunctorToEndofunctorMop F
144+
curriedActionMop C D ≅ F :=
145+
.refl _
146+
147+
end MonoidalLeftAction
148+
149+
namespace MonoidalRightAction
150+
151+
variable {C D}
152+
153+
open MonoidalOpposite in
154+
/-- When `C` acts on the right on `D`, the functor `curriedAction : C ⥤ (D ⥤ D)`
155+
is monoidal, where `D ⥤ D` has the composition monoidal structure. -/
156+
@[simps!]
157+
instance curriedActionMonoidal [MonoidalRightAction C D] :
158+
(curriedAction C D).Monoidal where
159+
ε := (actionUnitNatIso C D).inv
160+
μ _ _ := {app _ := αᵣ _ _ _|>.inv}
161+
δ _ _ := {app _ := αᵣ _ _ _|>.hom}
162+
η := (actionUnitNatIso C D).hom
163+
associativity c₁ c₂ c₃ := by
164+
ext d
165+
simpa [-actionHom_associator] using
166+
(IsIso.inv_eq_inv.mpr <| actionHom_associator c₁ c₂ c₃ d).symm =≫
167+
d ⊴ᵣ (α_ c₁ c₂ c₃).hom
168+
oplax_right_unitality x := by
169+
ext t
170+
simpa [-actionHom_rightUnitor] using
171+
t ⊴ᵣ (ρ_ x).inv ≫= actionHom_rightUnitor x t
172+
oplax_left_unitality x := by
173+
ext t
174+
simpa [-actionHom_leftUnitor] using
175+
t ⊴ᵣ (λ_ x).inv ≫= actionHom_leftUnitor x t
176+
177+
/-- A monoidal functor `F : C ⥤ D ⥤ D` can be thought of as a right action
178+
of `C` on `D`. -/
179+
@[simps!]
180+
def actionOfMonoidalFunctorToEndofunctor (F : C ⥤ D ⥤ D) [F.Monoidal] :
181+
MonoidalRightAction C D where
182+
actionObj d c := (F.obj c).obj d
183+
actionHomLeft f c := (F.obj c).map f
184+
actionHomRight d _ _ f := (F.map f).app d
185+
actionAssocIso d c c' := Functor.Monoidal.μIso F c c'|>.app d|>.symm
186+
actionUnitIso d := Functor.Monoidal.εIso F|>.app d|>.symm
187+
actionAssocIso_hom_naturality {c₁ c₁' c₂ c₂' c₃ c₃'} f g h := by
188+
have e := congrArg (fun t ↦ t.app c₁) <|
189+
Functor.OplaxMonoidal.δ_natural F g h
190+
dsimp at e
191+
simp [reassoc_of% e]
192+
193+
/-- If the action of `C` on `D` comes from a monoidal functor `C ⥤ (D ⥤ D)`,
194+
then `curriedActionMop C D` is naturally isomorphic to that functor. -/
195+
@[simps!]
196+
def curriedActionActionOfMonoidalFunctorToEndofunctorIso
197+
(F : C ⥤ (D ⥤ D)) [F.Monoidal] :
198+
letI := actionOfMonoidalFunctorToEndofunctor F
199+
curriedAction C D ≅ F :=
200+
.refl _
201+
202+
end MonoidalRightAction
203+
204+
namespace endofunctorMonoidalCategory
205+
/-- Functor evaluation gives a right action of `C ⥤ C`.
206+
207+
Note that in the literature, this is defined as a left action, but mathlib's
208+
monoidal structure on `C ⥤ C` is the monoidal opposite of the one usually
209+
considered in the literature. -/
210+
@[simps! actionObj actionHomLeft actionHomRight actionAssocIso actionUnitIso]
211+
scoped instance evaluationRightAction : MonoidalRightAction (C ⥤ C) C :=
212+
MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor (𝟭 (C ⥤ C))
213+
214+
end endofunctorMonoidalCategory
215+
216+
end CategoryTheory.MonoidalCategory

‎Mathlib/CategoryTheory/Monoidal/Opposite.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,11 @@ theorem unmop_id_mop {X : C} : (𝟙 (mop X)).unmop = 𝟙 X := rfl
113113
@[simp]
114114
theorem mop_id_unmop {X : Cᴹᵒᵖ} : (𝟙 (unmop X)).mop = 𝟙 X := rfl
115115

116+
-- aesop prefers this lemma as a safe apply over Quiver.Hom.unmop_inj
117+
lemma MonoidalOpposite.hom_ext {x y : Cᴹᵒᵖ} {f g : x ⟶ y} (h : f.unmop = g.unmop) :
118+
f = g :=
119+
Quiver.Hom.unmop_inj h
120+
116121
variable (C)
117122

118123
/-- The identity functor on `C`, viewed as a functor from `C` to its monoidal opposite. -/

0 commit comments

Comments
 (0)