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)).toPrefunctor.obj X = X

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_associator_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C) (G : CategoryTheory.Functor C C) (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).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_associator_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C) (G : CategoryTheory.Functor C C) (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)).toPrefunctor.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).toPrefunctor.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.toPrefunctor.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))).toPrefunctor.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.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_ε_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.tensoringRightMonoidal C).toLaxMonoidalFunctor.ε.app X = (CategoryTheory.MonoidalCategory.rightUnitor X).inv

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_toFunctor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) : ((CategoryTheory.tensoringRightMonoidal C).toLaxMonoidalFunctor.toFunctor.toPrefunctor.map f).app Z = CategoryTheory.MonoidalCategory.whiskerLeft Z f

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_toFunctor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y : C} {Y' : C} (f : Y ⟶ Y') : ((CategoryTheory.tensoringRightMonoidal C).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).toPrefunctor.map f = CategoryTheory.MonoidalCategory.whiskerRight f X

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_toFunctor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : ((CategoryTheory.tensoringRightMonoidal C).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).toPrefunctor.obj Y = CategoryTheory.MonoidalCategory.tensorObj Y X

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_μ_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : ((CategoryTheory.tensoringRightMonoidal C).toLaxMonoidalFunctor.μ X Y).app Z = (CategoryTheory.MonoidalCategory.associator Z X Y).hom

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

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.μ_hom_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (i : M) (j : M) (X : C) {Z : C} (h : (CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj i) (F.toPrefunctor.obj j)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ i j).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) h) = h

@[simp]

theorem CategoryTheory.μ_hom_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (i : M) (j : M) (X : C) : CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ i j).app X) ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj i) (F.toPrefunctor.obj j)).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.μ_inv_hom_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (i : M) (j : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ i j).app X) h) = h

@[simp]

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (i : M) (j : M) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) ((F.toLaxMonoidalFunctor.μ i j).app X) = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.ε_hom_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (X : C) {Z : C} (h : (𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) h) = h

@[simp]

theorem CategoryTheory.ε_hom_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (X : C) : CategoryTheory.CategoryStruct.comp (F.ε.app X) ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) = CategoryTheory.CategoryStruct.id ((𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.ε_inv_hom_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (X : C) {Z : C} (h : (F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp (F.ε.app X) h) = h

@[simp]

theorem CategoryTheory.ε_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (F.ε.app X) = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.obj 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : (F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (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.MonoidalFunctor M (CategoryTheory.Functor C C)) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.ε.app X) ((F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp f (F.ε.app Y)

@[simp]

theorem CategoryTheory.ε_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : (𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp ((𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.ε_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) ((𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.obj m).toPrefunctor.map f)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app Y) h) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).toPrefunctor.map 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.obj m).toPrefunctor.map f)) ((F.toLaxMonoidalFunctor.μ m n).app Y) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) ((F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).toPrefunctor.map f)

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : (F.toPrefunctor.obj n).toPrefunctor.obj ((F.toPrefunctor.obj m).toPrefunctor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.obj m).toPrefunctor.map f)) h) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app Y) h)

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.obj m).toPrefunctor.map f)) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).toPrefunctor.map f) ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} {n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m' n')).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map g).app ((F.toPrefunctor.obj m).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n').toPrefunctor.map ((F.toPrefunctor.map f).app X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m' n').app X) h)) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g)).app X) 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} {n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map g).app ((F.toPrefunctor.obj m).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n').toPrefunctor.map ((F.toPrefunctor.map f).app X)) ((F.toLaxMonoidalFunctor.μ m' n').app X)) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} (f : m ⟶ m') (X : C) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m' n)).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.map f).app X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m' n).app X) h) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} (f : m ⟶ m') (X : C) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.map f).app X)) ((F.toLaxMonoidalFunctor.μ m' n).app X) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {n' : M} (g : n ⟶ n') (X : C) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m n')).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map g).app ((F.toPrefunctor.obj m).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n').app X) h) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {n' : M} (g : n ⟶ n') (X : C) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map g).app ((F.toPrefunctor.obj m).toPrefunctor.obj X)) ((F.toLaxMonoidalFunctor.μ m n').app X) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X)

@[simp]

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} (f : m ⟶ m') (X : C) {Z : C} (h : (F.toPrefunctor.obj n).toPrefunctor.obj ((F.toPrefunctor.obj m').toPrefunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.map f).app X)) h) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id n))).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m' n).inv.app X) h)

@[simp]

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} (f : m ⟶ m') (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) ((F.toPrefunctor.obj n).toPrefunctor.map ((F.toPrefunctor.map f).app X)) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id n))).app X) ((CategoryTheory.MonoidalFunctor.μIso F m' n).inv.app X)

@[simp]

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {n' : M} (g : n ⟶ n') (X : C) {Z : C} (h : (F.toPrefunctor.obj n').toPrefunctor.obj ((F.toPrefunctor.obj m).toPrefunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map g).app ((F.toPrefunctor.obj m).toPrefunctor.obj X)) h) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n').inv.app X) h)

@[simp]

theorem CategoryTheory.μ_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {n' : M} (g : n ⟶ n') (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) ((F.toPrefunctor.map g).app ((F.toPrefunctor.obj m).toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X) ((CategoryTheory.MonoidalFunctor.μIso F m n').inv.app 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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj n).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (𝟙_ M) n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X) h)) = 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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (𝟙_ M) n).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X)) = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj n).toPrefunctor.obj ((𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.obj X))

@[simp]

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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj n).toPrefunctor.obj ((F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map (F.ε.app X)) h = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor n).inv).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F (𝟙_ M) n).inv.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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) : (F.toPrefunctor.obj n).toPrefunctor.map (F.ε.app X) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor n).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F (𝟙_ M) n).inv.app X)

@[simp]

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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj n).toPrefunctor.obj ((𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj n).toPrefunctor.map ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X)) h = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (𝟙_ M) n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) : (F.toPrefunctor.obj n).toPrefunctor.map ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (𝟙_ M) n).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app 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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj n).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.ε.app ((F.toPrefunctor.obj n).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ n (𝟙_ M)).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X) h)) = 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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) : CategoryTheory.CategoryStruct.comp (F.ε.app ((F.toPrefunctor.obj n).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ n (𝟙_ M)).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X)) = CategoryTheory.CategoryStruct.id ((𝟙_ (CategoryTheory.Functor C C)).toPrefunctor.obj ((F.toPrefunctor.obj n).toPrefunctor.obj 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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) : F.ε.app ((F.toPrefunctor.obj n).toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor n).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X)

@[simp]

theorem CategoryTheory.ε_inv_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.MonoidalFunctor M (CategoryTheory.Functor C C)) (n : M) (X : C) : (CategoryTheory.MonoidalFunctor.εIso F).inv.app ((F.toPrefunctor.obj n).toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ n (𝟙_ M)).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃))).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj m₃).toPrefunctor.map ((F.toLaxMonoidalFunctor.μ m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X) h)) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₂ m₃).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) h)

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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj m₃).toPrefunctor.map ((F.toLaxMonoidalFunctor.μ m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X)) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₂ m₃).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) ((F.toLaxMonoidalFunctor.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X)

@[simp]

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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj m₃).toPrefunctor.obj ((F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂)).toPrefunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj m₃).toPrefunctor.map ((F.toLaxMonoidalFunctor.μ m₁ m₂).app X)) h = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₂ m₃).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).inv).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).inv.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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) : (F.toPrefunctor.obj m₃).toPrefunctor.map ((F.toLaxMonoidalFunctor.μ m₁ m₂).app X) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₂ m₃).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).inv.app X)))

@[simp]

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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) {Z : C} (h : (F.toPrefunctor.obj m₃).toPrefunctor.obj ((CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj m₁) (F.toPrefunctor.obj m₂)).toPrefunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj m₃).toPrefunctor.map ((CategoryTheory.MonoidalFunctor.μIso F m₁ m₂).inv.app X)) h = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.toPrefunctor.obj m₁).toPrefunctor.obj 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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) : (F.toPrefunctor.obj m₃).toPrefunctor.map ((CategoryTheory.MonoidalFunctor.μIso F m₁ m₂).inv.app X) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) ((CategoryTheory.MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X))))

@[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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {X : C} {Y : C} (f : X ⟶ (F.toPrefunctor.obj m).toPrefunctor.obj Y) {Z : C} (h : (F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj m (𝟙_ M))).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m (𝟙_ M)).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor m).inv).app Y) 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.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {X : C} {Y : C} (f : X ⟶ (F.toPrefunctor.obj m).toPrefunctor.obj Y) : CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.obj (𝟙_ M)).toPrefunctor.map f) ((F.toLaxMonoidalFunctor.μ m (𝟙_ M)).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp f ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor m).inv).app Y))

@[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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m₁ : M) (m₂ : M) (X : C) : CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (𝟙_ M) m₂).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ M) m₂)).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator m₁ (𝟙_ M) m₂).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorObj m₁ (𝟙_ M)) m₂).inv.app X))) = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ (𝟙_ M) m₂).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor m₂).hom).app ((F.toPrefunctor.obj m₁).toPrefunctor.obj X)) ((F.toPrefunctor.obj m₂).toPrefunctor.map ((F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor m₁).inv).app X)))

@[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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (X : C) : (CategoryTheory.unitOfTensorIsoUnit F m n h).inv.app X = CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map h.inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (X : C) : (CategoryTheory.unitOfTensorIsoUnit F m n h).hom.app X = CategoryTheory.CategoryStruct.comp ((F.toLaxMonoidalFunctor.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map h.hom).app X) ((CategoryTheory.MonoidalFunctor.εIso F).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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) : CategoryTheory.Functor.comp (F.toPrefunctor.obj m) (F.toPrefunctor.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.MonoidalFunctor.μIso F m n ≪≫ F.mapIso h ≪≫ (CategoryTheory.MonoidalFunctor.εIso F).symm

@[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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h₁.hom (CategoryTheory.CategoryStruct.id m)) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)) : (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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h₁.hom (CategoryTheory.CategoryStruct.id m)) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)) : (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.toPrefunctor.obj n

@[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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h₁.hom (CategoryTheory.CategoryStruct.id m)) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)) : (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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h₁.hom (CategoryTheory.CategoryStruct.id m)) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)) : (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.toPrefunctor.obj m

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.MonoidalFunctor M (CategoryTheory.Functor C C)) (m : M) (n : M) (h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M) (h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h₁.hom (CategoryTheory.CategoryStruct.id m)) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)) : 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.