Transporting internal actions by lax monoidal functors

A lax monoidal functor carries an action of a monoid object to an action of the image monoid object. The action map is the tensorator followed by the image of the original action. Equivariant morphisms remain equivariant. This applies, in particular, to passing from algebra coactions to actions on affine schemes by a monoidal spectrum functor.

The construction follows Mathlib's CategoryTheory.Functor.monObjObj, using the same tensorator and coherence identities.

@[instance_reducible]

def CategoryTheory.Functor.modObjObj {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (M X : C) [MonObj M] [ModObj M X] : ModObj (F.obj M) (F.obj X)

A lax monoidal functor transports an internal action to an action of the image monoid.

Equations

• F.modObjObj M X = { smul := CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F M X) (F.map CategoryTheory.ModObj.smul), one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem CategoryTheory.Functor.modObjObj_smul {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (M X : C) [MonObj M] [ModObj M X] : ModObj.smul = CategoryStruct.comp (LaxMonoidal.μ F M X) (F.map ModObj.smul)

The transported action is the tensorator followed by the image of the action.

theorem CategoryTheory.Functor.modObjObj_isModHom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (M : C) {X : C} [MonObj M] [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] : IsModHom (F.obj M) (F.map f)

A lax monoidal functor transports equivariant morphisms to equivariant morphisms.