Endofunctors as a monoidal category.

We give the monoidal category structure on C ⥤ C, and show that when C itself is monoidal, it embeds via a monoidal functor into C ⥤ C.

TODO

Can we use this to show coherence results, e.g. a cheap proof that λ_ (𝟙_ C) = ρ_ (𝟙_ C)? I suspect this is harder than is usually made out.

def CategoryTheory.endofunctorMonoidalCategory (C : Type u) [Category.{v, u} C] : MonoidalCategory (Functor C C)

The category of endofunctors of any category is a monoidal category, with tensor product given by composition of functors (and horizontal composition of natural transformations).

Equations

• CategoryTheory.endofunctorMonoidalCategory C = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj (C : Type u) [Category.{v, u} C] (X : C) : (𝟙_ (Functor C C)).obj X = X

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map (C : Type u) [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : (𝟙_ (Functor C C)).map f = f

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj (C : Type u) [Category.{v, u} C] (F G : Functor C C) (X : C) : (MonoidalCategoryStruct.tensorObj F G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_map (C : Type u) [Category.{v, u} C] (F G : Functor C C) {X Y : C} (f : X ⟶ Y) : (MonoidalCategoryStruct.tensorObj F G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorMap_app (C : Type u) [Category.{v, u} C] {F G H K : Functor C C} {α : F ⟶ G} {β : H ⟶ K} (X : C) : (MonoidalCategoryStruct.tensorHom α β).app X = CategoryStruct.comp (β.app (F.obj X)) (K.map (α.app X))

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_whiskerLeft_app (C : Type u) [Category.{v, u} C] {F H K : Functor C C} {β : H ⟶ K} (X : C) : (MonoidalCategoryStruct.whiskerLeft F β).app X = β.app (F.obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_whiskerRight_app (C : Type u) [Category.{v, u} C] {F G H : Functor C C} {α : F ⟶ G} (X : C) : (MonoidalCategoryStruct.whiskerRight α H).app X = H.map (α.app X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_associator_hom_app (C : Type u) [Category.{v, u} C] (F G H : Functor C C) (X : C) : (MonoidalCategoryStruct.associator F G H).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj F G) H).obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_associator_inv_app (C : Type u) [Category.{v, u} C] (F G H : Functor C C) (X : C) : (MonoidalCategoryStruct.associator F G H).inv.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj F (MonoidalCategoryStruct.tensorObj G H)).obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_hom_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) : (MonoidalCategoryStruct.leftUnitor F).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (𝟙_ (Functor C C)) F).obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) : (MonoidalCategoryStruct.leftUnitor F).inv.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_rightUnitor_hom_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) : (MonoidalCategoryStruct.rightUnitor F).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj F (𝟙_ (Functor C C))).obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_rightUnitor_inv_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) : (MonoidalCategoryStruct.rightUnitor F).inv.app X = CategoryStruct.id (F.obj X)

instance CategoryTheory.MonoidalCategory.instMonoidalFunctorTensoringRight (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : (tensoringRight C).Monoidal

Tensoring on the right gives a monoidal functor from C into endofunctors of C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_ε (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : Functor.LaxMonoidal.ε (tensoringRight C) = (rightUnitorNatIso C).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_η (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : Functor.OplaxMonoidal.η (tensoringRight C) = (rightUnitorNatIso C).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_μ (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) : (Functor.LaxMonoidal.μ (tensoringRight C) X Y).app Z = (associator Z X Y).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_δ (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) : (Functor.OplaxMonoidal.δ (tensoringRight C) X Y).app Z = (associator Z X Y).inv

@[simp]

theorem CategoryTheory.μ_δ_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (i j : M) (X : C) [F.Monoidal] : CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) ((Functor.OplaxMonoidal.δ F i j).app X) = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X)

@[simp]

theorem CategoryTheory.μ_δ_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (i j : M) (X : C) [F.Monoidal] {Z : C} (h : (MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X ⟶ Z) : CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) h) = h

@[simp]

theorem CategoryTheory.δ_μ_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (i j : M) (X : C) [F.Monoidal] : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) ((Functor.LaxMonoidal.μ F i j).app X) = CategoryStruct.id ((F.obj (MonoidalCategoryStruct.tensorObj i j)).obj X)

@[simp]

theorem CategoryTheory.δ_μ_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (i j : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj i j)).obj X ⟶ Z) : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) h) = h

@[simp]

theorem CategoryTheory.ε_η_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (X : C) [F.Monoidal] : CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) ((Functor.OplaxMonoidal.η F).app X) = CategoryStruct.id ((𝟙_ (Functor C C)).obj X)

@[simp]

theorem CategoryTheory.ε_η_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (X : C) [F.Monoidal] {Z : C} (h : (𝟙_ (Functor C C)).obj X ⟶ Z) : CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) h) = h

@[simp]

theorem CategoryTheory.η_ε_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (X : C) [F.Monoidal] : CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) ((Functor.LaxMonoidal.ε F).app X) = CategoryStruct.id ((F.obj (𝟙_ M)).obj X)

@[simp]

theorem CategoryTheory.η_ε_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (X : C) [F.Monoidal] {Z : C} (h : (F.obj (𝟙_ M)).obj X ⟶ Z) : CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) h) = h

@[simp]

theorem CategoryTheory.ε_naturality {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] : CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) ((F.obj (𝟙_ M)).map f) = CategoryStruct.comp f ((Functor.LaxMonoidal.ε F).app Y)

@[simp]

theorem CategoryTheory.ε_naturality_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] {Z : C} (h : (F.obj (𝟙_ M)).obj Y ⟶ Z) : CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((F.obj (𝟙_ M)).map f) h) = CategoryStruct.comp f (CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app Y) h)

@[simp]

theorem CategoryTheory.η_naturality {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] : CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) ((𝟙_ (Functor C C)).map f) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) f

@[simp]

theorem CategoryTheory.η_naturality_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] {Z : C} (h : (𝟙_ (Functor C C)).obj Y ⟶ Z) : CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp ((𝟙_ (Functor C C)).map f) h) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.μ_naturality {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n : M} {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] : CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) ((Functor.LaxMonoidal.μ F m n).app Y) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f)

@[simp]

theorem CategoryTheory.μ_naturality_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n : M} {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m n)).obj Y ⟶ Z) : CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app Y) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) h)

theorem CategoryTheory.δ_naturality {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n : M} {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.obj n).map ((F.obj m).map f)) = CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) ((Functor.OplaxMonoidal.δ F m n).app Y)

theorem CategoryTheory.δ_naturality_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n : M} {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] {Z : C} (h : (F.obj n).obj ((F.obj m).obj Y) ⟶ Z) : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) h) = CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app Y) h)

theorem CategoryTheory.μ_naturality₂ {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) [F.LaxMonoidal] : CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((Functor.LaxMonoidal.μ F m' n').app X)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.tensorHom f g)).app X)

theorem CategoryTheory.μ_naturality₂_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m' n')).obj X ⟶ Z) : CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m' n').app X) h)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.tensorHom f g)).app X) h)

@[simp]

theorem CategoryTheory.μ_naturalityₗ {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' : M} (f : m ⟶ m') (X : C) [F.LaxMonoidal] : CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) ((Functor.LaxMonoidal.μ F m' n).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X)

@[simp]

theorem CategoryTheory.μ_naturalityₗ_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' : M} (f : m ⟶ m') (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m' n)).obj X ⟶ Z) : CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m' n).app X) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) h)

@[simp]

theorem CategoryTheory.μ_naturalityᵣ {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n n' : M} (g : n ⟶ n') (X : C) [F.LaxMonoidal] : CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) ((Functor.LaxMonoidal.μ F m n').app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X)

@[simp]

theorem CategoryTheory.μ_naturalityᵣ_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n n' : M} (g : n ⟶ n') (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m n')).obj X ⟶ Z) : CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n').app X) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) h)

@[simp]

theorem CategoryTheory.δ_naturalityₗ {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' : M} (f : m ⟶ m') (X : C) [F.OplaxMonoidal] : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.obj n).map ((F.map f).app X)) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) ((Functor.OplaxMonoidal.δ F m' n).app X)

@[simp]

theorem CategoryTheory.δ_naturalityₗ_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' : M} (f : m ⟶ m') (X : C) [F.OplaxMonoidal] {Z : C} (h : (F.obj n).obj ((F.obj m').obj X) ⟶ Z) : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) h) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m' n).app X) h)

@[simp]

theorem CategoryTheory.δ_naturalityᵣ {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n n' : M} (g : n ⟶ n') (X : C) [F.OplaxMonoidal] : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.map g).app ((F.obj m).obj X)) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) ((Functor.OplaxMonoidal.δ F m n').app X)

@[simp]

theorem CategoryTheory.δ_naturalityᵣ_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n n' : M} (g : n ⟶ n') (X : C) [F.OplaxMonoidal] {Z : C} (h : (F.obj n').obj ((F.obj m).obj X) ⟶ Z) : CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) h) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n').app X) h)

theorem CategoryTheory.left_unitality_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.LaxMonoidal] : CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X) ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X)) = CategoryStruct.id ((F.obj n).obj ((𝟙_ (Functor C C)).obj X))

theorem CategoryTheory.left_unitality_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj n).obj X ⟶ Z) : CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X) h)) = h

@[simp]

theorem CategoryTheory.obj_ε_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] : (F.obj n).map ((Functor.LaxMonoidal.ε F).app X) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).inv).app X) ((Functor.OplaxMonoidal.δ F (𝟙_ M) n).app X)

theorem CategoryTheory.obj_ε_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj n).obj ((F.obj (𝟙_ M)).obj X) ⟶ Z) : CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) h = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).inv).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F (𝟙_ M) n).app X) h)

@[simp]

theorem CategoryTheory.obj_η_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] : (F.obj n).map ((Functor.OplaxMonoidal.η F).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X) ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X)

theorem CategoryTheory.obj_η_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj n).obj ((𝟙_ (Functor C C)).obj X) ⟶ Z) : CategoryStruct.comp ((F.obj n).map ((Functor.OplaxMonoidal.η F).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X) h)

theorem CategoryTheory.right_unitality_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] : CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app ((F.obj n).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (𝟙_ M)).app X) ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X)) = CategoryStruct.id ((𝟙_ (Functor C C)).obj ((F.obj n).obj X))

theorem CategoryTheory.right_unitality_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj n).obj X ⟶ Z) : CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app ((F.obj n).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (𝟙_ M)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X) h)) = h

@[simp]

theorem CategoryTheory.ε_app_obj {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] : (Functor.LaxMonoidal.ε F).app ((F.obj n).obj X) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor n).inv).app X) ((Functor.OplaxMonoidal.δ F n (𝟙_ M)).app X)

@[simp]

theorem CategoryTheory.η_app_obj {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (n : M) (X : C) [F.Monoidal] : (Functor.OplaxMonoidal.η F).app ((F.obj n).obj X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (𝟙_ M)).app X) ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X)

theorem CategoryTheory.associativity_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ m₃ : M) (X : C) [F.LaxMonoidal] : CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)

theorem CategoryTheory.associativity_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ m₃ : M) (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃))).obj X ⟶ Z) : CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) h)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) h)

@[simp]

theorem CategoryTheory.obj_μ_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] : (F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X) ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)))

theorem CategoryTheory.obj_μ_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj m₃).obj ((F.obj (MonoidalCategoryStruct.tensorObj m₁ m₂)).obj X) ⟶ Z) : CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) h)))

@[simp]

theorem CategoryTheory.obj_μ_inv_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] : (F.obj m₃).map ((Functor.OplaxMonoidal.δ F m₁ m₂).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) ((Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X))))

theorem CategoryTheory.obj_μ_inv_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj m₃).obj ((MonoidalCategoryStruct.tensorObj (F.obj m₁) (F.obj m₂)).obj X) ⟶ Z) : CategoryStruct.comp ((F.obj m₃).map ((Functor.OplaxMonoidal.δ F m₁ m₂).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X)) h)))

@[simp]

theorem CategoryTheory.obj_zero_map_μ_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) [F.Monoidal] : CategoryStruct.comp ((F.obj (𝟙_ M)).map f) ((Functor.LaxMonoidal.μ F m (𝟙_ M)).app Y) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f ((F.map (MonoidalCategoryStruct.rightUnitor m).inv).app Y))

@[simp]

theorem CategoryTheory.obj_zero_map_μ_app_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) [F.Monoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m (𝟙_ M))).obj Y ⟶ Z) : CategoryStruct.comp ((F.obj (𝟙_ M)).map f) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m (𝟙_ M)).app Y) h) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor m).inv).app Y) h))

@[simp]

theorem CategoryTheory.obj_μ_zero_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m₁ m₂ : M) (X : C) [F.Monoidal] : CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj (𝟙_ M) m₂)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ (𝟙_ M) m₂).inv).app X) ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ (𝟙_ M)) m₂).app X))) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor m₂).hom).app ((F.obj m₁).obj X)) ((F.obj m₂).map ((F.map (MonoidalCategoryStruct.rightUnitor m₁).inv).app X)))

noncomputable def CategoryTheory.unitOfTensorIsoUnit {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) [F.Monoidal] : (F.obj m).comp (F.obj n) ≅ Functor.id C

If m ⊗ n ≅ 𝟙_M, then F.obj m is a left inverse of F.obj n.

Equations

• CategoryTheory.unitOfTensorIsoUnit F m n h = CategoryTheory.Functor.Monoidal.μIso F m n ≪≫ F.mapIso h ≪≫ (CategoryTheory.Functor.Monoidal.εIso F).symm

@[simp]

theorem CategoryTheory.unitOfTensorIsoUnit_inv_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) [F.Monoidal] (X : C) : (unitOfTensorIsoUnit F m n h).inv.app X = CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((F.map h.inv).app X) ((Functor.OplaxMonoidal.δ F m n).app X))

@[simp]

theorem CategoryTheory.unitOfTensorIsoUnit_hom_app {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) [F.Monoidal] (X : C) : (unitOfTensorIsoUnit F m n h).hom.app X = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map h.hom).app X) ((Functor.OplaxMonoidal.η F).app X))

noncomputable def CategoryTheory.equivOfTensorIsoUnit {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) (h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M) (H : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom)) [F.Monoidal] : C ≌ C

If m ⊗ n ≅ 𝟙_M and n ⊗ m ≅ 𝟙_M (subject to some commuting constraints), then F.obj m and F.obj n forms a self-equivalence of C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.equivOfTensorIsoUnit_unitIso {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) (h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M) (H : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom)) [F.Monoidal] : (equivOfTensorIsoUnit F m n h₁ h₂ H).unitIso = (unitOfTensorIsoUnit F m n h₁).symm

@[simp]

theorem CategoryTheory.equivOfTensorIsoUnit_functor {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) (h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M) (H : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom)) [F.Monoidal] : (equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.obj m

@[simp]

theorem CategoryTheory.equivOfTensorIsoUnit_counitIso {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) (h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M) (H : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom)) [F.Monoidal] : (equivOfTensorIsoUnit F m n h₁ h₂ H).counitIso = unitOfTensorIsoUnit F n m h₂

@[simp]

theorem CategoryTheory.equivOfTensorIsoUnit_inverse {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) (m n : M) (h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M) (h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M) (H : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom)) [F.Monoidal] : (equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.obj n