Whiskerings, associators and unitors under a lawful Day convolution structure

For a lawful Day convolution monoidal structure on D, Mathlib proves that the faithful functor ι : D ⥤ C ⥤ V carries tensor products of morphisms and associators to their Day convolution counterparts. This file adds the corresponding statements for left and right whiskerings and for inverse associators. They are used to transfer the Day convolution braiding to C ⊛⥤ V.

For C ⊛⥤ V itself, we restate Mathlib's characterisations of the whiskerings, the tensor product of morphisms, the associator and the unitors along the Day convolution units η F G and ν C V, in a form simp can use, and prove that morphisms out of (F ⊗ G) ⊗ H, 𝟙_ ⊗ F and F ⊗ 𝟙_ are determined by their restrictions along these units.

Main statements

• LawfulDayConvolutionMonoidalCategoryStruct.ι_map_whiskerLeft_eq_tensorHom and LawfulDayConvolutionMonoidalCategoryStruct.ι_map_whiskerRight_eq_tensorHom: ι carries whiskerings to Day convolutions with an identity.
• LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_inv_eq_associator_inv: ι carries the inverse associator to the inverse Day convolution associator.
• DayFunctor.tensor_tensor_hom_ext, DayFunctor.unit_tensor_hom_ext, DayFunctor.tensor_unit_hom_ext: extensionality for morphisms out of iterated Day convolutions.

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_whiskerLeft_eq_tensorHom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D) {d' d'' : D} (f : d' ⟶ d'') : (ι C V D).map (whiskerLeft d f) = DayConvolution.map (CategoryStruct.id ((ι C V D).obj d)) ((ι C V D).map f)

ι carries a left whiskering d ◁ f to the Day convolution of 𝟙 and ι.map f.

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_whiskerRight_eq_tensorHom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] {d d' : D} (f : d ⟶ d') (d'' : D) : (ι C V D).map (whiskerRight f d'') = DayConvolution.map ((ι C V D).map f) (CategoryStruct.id ((ι C V D).obj d''))

ι carries a right whiskering f ▷ d'' to the Day convolution of ι.map f and 𝟙.

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_inv_eq_associator_inv (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d d' d'' : D) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] : (ι C V D).map (associator d d' d'').inv = (DayConvolution.associator ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).inv

ι carries the inverse associator to the inverse Day convolution associator.

The monoidal structure along the Day convolution units

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_whiskerLeft_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) {G G' : DayFunctor C V} (g : G ⟶ G') (x y : C) : CategoryStruct.comp ((F.η G).app (x, y)) ((whiskerLeft F g).natTrans.app (tensorObj x y)) = CategoryStruct.comp (whiskerLeft (F.functor.obj x) (g.natTrans.app y)) ((F.η G').app (x, y))

The left whiskering F ◁ g restricted along the Day convolution unit η F G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_whiskerLeft_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) {G G' : DayFunctor C V} (g : G ⟶ G') (x y : C) {Z : V} (h : (tensorObj F G').functor.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((F.η G).app (x, y)) (CategoryStruct.comp ((whiskerLeft F g).natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (whiskerLeft (F.functor.obj x) (g.natTrans.app y)) (CategoryStruct.comp ((F.η G').app (x, y)) h)

The left whiskering F ◁ g restricted along the Day convolution unit η F G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_whiskerRight_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F F' : DayFunctor C V} (f : F ⟶ F') (G : DayFunctor C V) (x y : C) : CategoryStruct.comp ((F.η G).app (x, y)) ((whiskerRight f G).natTrans.app (tensorObj x y)) = CategoryStruct.comp (whiskerRight (f.natTrans.app x) (G.functor.obj y)) ((F'.η G).app (x, y))

The right whiskering f ▷ G restricted along the Day convolution unit η F G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_whiskerRight_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F F' : DayFunctor C V} (f : F ⟶ F') (G : DayFunctor C V) (x y : C) {Z : V} (h : (tensorObj F' G).functor.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((F.η G).app (x, y)) (CategoryStruct.comp ((whiskerRight f G).natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (whiskerRight (f.natTrans.app x) (G.functor.obj y)) (CategoryStruct.comp ((F'.η G).app (x, y)) h)

The right whiskering f ▷ G restricted along the Day convolution unit η F G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_tensorHom_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F F' G G' : DayFunctor C V} (f : F ⟶ F') (g : G ⟶ G') (x y : C) : CategoryStruct.comp ((F.η G).app (x, y)) ((tensorHom f g).natTrans.app (tensorObj x y)) = CategoryStruct.comp (tensorHom (f.natTrans.app x) (g.natTrans.app y)) ((F'.η G').app (x, y))

The tensor product f ⊗ₘ g restricted along the Day convolution unit η F G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_tensorHom_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F F' G G' : DayFunctor C V} (f : F ⟶ F') (g : G ⟶ G') (x y : C) {Z : V} (h : (tensorObj F' G').functor.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((F.η G).app (x, y)) (CategoryStruct.comp ((tensorHom f g).natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (tensorHom (f.natTrans.app x) (g.natTrans.app y)) (CategoryStruct.comp ((F'.η G').app (x, y)) h)

The tensor product f ⊗ₘ g restricted along the Day convolution unit η F G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_whiskerRight_comp_η_app_comp_associator_hom_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G H : DayFunctor C V) (x y z : C) : CategoryStruct.comp (whiskerRight ((F.η G).app (x, y)) (H.functor.obj z)) (CategoryStruct.comp (((tensorObj F G).η H).app (tensorObj x y, z)) ((associator F G H).hom.natTrans.app (tensorObj (tensorObj x y) z))) = CategoryStruct.comp (associator (F.functor.obj x) ((G.functor, H.functor).1.obj (y, z).1) ((G.functor, H.functor).2.obj (y, z).2)).hom (CategoryStruct.comp (whiskerLeft (F.functor.obj x) ((G.η H).app (y, z))) (CategoryStruct.comp ((F.η (tensorObj G H)).app (x, tensorObj y z)) ((tensorObj F (tensorObj G H)).functor.map (associator x y z).inv)))

The associator (F ⊗ G) ⊗ H ≅ F ⊗ G ⊗ H restricted along the Day convolution units: at (x, y, z) it is the associator of V, followed by the units and the action of F ⊗ G ⊗ H on the inverse associator of C.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_whiskerRight_comp_η_app_comp_associator_hom_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G H : DayFunctor C V) (x y z : C) {Z : V} (h : (tensorObj F (tensorObj G H)).functor.obj (tensorObj (tensorObj x y) z) ⟶ Z) : CategoryStruct.comp (whiskerRight ((F.η G).app (x, y)) (H.functor.obj z)) (CategoryStruct.comp (((tensorObj F G).η H).app (tensorObj x y, z)) (CategoryStruct.comp ((associator F G H).hom.natTrans.app (tensorObj (tensorObj x y) z)) h)) = CategoryStruct.comp (associator (F.functor.obj x) (G.functor.obj y) (H.functor.obj z)).hom (CategoryStruct.comp (whiskerLeft (F.functor.obj x) ((G.η H).app (y, z))) (CategoryStruct.comp ((F.η (tensorObj G H)).app (x, tensorObj y z)) (CategoryStruct.comp ((tensorObj F (tensorObj G H)).functor.map (associator x y z).inv) h)))

The associator (F ⊗ G) ⊗ H ≅ F ⊗ G ⊗ H restricted along the Day convolution units: at (x, y, z) it is the associator of V, followed by the units and the action of F ⊗ G ⊗ H on the inverse associator of C.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.whiskerLeft_η_app_comp_η_app_comp_associator_inv_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G H : DayFunctor C V) (x y z : C) : CategoryStruct.comp (whiskerLeft (F.functor.obj x) ((G.η H).app (y, z))) (CategoryStruct.comp ((F.η (tensorObj G H)).app (x, tensorObj y z)) ((associator F G H).inv.natTrans.app (tensorObj x (tensorObj y z)))) = CategoryStruct.comp (associator ((F.functor, G.functor).1.obj (x, y).1) ((F.functor, G.functor).2.obj (x, y).2) (H.functor.obj z)).inv (CategoryStruct.comp (whiskerRight ((F.η G).app (x, y)) (H.functor.obj z)) (CategoryStruct.comp (((tensorObj F G).η H).app (tensorObj x y, z)) ((tensorObj (tensorObj F G) H).functor.map (associator x y z).hom)))

The inverse associator restricted along two Day convolution units regroups the three factors by the inverse pointwise associator.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.whiskerLeft_η_app_comp_η_app_comp_associator_inv_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G H : DayFunctor C V) (x y z : C) {Z : V} (h : (tensorObj (tensorObj F G) H).functor.obj (tensorObj x (tensorObj y z)) ⟶ Z) : CategoryStruct.comp (whiskerLeft (F.functor.obj x) ((G.η H).app (y, z))) (CategoryStruct.comp ((F.η (tensorObj G H)).app (x, tensorObj y z)) (CategoryStruct.comp ((associator F G H).inv.natTrans.app (tensorObj x (tensorObj y z))) h)) = CategoryStruct.comp (associator (F.functor.obj x) (G.functor.obj y) (H.functor.obj z)).inv (CategoryStruct.comp (whiskerRight ((F.η G).app (x, y)) (H.functor.obj z)) (CategoryStruct.comp (((tensorObj F G).η H).app (tensorObj x y, z)) (CategoryStruct.comp ((tensorObj (tensorObj F G) H).functor.map (associator x y z).hom) h)))

The inverse associator restricted along two Day convolution units regroups the three factors by the inverse pointwise associator.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ν_whiskerRight_comp_η_app_comp_leftUnitor_hom_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) (y : C) : CategoryStruct.comp (whiskerRight (ν C V) (F.functor.obj y)) (CategoryStruct.comp (((tensorUnit (DayFunctor C V)).η F).app (tensorUnit C, y)) ((leftUnitor F).hom.natTrans.app (tensorObj (tensorUnit C) y))) = CategoryStruct.comp (leftUnitor (F.functor.obj y)).hom (F.functor.map (leftUnitor y).inv)

The left unitor 𝟙_ ⊗ F ≅ F restricted along the Day convolution units.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ν_whiskerRight_comp_η_app_comp_leftUnitor_hom_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) (y : C) {Z : V} (h : F.functor.obj (tensorObj (tensorUnit C) y) ⟶ Z) : CategoryStruct.comp (whiskerRight (ν C V) (F.functor.obj y)) (CategoryStruct.comp (((tensorUnit (DayFunctor C V)).η F).app (tensorUnit C, y)) (CategoryStruct.comp ((leftUnitor F).hom.natTrans.app (tensorObj (tensorUnit C) y)) h)) = CategoryStruct.comp (leftUnitor (F.functor.obj y)).hom (CategoryStruct.comp (F.functor.map (leftUnitor y).inv) h)

The left unitor 𝟙_ ⊗ F ≅ F restricted along the Day convolution units.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.whiskerLeft_ν_comp_η_app_comp_rightUnitor_hom_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) (x : C) : CategoryStruct.comp (whiskerLeft (F.functor.obj x) (ν C V)) (CategoryStruct.comp ((F.η (tensorUnit (DayFunctor C V))).app (x, tensorUnit C)) ((rightUnitor F).hom.natTrans.app (tensorObj x (tensorUnit C)))) = CategoryStruct.comp (rightUnitor (F.functor.obj x)).hom (F.functor.map (rightUnitor x).inv)

The right unitor F ⊗ 𝟙_ ≅ F restricted along the Day convolution units.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.whiskerLeft_ν_comp_η_app_comp_rightUnitor_hom_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F : DayFunctor C V) (x : C) {Z : V} (h : F.functor.obj (tensorObj x (tensorUnit C)) ⟶ Z) : CategoryStruct.comp (whiskerLeft (F.functor.obj x) (ν C V)) (CategoryStruct.comp ((F.η (tensorUnit (DayFunctor C V))).app (x, tensorUnit C)) (CategoryStruct.comp ((rightUnitor F).hom.natTrans.app (tensorObj x (tensorUnit C))) h)) = CategoryStruct.comp (rightUnitor (F.functor.obj x)).hom (CategoryStruct.comp (F.functor.map (rightUnitor x).inv) h)

The right unitor F ⊗ 𝟙_ ≅ F restricted along the Day convolution units.

theorem CategoryTheory.MonoidalCategory.DayFunctor.unit_tensor_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G : DayFunctor C V} {α β : tensorObj (tensorUnit (DayFunctor C V)) F ⟶ G} (h : ∀ (y : C), CategoryStruct.comp (whiskerRight (ν C V) (F.functor.obj y)) (CategoryStruct.comp (((tensorUnit (DayFunctor C V)).η F).app (tensorUnit C, y)) (α.natTrans.app (tensorObj (tensorUnit C) y))) = CategoryStruct.comp (whiskerRight (ν C V) (F.functor.obj y)) (CategoryStruct.comp (((tensorUnit (DayFunctor C V)).η F).app (tensorUnit C, y)) (β.natTrans.app (tensorObj (tensorUnit C) y)))) : α = β

Morphisms out of 𝟙_ ⊗ F are determined by their restrictions along ν C V and the Day convolution unit η (𝟙_ _) F.

theorem CategoryTheory.MonoidalCategory.DayFunctor.tensor_unit_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G : DayFunctor C V} {α β : tensorObj F (tensorUnit (DayFunctor C V)) ⟶ G} (h : ∀ (x : C), CategoryStruct.comp (whiskerLeft (F.functor.obj x) (ν C V)) (CategoryStruct.comp ((F.η (tensorUnit (DayFunctor C V))).app (x, tensorUnit C)) (α.natTrans.app (tensorObj x (tensorUnit C)))) = CategoryStruct.comp (whiskerLeft (F.functor.obj x) (ν C V)) (CategoryStruct.comp ((F.η (tensorUnit (DayFunctor C V))).app (x, tensorUnit C)) (β.natTrans.app (tensorObj x (tensorUnit C))))) : α = β

Morphisms out of F ⊗ 𝟙_ are determined by their restrictions along ν C V and the Day convolution unit η F (𝟙_ _).

theorem CategoryTheory.MonoidalCategory.DayFunctor.tensor_tensor_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G H K : DayFunctor C V} {α β : tensorObj (tensorObj F G) H ⟶ K} (h : ∀ (x y z : C), CategoryStruct.comp (whiskerRight ((F.η G).app (x, y)) (H.functor.obj z)) (CategoryStruct.comp (((tensorObj F G).η H).app (tensorObj x y, z)) (α.natTrans.app (tensorObj (tensorObj x y) z))) = CategoryStruct.comp (whiskerRight ((F.η G).app (x, y)) (H.functor.obj z)) (CategoryStruct.comp (((tensorObj F G).η H).app (tensorObj x y, z)) (β.natTrans.app (tensorObj (tensorObj x y) z)))) : α = β

Morphisms out of (F ⊗ G) ⊗ H are determined by their restrictions along the Day convolution units η F G and η (F ⊗ G) H.