Structure maps of modules for Day convolution

For monoidal categories C and V, the action of a monoid M in C ⊛⥤ V on a module X restricts along the Day convolution units to natural maps M p ⊗ X q ⟶ X (p ⊗ q). A morphism of Day functors is a module morphism exactly when it commutes with these structure maps, by the universal property of Day convolution.

When M comes from a lax monoidal functor through DayFunctor.monObj, its unit and tensorator give the unit and iteration laws of the structure maps. For the sphere symmetric sequence these are the equivariant iterated structure maps of a symmetric spectrum.

The proofs restrict Mathlib's internal-module laws along the units of the Day convolution constructed by Robin Carlier, using the computation and extensionality lemmas in TauCeti.CategoryTheory.Monoidal.DayConvolution.Basic.

Main definitions

• Mod.dayStructureMap: the levelwise action of a Day convolution module.
• Mod.dayHomMk: construct a module morphism from compatibility with the structure maps.

Main statements

• Mod.dayStructureMap_naturality: naturality in both variables.
• Mod.dayStructureMap_hom, Mod.isModHom_iff_dayStructureMap: the structure-map criterion for module morphisms.
• Mod.dayStructureMap_unit, Mod.dayStructureMap_assoc: the unit and iteration laws for modules over the monoid of a lax monoidal functor.

References

• B. Day, On closed categories of functors, Reports of the Midwest Category Seminar IV, Lecture Notes in Math. 137 (1970), 1-38.
• M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 2.2.

noncomputable def CategoryTheory.Mod.dayStructureMap {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] (X : Mod (MonoidalCategory.DayFunctor C V) M) (p q : C) : MonoidalCategoryStruct.tensorObj (M.functor.obj p) (X.X.functor.obj q) ⟶ X.X.functor.obj (MonoidalCategoryStruct.tensorObj p q)

The levelwise action M p ⊗ X q ⟶ X (p ⊗ q), obtained by restricting the module action along the Day convolution unit.

theorem CategoryTheory.Mod.dayStructureMap_def {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] (X : Mod (MonoidalCategory.DayFunctor C V) M) (p q : C) : X.dayStructureMap p q = CategoryStruct.comp ((M.η X.X).app (p, q)) (ModObj.smul.natTrans.app (MonoidalCategoryStruct.tensorObj p q))

The structure maps restrict the module action along the Day convolution units.

theorem CategoryTheory.Mod.dayStructureMap_naturality {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] (X : Mod (MonoidalCategory.DayFunctor C V) M) {p p' q q' : C} (f : p ⟶ p') (g : q ⟶ q') : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (M.functor.map f) (X.X.functor.map g)) (X.dayStructureMap p' q') = CategoryStruct.comp (X.dayStructureMap p q) (X.X.functor.map (MonoidalCategoryStruct.tensorHom f g))

Naturality of the structure maps in both variables.

theorem CategoryTheory.Mod.dayStructureMap_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] (X : Mod (MonoidalCategory.DayFunctor C V) M) {p p' q q' : C} (f : p ⟶ p') (g : q ⟶ q') {Z : V} (h : X.X.functor.obj (MonoidalCategoryStruct.tensorObj p' q') ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (M.functor.map f) (X.X.functor.map g)) (CategoryStruct.comp (X.dayStructureMap p' q') h) = CategoryStruct.comp (X.dayStructureMap p q) (CategoryStruct.comp (X.X.functor.map (MonoidalCategoryStruct.tensorHom f g)) h)

Naturality of the structure maps in both variables.

@[simp]

theorem CategoryTheory.Mod.dayStructureMap_hom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] {X Y : Mod (MonoidalCategory.DayFunctor C V) M} (f : X ⟶ Y) (p q : C) : CategoryStruct.comp (X.dayStructureMap p q) (f.hom.natTrans.app (MonoidalCategoryStruct.tensorObj p q)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (M.functor.obj p) (f.hom.natTrans.app q)) (Y.dayStructureMap p q)

Every module morphism commutes with the structure maps.

@[simp]

theorem CategoryTheory.Mod.dayStructureMap_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] {X Y : Mod (MonoidalCategory.DayFunctor C V) M} (f : X ⟶ Y) (p q : C) {Z : V} (h : Y.X.functor.obj (MonoidalCategoryStruct.tensorObj p q) ⟶ Z) : CategoryStruct.comp (X.dayStructureMap p q) (CategoryStruct.comp (f.hom.natTrans.app (MonoidalCategoryStruct.tensorObj p q)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (M.functor.obj p) (f.hom.natTrans.app q)) (CategoryStruct.comp (Y.dayStructureMap p q) h)

Every module morphism commutes with the structure maps.

theorem CategoryTheory.Mod.isModHom_iff_dayStructureMap {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] {X Y : Mod (MonoidalCategory.DayFunctor C V) M} (f : X.X ⟶ Y.X) : IsModHom M f ↔ ∀ (p q : C), CategoryStruct.comp (X.dayStructureMap p q) (f.natTrans.app (MonoidalCategoryStruct.tensorObj p q)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (M.functor.obj p) (f.natTrans.app q)) (Y.dayStructureMap p q)

A morphism of Day functors is a module morphism exactly when it commutes with the structure maps at every pair of objects.

def CategoryTheory.Mod.dayHomMk {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] {X Y : Mod (MonoidalCategory.DayFunctor C V) M} (f : X.X ⟶ Y.X) (h : ∀ (p q : C), CategoryStruct.comp (X.dayStructureMap p q) (f.natTrans.app (MonoidalCategoryStruct.tensorObj p q)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (M.functor.obj p) (f.natTrans.app q)) (Y.dayStructureMap p q)) : X ⟶ Y

Construct a module morphism from a morphism of Day functors and its compatibility with the structure maps.

@[simp]

theorem CategoryTheory.Mod.dayHomMk_hom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {M : MonoidalCategory.DayFunctor C V} [MonObj M] {X Y : Mod (MonoidalCategory.DayFunctor C V) M} (f : X.X ⟶ Y.X) (h : ∀ (p q : C), CategoryStruct.comp (X.dayStructureMap p q) (f.natTrans.app (MonoidalCategoryStruct.tensorObj p q)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (M.functor.obj p) (f.natTrans.app q)) (Y.dayStructureMap p q)) : (dayHomMk f h).hom = f

@[simp]

theorem CategoryTheory.Mod.dayStructureMap_unit {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {F : MonoidalCategory.DayFunctor C V} [F.functor.LaxMonoidal] (X : Mod (MonoidalCategory.DayFunctor C V) F) (q : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.ε F.functor) (X.X.functor.obj q)) (X.dayStructureMap (MonoidalCategoryStruct.tensorUnit C) q) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (X.X.functor.obj q)).hom (X.X.functor.map (MonoidalCategoryStruct.leftUnitor q).inv)

Acting by the monoidal unit, after its image under the lax monoidal unit map, is the left unitor followed by the canonical reindexing.

@[simp]

theorem CategoryTheory.Mod.dayStructureMap_unit_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {F : MonoidalCategory.DayFunctor C V} [F.functor.LaxMonoidal] (X : Mod (MonoidalCategory.DayFunctor C V) F) (q : C) {Z : V} (h : X.X.functor.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) q) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.ε F.functor) (X.X.functor.obj q)) (CategoryStruct.comp (X.dayStructureMap (MonoidalCategoryStruct.tensorUnit C) q) h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (X.X.functor.obj q)).hom (CategoryStruct.comp (X.X.functor.map (MonoidalCategoryStruct.leftUnitor q).inv) h)

Acting by the monoidal unit, after its image under the lax monoidal unit map, is the left unitor followed by the canonical reindexing.

theorem CategoryTheory.Mod.dayStructureMap_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {F : MonoidalCategory.DayFunctor C V} [F.functor.LaxMonoidal] (X : Mod (MonoidalCategory.DayFunctor C V) F) (p q r : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ F.functor p q) (X.X.functor.obj r)) (X.dayStructureMap (MonoidalCategoryStruct.tensorObj p q) r) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.functor.obj p) (F.functor.obj q) (X.X.functor.obj r)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.functor.obj p) (X.dayStructureMap q r)) (CategoryStruct.comp (X.dayStructureMap p (MonoidalCategoryStruct.tensorObj q r)) (X.X.functor.map (MonoidalCategoryStruct.associator p q r).inv)))

Multiplying before acting agrees with two successive structure maps. The final reindexing records the associator of the source category.

theorem CategoryTheory.Mod.dayStructureMap_assoc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (MonoidalCategory.externalProduct F G)] [(Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (MonoidalCategory.tensor C) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C))) d) (MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((MonoidalCategory.tensor C).prod (Functor.id C)) d) (MonoidalCategory.tensorRight v)] {F : MonoidalCategory.DayFunctor C V} [F.functor.LaxMonoidal] (X : Mod (MonoidalCategory.DayFunctor C V) F) (p q r : C) {Z : V} (h : X.X.functor.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj p q) r) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Functor.LaxMonoidal.μ F.functor p q) (X.X.functor.obj r)) (CategoryStruct.comp (X.dayStructureMap (MonoidalCategoryStruct.tensorObj p q) r) h) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.functor.obj p) (F.functor.obj q) (X.X.functor.obj r)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.functor.obj p) (X.dayStructureMap q r)) (CategoryStruct.comp (X.dayStructureMap p (MonoidalCategoryStruct.tensorObj q r)) (CategoryStruct.comp (X.X.functor.map (MonoidalCategoryStruct.associator p q r).inv) h)))

Multiplying before acting agrees with two successive structure maps. The final reindexing records the associator of the source category.