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) [CategoryTheory.Category.{v, u} C] : CategoryTheory.MonoidalCategory (CategoryTheory.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) [CategoryTheory.Category.{v, u} C] (X : C) : (𝟙_ (CategoryTheory.Functor C C)).obj X = X

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.MonoidalCategory.instMonoidalFunctorTensoringRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalCategory.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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalCategory.tensoringRight C) = (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).inv

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.δ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.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) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X) (CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) h) = CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).map f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app Y) h)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.δ_naturalityₗ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.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) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X) (CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.whiskerRight f n)).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m' n).app X) h)

@[simp]

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

@[simp]

theorem CategoryTheory.δ_naturalityᵣ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.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) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.whiskerLeft m g)).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n').app X) h)

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

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

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.unitOfTensorIsoUnit {C : Type u} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M) (h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) [F.Monoidal] : (F.obj m).comp (F.obj n) ≅ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M) (h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) [F.Monoidal] (X : C) : (CategoryTheory.unitOfTensorIsoUnit F m n h).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X) (CategoryTheory.CategoryStruct.comp ((F.map h.inv).app X) ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X))

@[simp]

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

noncomputable def CategoryTheory.equivOfTensorIsoUnit {C : Type u} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight h₁.hom m) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft m h₂.hom) (CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight h₁.hom m) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft m h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)) [F.Monoidal] : (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).unitIso = (CategoryTheory.unitOfTensorIsoUnit F m n h₁).symm

@[simp]

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

@[simp]

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

@[simp]

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