Monoid actions on categories as pseudofunctors #
A monoid M acts on a category C in the categorical sense when we are given a left action
MonoidalLeftAction (Discrete M) C of the discrete monoidal category on M. Equivalently, such
an action is a pseudofunctor LocallyDiscrete (SingleObj M) ⥤ᵖ Cat out of the one-object
bicategory of M whose value at the unique object is C. This file constructs both directions
of this comparison and shows that they are mutually inverse. It is the case of a discrete
monoidal category of the comparison between actions and pseudofunctors listed as a TODO in
Mathlib.CategoryTheory.Monoidal.Action.Basic.
Composition order: in SingleObj M the composite g ≫ h is the product h * g, while a left
action satisfies T (h * g) ≅ T g ⋙ T h. Thus the pseudofunctor sends g to the action
functor actionLeft C ⟨g⟩, its unit comparison is λₗ, and its composition comparison at
g ≫ h has components αₗ ⟨h⟩ ⟨g⟩ X : (h * g) ⊙ₗ X ≅ h ⊙ₗ g ⊙ₗ X. The coherence of the
pseudofunctor is exactly the associativity and unit axioms of the action, and conversely.
Main declarations #
CategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctor: the pseudofunctorLocallyDiscrete (SingleObj M) ⥤ᵖ Catattached to an action ofDiscrete MonC;CategoryTheory.Pseudofunctor.monoidalLeftAction: conversely, the action ofDiscrete Mon the value of a pseudofunctorLocallyDiscrete (SingleObj M) ⥤ᵖ Catat the unique object, whose associator and unitor are given by the composition and unit comparisons of the pseudofunctor;CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalLeftAction_pseudofunctor: the action recovered frompseudofunctor M Cis the original action, including its associator and unitor;CategoryTheory.Pseudofunctor.pseudofunctor_monoidalLeftAction: conversely, the pseudofunctor recovered fromF.monoidalLeftActionisF, including its unit and composition comparisons;CategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctorEquiv: the resulting bijection between categories equipped with a left action ofDiscrete Mand pseudofunctorsLocallyDiscrete (SingleObj M) ⥤ᵖ Cat;TauCeti.trivialAction M D: the trivial action ofMon a categoryD, as a pseudofunctor with identity action functors and identity unit and composition comparisons.
The pseudofunctor LocallyDiscrete (SingleObj M) ⥤ᵖ Cat attached to a left action of
Discrete M on C. It sends the unique object to C and g to actionLeft C ⟨g⟩; its unit
comparison is λₗ and its composition comparison at g ≫ h (that is, at h * g) has
components αₗ ⟨h⟩ ⟨g⟩.
Instances For
The left action of Discrete M on the value of a pseudofunctor
F : LocallyDiscrete (SingleObj M) ⥤ᵖ Cat at the unique object. The action functor of c is
F.map c, the associator αₗ c c' has components those of F.mapComp c' c, and the unitor
λₗ has components those of F.mapId.
Instances For
The action of Discrete M recovered from the pseudofunctor pseudofunctor M C is the
original action: the comparison transports the action functors, the associator and the unitor
unchanged.
The pseudofunctor recovered from the action F.monoidalLeftAction is F itself: the
comparison transports the action functors, the unit comparison and the composition comparison
unchanged.
Left actions of Discrete M on categories correspond bijectively to pseudofunctors
LocallyDiscrete (SingleObj M) ⥤ᵖ Cat: an action on C is sent to pseudofunctor M C, and a
pseudofunctor F to the action F.monoidalLeftAction on its value at the unique object.
Instances For
The trivial categorical action of a monoid M on a category D, as a pseudofunctor
LocallyDiscrete (SingleObj M) ⥤ᵖ Cat: every element of M acts by the identity functor, and
the unit and composition comparisons are identities.