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

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
Instances For
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj (C : Type u) (X : C) :
(𝟙_ ()).obj X = X
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map (C : Type u) {X : C} {Y : C} (f : X Y) :
(𝟙_ ()).map f = f
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj (C : Type u) (F : ) (G : ) (X : C) :
X = G.obj (F.obj X)
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_map (C : Type u) (F : ) (G : ) {X : C} {Y : C} (f : X Y) :
f = G.map (F.map f)
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_tensorMap_app (C : Type u) {F : } {G : } {H : } {K : } {α : F G} {β : H K} (X : C) :
X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (K.map (α.app X))
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_whiskerLeft_app (C : Type u) {F : } {H : } {K : } {β : H K} (X : C) :
X = β.app (F.obj X)
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_whiskerRight_app (C : Type u) {F : } {G : } {H : } {α : F G} (X : C) :
X = H.map (α.app X)
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_associator_hom_app (C : Type u) (F : ) (G : ) (H : ) (X : C) :
.hom.app X =
@[simp]
theorem CategoryTheory.endofunctorMonoidalCategory_associator_inv_app (C : Type u) (F : ) (G : ) (H : ) (X : C) :
.inv.app X =
@[simp]
theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_toFunctor_map_app (C : Type u) :
∀ {X Y : C} (f : X Y) (j : C), ().app j =
@[simp]
theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_toFunctor_obj_map (C : Type u) (k : C) :
∀ {X Y : C} (f : X Y), ().map f =
@[simp]
theorem CategoryTheory.tensoringRightMonoidal_toLaxMonoidalFunctor_μ_app (C : Type u) (X : C) (Y : C) (X : C) :
().app X = .hom

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.
Instances For
@[simp]
theorem CategoryTheory.μ_hom_inv_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (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} {M : Type u_1} [] (F : ) (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} {M : Type u_1} [] (F : ) (i : M) (j : M) (X : C) {Z : C} (h : (F.obj ).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} {M : Type u_1} [] (F : ) (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 ).obj X)
@[simp]
theorem CategoryTheory.ε_hom_inv_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (X : C) {Z : C} (h : (𝟙_ ()).obj X Z) :
@[simp]
theorem CategoryTheory.ε_hom_inv_app {C : Type u} {M : Type u_1} [] (F : ) (X : C) :
CategoryTheory.CategoryStruct.comp (F.app X) (F.εIso.inv.app X) = CategoryTheory.CategoryStruct.id ((𝟙_ ()).obj X)
@[simp]
theorem CategoryTheory.ε_inv_hom_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (X : C) {Z : C} (h : (F.obj (𝟙_ M)).obj X Z) :
@[simp]
theorem CategoryTheory.ε_inv_hom_app {C : Type u} {M : Type u_1} [] (F : ) (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} {M : Type u_1} [] (F : ) {X : C} {Y : C} (f : X Y) {Z : C} (h : (F.obj (𝟙_ M)).obj Y Z) :
@[simp]
theorem CategoryTheory.ε_naturality {C : Type u} {M : Type u_1} [] (F : ) {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} {M : Type u_1} [] (F : ) {X : C} {Y : C} (f : X Y) {Z : C} (h : (𝟙_ ()).obj Y Z) :
@[simp]
theorem CategoryTheory.ε_inv_naturality {C : Type u} {M : Type u_1} [] (F : ) {X : C} {Y : C} (f : X Y) :
CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) ((𝟙_ ()).map f) = CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) f
@[simp]
theorem CategoryTheory.μ_naturality_assoc {C : Type u} {M : Type u_1} [] (F : ) {m : M} {n : M} {X : C} {Y : C} (f : X Y) {Z : C} (h : (F.obj ).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 ).map f) h)
@[simp]
theorem CategoryTheory.μ_naturality {C : Type u} {M : Type u_1} [] (F : ) {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 ).map f)
theorem CategoryTheory.μ_inv_naturality_assoc {C : Type u} {M : Type u_1} [] (F : ) {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 ).map f) (CategoryTheory.CategoryStruct.comp ((F.μIso m n).inv.app Y) h)
theorem CategoryTheory.μ_inv_naturality {C : Type u} {M : Type u_1} [] (F : ) {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 ).map f) ((F.μIso m n).inv.app Y)
theorem CategoryTheory.μ_naturality₂_assoc {C : Type u} {M : Type u_1} [] (F : ) {m : M} {n : M} {m' : M} {n' : M} (f : m m') (g : n n') (X : C) {Z : C} (h : (F.obj ).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 ).app X) h)
theorem CategoryTheory.μ_naturality₂ {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X)
@[simp]
theorem CategoryTheory.μ_naturalityₗ_assoc {C : Type u} {M : Type u_1} [] (F : ) {m : M} {n : M} {m' : M} (f : m m') (X : C) {Z : C} (h : (F.obj ).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 ).app X) h)
@[simp]
theorem CategoryTheory.μ_naturalityₗ {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X)
@[simp]
theorem CategoryTheory.μ_naturalityᵣ_assoc {C : Type u} {M : Type u_1} [] (F : ) {m : M} {n : M} {n' : M} (g : n n') (X : C) {Z : C} (h : (F.obj ).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 ).app X) h)
@[simp]
theorem CategoryTheory.μ_naturalityᵣ {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X)
@[simp]
theorem CategoryTheory.μ_inv_naturalityₗ_assoc {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso m' n).inv.app X) h)
@[simp]
theorem CategoryTheory.μ_inv_naturalityₗ {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X) ((F.μIso m' n).inv.app X)
@[simp]
theorem CategoryTheory.μ_inv_naturalityᵣ_assoc {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso m n').inv.app X) h)
@[simp]
theorem CategoryTheory.μ_inv_naturalityᵣ {C : Type u} {M : Type u_1} [] (F : ) {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 ).app X) ((F.μIso m n').inv.app X)
theorem CategoryTheory.left_unitality_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (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 ).app X) h)) = h
theorem CategoryTheory.left_unitality_app {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) :
CategoryTheory.CategoryStruct.comp ((F.obj n).map (F.app X)) (CategoryTheory.CategoryStruct.comp ((F (𝟙_ M) n).app X) ((F.map ).app X)) = CategoryTheory.CategoryStruct.id ((F.obj n).obj ((𝟙_ ()).obj X))
@[simp]
theorem CategoryTheory.obj_ε_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (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 ).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso (𝟙_ M) n).inv.app X) h)
@[simp]
theorem CategoryTheory.obj_ε_app {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) :
(F.obj n).map (F.app X) = CategoryTheory.CategoryStruct.comp ((F.map ).app X) ((F.μIso (𝟙_ M) n).inv.app X)
@[simp]
theorem CategoryTheory.obj_ε_inv_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) {Z : C} (h : (F.obj n).obj ((𝟙_ ()).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 ).app X) h)
@[simp]
theorem CategoryTheory.obj_ε_inv_app {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) :
(F.obj n).map (F.εIso.inv.app X) = CategoryTheory.CategoryStruct.comp ((F (𝟙_ M) n).app X) ((F.map ).app X)
theorem CategoryTheory.right_unitality_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (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 ).app X) h)) = h
theorem CategoryTheory.right_unitality_app {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) :
CategoryTheory.CategoryStruct.comp (F.app ((F.obj n).obj X)) (CategoryTheory.CategoryStruct.comp ((F n (𝟙_ M)).app X) ((F.map ).app X)) = CategoryTheory.CategoryStruct.id ((𝟙_ ()).obj ((F.obj n).obj X))
@[simp]
theorem CategoryTheory.ε_app_obj {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) :
F.app ((F.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((F.map ).app X) ((F.μIso n (𝟙_ M)).inv.app X)
@[simp]
theorem CategoryTheory.ε_inv_app_obj {C : Type u} {M : Type u_1} [] (F : ) (n : M) (X : C) :
F.εIso.inv.app ((F.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((F n (𝟙_ M)).app X) ((F.map ).app X)
theorem CategoryTheory.associativity_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) {Z : C} (h : ().obj X Z) :
CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((F m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((F m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.map ().hom).app X) h)) = CategoryTheory.CategoryStruct.comp ((F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F m₁ ).app X) h)
theorem CategoryTheory.associativity_app {C : Type u} {M : Type u_1} [] (F : ) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) :
CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((F m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((F m₃).app X) ((F.map ().hom).app X)) = CategoryTheory.CategoryStruct.comp ((F m₂ m₃).app ((F.obj m₁).obj X)) ((F m₁ ).app X)
@[simp]
theorem CategoryTheory.obj_μ_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) {Z : C} (h : (F.obj m₃).obj ((F.obj ).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₁ ).app X) (CategoryTheory.CategoryStruct.comp ((F.map ().inv).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso m₃).inv.app X) h)))
@[simp]
theorem CategoryTheory.obj_μ_app {C : Type u} {M : Type u_1} [] (F : ) (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₁ ).app X) (CategoryTheory.CategoryStruct.comp ((F.map ().inv).app X) ((F.μIso m₃).inv.app X)))
@[simp]
theorem CategoryTheory.obj_μ_inv_app_assoc {C : Type u} {M : Type u_1} [] (F : ) (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 m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.map ().hom).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso 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} {M : Type u_1} [] (F : ) (m₁ : M) (m₂ : M) (m₃ : M) (X : C) :
(F.obj m₃).map ((F.μIso m₁ m₂).inv.app X) = CategoryTheory.CategoryStruct.comp ((F m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.map ().hom).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso 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} {M : Type u_1} [] (F : ) {m : M} {X : C} {Y : C} (f : X (F.obj m).obj Y) {Z : C} (h : (F.obj ()).obj Y Z) :
@[simp]
theorem CategoryTheory.obj_zero_map_μ_app {C : Type u} {M : Type u_1} [] (F : ) {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 ).app Y))
@[simp]
theorem CategoryTheory.obj_μ_zero_app {C : Type u} {M : Type u_1} [] (F : ) (m₁ : M) (m₂ : M) (X : C) :
CategoryTheory.CategoryStruct.comp ((F (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F m₁ ()).app X) (CategoryTheory.CategoryStruct.comp ((F.map ().inv).app X) ((F.μIso () m₂).inv.app X))) = CategoryTheory.CategoryStruct.comp ((F (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.map ).app ((F.obj m₁).obj X)) ((F.obj m₂).map ((F.map ).app X)))
@[simp]
theorem CategoryTheory.unitOfTensorIsoUnit_inv_app {C : Type u} {M : Type u_1} [] (F : ) (m : M) (n : M) (h : ) (X : C) :
().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} {M : Type u_1} [] (F : ) (m : M) (n : M) (h : ) (X : C) :
().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} {M : Type u_1} [] (F : ) (m : M) (n : M) (h : ) :
(F.obj m).comp (F.obj n)

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

Equations
• = (F.μIso m n).trans ((F.mapIso h).trans F.εIso.symm)
Instances For
@[simp]
theorem CategoryTheory.equivOfTensorIsoUnit_counitIso {C : Type u} {M : Type u_1} [] (F : ) (m : M) (n : M) (h₁ : ) (h₂ : ) (H : ) :
().counitIso =
@[simp]
theorem CategoryTheory.equivOfTensorIsoUnit_inverse {C : Type u} {M : Type u_1} [] (F : ) (m : M) (n : M) (h₁ : ) (h₂ : ) (H : ) :
().inverse = F.obj n
@[simp]
theorem CategoryTheory.equivOfTensorIsoUnit_unitIso {C : Type u} {M : Type u_1} [] (F : ) (m : M) (n : M) (h₁ : ) (h₂ : ) (H : ) :
().unitIso = ().symm
@[simp]
theorem CategoryTheory.equivOfTensorIsoUnit_functor {C : Type u} {M : Type u_1} [] (F : ) (m : M) (n : M) (h₁ : ) (h₂ : ) (H : ) :
().functor = F.obj m
noncomputable def CategoryTheory.equivOfTensorIsoUnit {C : Type u} {M : Type u_1} [] (F : ) (m : M) (n : M) (h₁ : ) (h₂ : ) (H : ) :
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.
Instances For