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.

source

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).

Instances For

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) :

(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj X = X

source

@[simp]

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

(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).map f = f

source

@[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).obj X = G.obj (F.obj X)

source

@[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).map f = G.map (F.map f)

source

@[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.obj X)) (K.map (α.app X))

source

@[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).obj X)

source

@[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)).obj X)

source

@[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.MonoidalCategory.tensorUnit' F).obj X)

source

@[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)

source

@[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.MonoidalCategory.tensorUnit').obj X)

source

@[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)

source

@[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.obj X).obj Y = CategoryTheory.MonoidalCategory.tensorObj Y X

source

@[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.obj X).map f = CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X)

source

@[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

source

@[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.map f).app Z = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f

source

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_μ_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) :

(CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.tensoringRightMonoidal C).toLaxMonoidalFunctor X Y).app Z = (CategoryTheory.MonoidalCategory.associator Z X Y).hom

source

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.

Instances For

source

@[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.obj i) (F.obj j)).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor i j).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) h) = h

source

@[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 ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor i j).app X) ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (F.obj i) (F.obj j)).obj X)

source

@[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.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F i j).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor i j).app X) h) = h

source

@[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) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor i j).app X) = CategoryTheory.CategoryStruct.id ((F.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).obj X)

source

@[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.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) h) = h

source

@[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.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj X)

source

@[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.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp (F.ε.app X) h) = h

source

@[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.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).obj X)

source

@[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.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).map f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (F.ε.app Y) h)

source

@[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.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).map f) = CategoryTheory.CategoryStruct.comp f (F.ε.app Y)

source

@[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.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).map f) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp f h)

source

@[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.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) f

source

@[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.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.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) (CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).map f) h)

source

@[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.obj n).map ((F.obj m).map f)) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).map f)

source

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.obj n).obj ((F.obj m).obj Y) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.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.MonoidalFunctor.μIso F m n).inv.app Y) h)

source

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.obj n).map ((F.obj m).map f)) = CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).map f) ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app Y)

source

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.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.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n').app X) h)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom f g)).app X) h)

source

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.map g).app ((F.obj m).obj X)) (CategoryTheory.CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n').app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) ((F.map (CategoryTheory.MonoidalCategory.tensorHom f g)).app X)

source

@[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.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.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id n))).app X) h)

source

@[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.obj n).map ((F.map f).app X)) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) ((F.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id n))).app X)

source

@[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.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.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n').app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X) h)

source

@[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.map g).app ((F.obj m).obj X)) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n').app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) ((F.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X)

source

@[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.obj n).obj ((F.obj m').obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id n))).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m' n).inv.app X) h)

source

@[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.obj n).map ((F.map f).app X)) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id n))).app X) ((CategoryTheory.MonoidalFunctor.μIso F m' n).inv.app X)

source

@[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.obj n').obj ((F.obj m).obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m n').inv.app X) h)

source

@[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.map g).app ((F.obj m).obj X)) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id m) g)).app X) ((CategoryTheory.MonoidalFunctor.μIso F m n').inv.app X)

source

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.obj n).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj n).map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit M) n).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X) h)) = h

source

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.obj n).map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit M) n).app X) ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X)) = CategoryTheory.CategoryStruct.id ((F.obj n).obj ((CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj X))

source

@[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.obj n).obj ((F.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj n).map (F.ε.app X)) h = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).inv).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorUnit M) n).inv.app X) h)

source

@[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.obj n).map (F.ε.app X) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorUnit M) n).inv.app X)

source

@[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.obj n).obj ((CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj n).map ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X)) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit M) n).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X) h)

source

@[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.obj n).map ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit M) n).app X) ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X)

source

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.obj n).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.ε.app ((F.obj n).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (CategoryTheory.MonoidalCategory.tensorUnit M)).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X) h)) = h

source

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.obj n).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (CategoryTheory.MonoidalCategory.tensorUnit M)).app X) ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C C)).obj ((F.obj n).obj X))

source

@[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.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F n (CategoryTheory.MonoidalCategory.tensorUnit M)).inv.app X)

source

@[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.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (CategoryTheory.MonoidalCategory.tensorUnit M)).app X) ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X)

source

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.obj (CategoryTheory.MonoidalCategory.tensorObj m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃))).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (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.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) h)

source

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

source

@[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.obj m₃).obj ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂)).obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X)) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor 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.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).inv.app X) h)))

source

@[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.obj m₃).map ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).inv.app X)))

source

@[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.obj m₃).obj ((CategoryTheory.MonoidalCategory.tensorObj (F.obj m₁) (F.obj m₂)).obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.MonoidalFunctor.μIso F m₁ m₂).inv.app X)) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (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.MonoidalFunctor.μIso F m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X)) h)))

source

@[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.obj m₃).map ((CategoryTheory.MonoidalFunctor.μIso F m₁ m₂).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (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.MonoidalFunctor.μIso F m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) ((CategoryTheory.MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X))))

source

@[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.obj m).obj Y) {Z : C} (h : (F.obj (CategoryTheory.MonoidalCategory.tensorObj m (CategoryTheory.MonoidalCategory.tensorUnit M))).obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).map f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (CategoryTheory.MonoidalCategory.tensorUnit M)).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.rightUnitor m).inv).app Y) h))

source

@[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.obj m).obj Y) :

CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorUnit M)).map f) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (CategoryTheory.MonoidalCategory.tensorUnit M)).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X) (CategoryTheory.CategoryStruct.comp f ((F.map (CategoryTheory.MonoidalCategory.rightUnitor m).inv).app Y))

source

@[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) :

source

@[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 ≅ CategoryTheory.MonoidalCategory.tensorUnit M) (X : C) :

(CategoryTheory.unitOfTensorIsoUnit F m n h).inv.app X = CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((F.map h.inv).app X) ((CategoryTheory.MonoidalFunctor.μIso F m n).inv.app X))

source

@[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 ≅ CategoryTheory.MonoidalCategory.tensorUnit M) (X : C) :

(CategoryTheory.unitOfTensorIsoUnit F m n h).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map h.hom).app X) ((CategoryTheory.MonoidalFunctor.εIso F).inv.app X))

source

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 ≅ CategoryTheory.MonoidalCategory.tensorUnit M) :

CategoryTheory.Functor.comp (F.obj m) (F.obj n) ≅ CategoryTheory.Functor.id C

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

Instances For

source

@[simp]

(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.obj n

source

@[simp]

(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).unitIso = (CategoryTheory.unitOfTensorIsoUnit F m n h₁).symm

source

@[simp]

(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.obj m

source

@[simp]

(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).counitIso = CategoryTheory.unitOfTensorIsoUnit F n m h₂

source

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.

Instances For