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 : C} {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 : CategoryTheory.Functor C C) (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 : 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)

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

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

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_ε_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.tensoringRightMonoidal C).ε.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 Y : C} (f : X ⟶ Y) (j : C), ((CategoryTheory.tensoringRightMonoidal C).map f).app j = CategoryTheory.MonoidalCategory.whiskerLeft j f

@[simp]

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

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_toFunctor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (k : C) (j : C) : ((CategoryTheory.tensoringRightMonoidal C).obj k).obj j = CategoryTheory.MonoidalCategory.tensorObj j k

@[simp]

theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_μ_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (X : C) : ((CategoryTheory.tensoringRightMonoidal C).μ X✝ Y).app X = (CategoryTheory.MonoidalCategory.associator X 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.obj i) (F.obj j)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.μ i j).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso 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.μ i j).app X) ((F.μIso i j).inv.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (F.obj i) (F.obj j)).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.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.μIso i j).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.μ 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 ((F.μIso i j).inv.app X) ((F.μ i j).app X) = CategoryTheory.CategoryStruct.id ((F.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).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)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp (F.εIso.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) (F.εIso.inv.app X) = CategoryTheory.CategoryStruct.id ((𝟙_ (CategoryTheory.Functor C C)).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.obj (𝟙_ M)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.εIso.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 (F.εIso.inv.app X) (F.ε.app X) = CategoryTheory.CategoryStruct.id ((F.obj (𝟙_ M)).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.obj (𝟙_ M)).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((F.obj (𝟙_ M)).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.obj (𝟙_ M)).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)).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) (CategoryTheory.CategoryStruct.comp ((𝟙_ (CategoryTheory.Functor C C)).map f) h) = CategoryTheory.CategoryStruct.comp (F.εIso.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 (F.εIso.inv.app X) ((𝟙_ (CategoryTheory.Functor C C)).map f) = CategoryTheory.CategoryStruct.comp (F.εIso.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.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) (CategoryTheory.CategoryStruct.comp ((F.μ m n).app Y) h) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).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.obj n).map ((F.obj m).map f)) ((F.μ m n).app Y) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).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.obj n).obj ((F.obj m).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.μIso 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 ((F.μIso 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 ((F.μIso 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) ((F.μIso 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.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 ((F.μ m' n').app X) h)) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.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.map g).app ((F.obj m).obj X)) (CategoryTheory.CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((F.μ m' n').app X)) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.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.obj (CategoryTheory.MonoidalCategory.tensorObj m' n)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) (CategoryTheory.CategoryStruct.comp ((F.μ m' n).app X) h) = CategoryTheory.CategoryStruct.comp ((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.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)) ((F.μ m' n).app X) = CategoryTheory.CategoryStruct.comp ((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.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 ((F.μ m n').app X) h) = CategoryTheory.CategoryStruct.comp ((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.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)) ((F.μ m n').app X) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.map (CategoryTheory.MonoidalCategory.whiskerLeft 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.obj n).obj ((F.obj m').obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.μIso 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.whiskerRight f n)).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso 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 ((F.μIso m n).inv.app X) ((F.obj n).map ((F.map f).app X)) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.whiskerRight f n)).app X) ((F.μIso 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.obj n').obj ((F.obj m).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.μIso 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.whiskerLeft m g)).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso 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 ((F.μIso m n).inv.app X) ((F.map g).app ((F.obj m).obj X)) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.whiskerLeft m g)).app X) ((F.μIso 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.obj n).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj n).map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((F.μ (𝟙_ M) n).app X) (CategoryTheory.CategoryStruct.comp ((F.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.obj n).map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((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))

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

@[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) ((F.μIso 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) : F.εIso.inv.app ((F.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((F.μ n (𝟙_ M)).app X) ((F.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.obj (CategoryTheory.MonoidalCategory.tensorObj m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃))).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((F.μ m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((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 ((F.μ m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.μ 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.obj m₃).map ((F.μ m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((F.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) ((F.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X)) = CategoryTheory.CategoryStruct.comp ((F.μ m₂ m₃).app ((F.obj m₁).obj X)) ((F.μ 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.obj m₃).obj ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂)).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((F.μ m₁ m₂).app X)) h = CategoryTheory.CategoryStruct.comp ((F.μ m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((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 ((F.μIso (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.obj m₃).map ((F.μ m₁ m₂).app X) = CategoryTheory.CategoryStruct.comp ((F.μ m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).inv).app X) ((F.μIso (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.obj m₃).obj ((CategoryTheory.MonoidalCategory.tensorObj (F.obj m₁) (F.obj m₂)).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((F.μIso m₁ m₂).inv.app X)) h = CategoryTheory.CategoryStruct.comp ((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 ((F.μIso m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.μIso m₂ m₃).inv.app ((F.obj m₁).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.obj m₃).map ((F.μIso m₁ m₂).inv.app X) = CategoryTheory.CategoryStruct.comp ((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 ((F.μIso m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) ((F.μIso m₂ m₃).inv.app ((F.obj m₁).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.obj m).obj Y) {Z : C} (h : (F.obj (CategoryTheory.MonoidalCategory.tensorObj m (𝟙_ M))).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj (𝟙_ M)).map f) (CategoryTheory.CategoryStruct.comp ((F.μ m (𝟙_ M)).app Y) h) = CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((F.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.obj m).obj Y) : CategoryTheory.CategoryStruct.comp ((F.obj (𝟙_ M)).map f) ((F.μ m (𝟙_ M)).app Y) = CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) (CategoryTheory.CategoryStruct.comp f ((F.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.μ (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ M) m₂)).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.associator m₁ (𝟙_ M) m₂).inv).app X) ((F.μIso (CategoryTheory.MonoidalCategory.tensorObj m₁ (𝟙_ M)) m₂).inv.app X))) = CategoryTheory.CategoryStruct.comp ((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)))

@[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.map h.inv).app X) ((F.μIso 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.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map h.hom).app X) (F.εIso.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) : (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 = F.μIso m n ≪≫ F.mapIso h ≪≫ F.εIso.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.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)) : (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.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)) : (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.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.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)) : (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.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)) : (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.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.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)) : 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.