Equivariant functors as strong transformations

Let a monoid M act on categories C and D, that is, let Discrete M act on the left on both. A functor F : C ⥤ D is equivariant when it is left-linear for these actions in the sense of Mathlib's Functor.LeftLinear: it carries isomorphisms F (g ⊙ₗ X) ≅ g ⊙ₗ F X compatible with the unitors and associators of the two actions. Equivalently, it carries natural isomorphisms actionLeft C g ⋙ F ≅ F ⋙ actionLeft D g satisfying the unit and product diagrams; this is Functor.commActionLeftIso, defined for an arbitrary monoidal category acting.

The actions correspond to the pseudofunctors pseudofunctor M C and pseudofunctor M D out of LocallyDiscrete (SingleObj M), and this file shows that equivariant functors are exactly the strong transformations between these pseudofunctors.

• MonoidalLeftAction.strongTrans M F is the strong transformation with component F whose naturality isomorphism at g comes from F.commActionLeftIso ⟨g⟩: its components are the oplax lineators δₗ F ⟨g⟩ X : F (g ⊙ₗ X) ⟶ g ⊙ₗ F X. The unit and composition axioms of a strong transformation are the unitality and associativity of these lineators.
• Conversely MonoidalLeftAction.functorOfStrongTrans η is the component of a strong transformation η at the unique object, and it is left-linear with lineators the components of the naturality isomorphisms of η.
• MonoidalLeftAction.strongTransEquiv packages the two constructions as an equivalence between functors equipped with a left-linear structure and strong transformations. Both round trips hold definitionally, so the comparison keeps the lineators, and not only the functor.

The order conventions are those of MonoidalLeftAction.pseudofunctor: the composite g ≫ h in SingleObj M is the product h * g, which acts by actionLeft C g ⋙ actionLeft C h.

def CategoryTheory.Functor.commActionLeftIso {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} {D' : Type u_3} [Category.{v_2, u_2} D] [Category.{v_3, u_3} D'] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] (F : Functor D D') [F.LeftLinear C] (c : C) : (MonoidalCategory.MonoidalLeftAction.actionLeft D c).comp F ≅ F.comp (MonoidalCategory.MonoidalLeftAction.actionLeft D' c)

A left-linear functor commutes with the action functors: the natural isomorphism actionLeft D c ⋙ F ≅ F ⋙ actionLeft D' c whose components are the oplax lineators δₗ F c X : F (c ⊙ₗ X) ⟶ c ⊙ₗ F X, with inverse the lax lineators μₗ F c X.

@[simp]

theorem CategoryTheory.Functor.commActionLeftIso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} {D' : Type u_3} [Category.{v_2, u_2} D] [Category.{v_3, u_3} D'] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] (F : Functor D D') [F.LeftLinear C] (c : C) (X : D) : (F.commActionLeftIso c).hom.app X = OplaxLeftLinear.δₗ F c X

@[simp]

theorem CategoryTheory.Functor.commActionLeftIso_inv_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} {D' : Type u_3} [Category.{v_2, u_2} D] [Category.{v_3, u_3} D'] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] (F : Functor D D') [F.LeftLinear C] (c : C) (X : D) : (F.commActionLeftIso c).inv.app X = LaxLeftLinear.μₗ F c X

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : Functor C D) [F.LeftLinear (Discrete M)] : (pseudofunctor M C).StrongTrans (pseudofunctor M D)

A functor that is left-linear for actions of a monoid M on C and on D is a strong transformation pseudofunctor M C ⟶ pseudofunctor M D. Its component at the unique object is F, and its naturality isomorphism at g is the 2-isomorphism of Cat given by F.commActionLeftIso ⟨g⟩ : actionLeft C ⟨g⟩ ⋙ F ≅ F ⋙ actionLeft D ⟨g⟩.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans_app (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : Functor C D) [F.LeftLinear (Discrete M)] (a : LocallyDiscrete (SingleObj M)) : (strongTrans M F).app a = F.toCatHom

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans_naturality_hom_toNatTrans_app (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : Functor C D) [F.LeftLinear (Discrete M)] {a b : LocallyDiscrete (SingleObj M)} (g : a ⟶ b) (X : C) : ((strongTrans M F).naturality g).hom.toNatTrans.app X = Functor.OplaxLeftLinear.δₗ F { as := g.as } X

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans_naturality_inv_toNatTrans_app (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : Functor C D) [F.LeftLinear (Discrete M)] {a b : LocallyDiscrete (SingleObj M)} (g : a ⟶ b) (X : C) : ((strongTrans M F).naturality g).inv.toNatTrans.app X = Functor.LaxLeftLinear.μₗ F { as := g.as } X

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.functorOfStrongTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (η : (pseudofunctor M C).StrongTrans (pseudofunctor M D)) : Functor C D

The functor C ⥤ D underlying a strong transformation η : pseudofunctor M C ⟶ pseudofunctor M D: its component at the unique object.

@[instance_reducible]

instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftLinearFunctorOfStrongTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (η : (pseudofunctor M C).StrongTrans (pseudofunctor M D)) : (functorOfStrongTrans η).LeftLinear (Discrete M)

The functor underlying a strong transformation η : pseudofunctor M C ⟶ pseudofunctor M D is left-linear: its oplax lineator δₗ _ c X is the component at X of the naturality isomorphism of η at c, and its lax lineator is the inverse. The unitality and associativity of the lineators are the unit and composition axioms of η.

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.functorOfStrongTrans_δₗ {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (η : (pseudofunctor M C).StrongTrans (pseudofunctor M D)) (c : Discrete M) (X : C) : Functor.OplaxLeftLinear.δₗ (functorOfStrongTrans η) c X = (η.naturality c).hom.toNatTrans.app X

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.functorOfStrongTrans_μₗ {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (η : (pseudofunctor M C).StrongTrans (pseudofunctor M D)) (c : Discrete M) (X : C) : Functor.LaxLeftLinear.μₗ (functorOfStrongTrans η) c X = (η.naturality c).inv.toNatTrans.app X

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.functorOfStrongTrans_strongTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : Functor C D) [F.LeftLinear (Discrete M)] : functorOfStrongTrans (strongTrans M F) = F

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftLinearFunctorOfStrongTrans_strongTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : Functor C D) [inst : F.LeftLinear (Discrete M)] : leftLinearFunctorOfStrongTrans (strongTrans M F) = inst

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans_functorOfStrongTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (η : (pseudofunctor M C).StrongTrans (pseudofunctor M D)) : strongTrans M (functorOfStrongTrans η) = η

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv (M : Type u) [Monoid M] (C D : Type w) [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] : (F : Functor C D) × F.LeftLinear (Discrete M) ≃ (pseudofunctor M C).StrongTrans (pseudofunctor M D)

Equivariant functors are the strong transformations between the pseudofunctors attached to the actions: functors C ⥤ D equipped with a left-linear structure for the actions of Discrete M correspond to strong transformations pseudofunctor M C ⟶ pseudofunctor M D. The correspondence keeps the lineators: the naturality isomorphisms of strongTrans M F have components the lineators of F.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv_apply {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F : (F : Functor C D) × F.LeftLinear (Discrete M)) : (strongTransEquiv M C D) F = strongTrans M F.fst

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv_symm_apply {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (η : (pseudofunctor M C).StrongTrans (pseudofunctor M D)) : (strongTransEquiv M C D).symm η = ⟨functorOfStrongTrans η, leftLinearFunctorOfStrongTrans η⟩