# mathlibdocumentation

category_theory.monoidal.End

# 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

Tensoring on the right gives a monoidal functor from C into endofunctors of C.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.μ_hom_inv_app {C : Type u} {M : Type u_1} (F : (C C)) (i j : M) (X : C) :
j).app X (F.μ_iso i j).inv.app X = 𝟙 X)
@[simp]
theorem category_theory.μ_hom_inv_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (i j : M) (X : C) {X' : C} (f' : X') :
j).app X (F.μ_iso i j).inv.app X f' = f'
@[simp]
theorem category_theory.μ_inv_hom_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (i j : M) (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (i j)).obj X X') :
(F.μ_iso i j).inv.app X j).app X f' = f'
@[simp]
theorem category_theory.μ_inv_hom_app {C : Type u} {M : Type u_1} (F : (C C)) (i j : M) (X : C) :
@[simp]
theorem category_theory.ε_hom_inv_app {C : Type u} {M : Type u_1} (F : (C C)) (X : C) :
F.ε_iso.inv.app X = 𝟙 ((𝟙_ (C C)).obj X)
@[simp]
theorem category_theory.ε_hom_inv_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (X : C) {X' : C} (f' : (𝟙_ (C C)).obj X X') :
F.ε_iso.inv.app X f' = f'
@[simp]
theorem category_theory.ε_inv_hom_app {C : Type u} {M : Type u_1} (F : (C C)) (X : C) :
@[simp]
theorem category_theory.ε_inv_hom_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj X X') :
F.ε_iso.inv.app X f' = f'
@[simp]
theorem category_theory.ε_naturality_assoc {C : Type u} {M : Type u_1} (F : (C C)) {X Y : C} (f : X Y) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj Y X') :
@[simp]
theorem category_theory.ε_naturality {C : Type u} {M : Type u_1} (F : (C C)) {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.ε_inv_naturality {C : Type u} {M : Type u_1} (F : (C C)) {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.ε_inv_naturality_assoc {C : Type u} {M : Type u_1} (F : (C C)) {X Y : C} (f : X Y) {X' : C} (f' : (𝟙_ (C C)).obj Y X') :
@[simp]
theorem category_theory.μ_naturality {C : Type u} {M : Type u_1} (F : (C C)) {m n : M} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.μ_naturality_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n : M} {X Y : C} (f : X Y) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (m n)).obj Y X') :
.map f) n).app Y f' = n).app X (F.to_lax_monoidal_functor.to_functor.obj (m n)).map f f'
theorem category_theory.μ_inv_naturality {C : Type u} {M : Type u_1} (F : (C C)) {m n : M} {X Y : C} (f : X Y) :
theorem category_theory.μ_inv_naturality_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n : M} {X Y : C} (f : X Y) {X' : C} (f' : .obj Y) X') :
(F.μ_iso m n).inv.app X .map f) f' = (F.to_lax_monoidal_functor.to_functor.obj (m n)).map f (F.μ_iso m n).inv.app Y f'
theorem category_theory.μ_naturality₂_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n m' n' : M} (f : m m') (g : n n') (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (m' n')).obj X X') :
theorem category_theory.μ_naturality₂ {C : Type u} {M : Type u_1} (F : (C C)) {m n m' n' : M} (f : m m') (g : n n') (X : C) :
@[simp]
theorem category_theory.μ_naturalityₗ {C : Type u} {M : Type u_1} (F : (C C)) {m n m' : M} (f : m m') (X : C) :
@[simp]
theorem category_theory.μ_naturalityₗ_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n m' : M} (f : m m') (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (m' n)).obj X X') :
@[simp]
theorem category_theory.μ_naturalityᵣ {C : Type u} {M : Type u_1} (F : (C C)) {m n n' : M} (g : n n') (X : C) :
@[simp]
theorem category_theory.μ_naturalityᵣ_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n n' : M} (g : n n') (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (m n')).obj X X') :
.obj X) n').app X f' = n).app X (F.to_lax_monoidal_functor.to_functor.map (𝟙 m g)).app X f'
@[simp]
theorem category_theory.μ_inv_naturalityₗ {C : Type u} {M : Type u_1} (F : (C C)) {m n m' : M} (f : m m') (X : C) :
@[simp]
theorem category_theory.μ_inv_naturalityₗ_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n m' : M} (f : m m') (X : C) {X' : C} (f' : ((F.to_lax_monoidal_functor.to_functor.obj m').obj X) X') :
(F.μ_iso m n).inv.app X .app X) f' = (F.to_lax_monoidal_functor.to_functor.map (f 𝟙 n)).app X (F.μ_iso m' n).inv.app X f'
@[simp]
theorem category_theory.μ_inv_naturalityᵣ_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m n n' : M} (g : n n') (X : C) {X' : C} (f' : .obj .obj X) X') :
(F.μ_iso m n).inv.app X .obj X) f' = (F.to_lax_monoidal_functor.to_functor.map (𝟙 m g)).app X (F.μ_iso m n').inv.app X f'
@[simp]
theorem category_theory.μ_inv_naturalityᵣ {C : Type u} {M : Type u_1} (F : (C C)) {m n n' : M} (g : n n') (X : C) :
theorem category_theory.left_unitality_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) {X' : C} (f' : X X') :
theorem category_theory.left_unitality_app {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) :
theorem category_theory.obj_ε_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) {X' : C} (f' : ((F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj X) X') :
@[simp]
theorem category_theory.obj_ε_app {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) :
@[simp]
theorem category_theory.obj_ε_inv_app {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) :
theorem category_theory.obj_ε_inv_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) {X' : C} (f' : ((𝟙_ (C C)).obj X) X') :
theorem category_theory.right_unitality_app {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) :
theorem category_theory.right_unitality_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.ε_app_obj {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) :
@[simp]
theorem category_theory.ε_inv_app_obj {C : Type u} {M : Type u_1} (F : (C C)) (n : M) (X : C) :
theorem category_theory.associativity_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ m₃ : M) (X : C) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (m₁ m₂ m₃)).obj X X') :
.map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) (F.to_lax_monoidal_functor.μ (m₁ m₂) m₃).app X (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X f' = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) (F.to_lax_monoidal_functor.μ m₁ (m₂ m₃)).app X f'
theorem category_theory.associativity_app {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ m₃ : M) (X : C) :
theorem category_theory.obj_μ_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ m₃ : M) (X : C) {X' : C} (f' : .obj ((F.to_lax_monoidal_functor.to_functor.obj (m₁ m₂)).obj X) X') :
.map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) f' = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) (F.to_lax_monoidal_functor.μ m₁ (m₂ m₃)).app X (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).inv).app X (F.μ_iso (m₁ m₂) m₃).inv.app X f'
@[simp]
theorem category_theory.obj_μ_app {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ m₃ : M) (X : C) :
.map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) (F.to_lax_monoidal_functor.μ m₁ (m₂ m₃)).app X (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).inv).app X (F.μ_iso (m₁ m₂) m₃).inv.app X
theorem category_theory.obj_μ_inv_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ m₃ : M) (X : C) {X' : C} (f' : .obj .obj X) X') :
.map ((F.μ_iso m₁ m₂).inv.app X) f' = (F.to_lax_monoidal_functor.μ (m₁ m₂) m₃).app X (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X (F.μ_iso m₁ (m₂ m₃)).inv.app X (F.μ_iso m₂ m₃).inv.app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) f'
@[simp]
theorem category_theory.obj_μ_inv_app {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ m₃ : M) (X : C) :
.map ((F.μ_iso m₁ m₂).inv.app X) = (F.to_lax_monoidal_functor.μ (m₁ m₂) m₃).app X (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X (F.μ_iso m₁ (m₂ m₃)).inv.app X (F.μ_iso m₂ m₃).inv.app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X)
@[simp]
theorem category_theory.obj_zero_map_μ_app_assoc {C : Type u} {M : Type u_1} (F : (C C)) {m : M} {X Y : C} (f : X Y) {X' : C} (f' : (F.to_lax_monoidal_functor.to_functor.obj (m 𝟙_ M)).obj Y X') :
@[simp]
theorem category_theory.obj_zero_map_μ_app {C : Type u} {M : Type u_1} (F : (C C)) {m : M} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.obj_μ_zero_app {C : Type u} {M : Type u_1} (F : (C C)) (m₁ m₂ : M) (X : C) :
@[simp]
theorem category_theory.unit_of_tensor_iso_unit_hom_app {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h : m n 𝟙_ M) (X : C) :
.hom.app X = n).app X X F.ε_iso.inv.app X
noncomputable def category_theory.unit_of_tensor_iso_unit {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h : m n 𝟙_ M) :

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

Equations
@[simp]
theorem category_theory.unit_of_tensor_iso_unit_inv_app {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h : m n 𝟙_ M) (X : C) :
.inv.app X = X (F.μ_iso m n).inv.app X
noncomputable def category_theory.equiv_of_tensor_iso_unit {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h₁ : m n 𝟙_ M) (h₂ : n m 𝟙_ M) (H : (h₁.hom 𝟙 m) (λ_ m).hom = (α_ m n m).hom (𝟙 m h₂.hom) (ρ_ 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
• h₂ H =
@[simp]
theorem category_theory.equiv_of_tensor_iso_unit_unit_iso {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h₁ : m n 𝟙_ M) (h₂ : n m 𝟙_ M) (H : (h₁.hom 𝟙 m) (λ_ m).hom = (α_ m n m).hom (𝟙 m h₂.hom) (ρ_ m).hom) :
h₂ H).unit_iso = h₁).symm
@[simp]
theorem category_theory.equiv_of_tensor_iso_unit_functor {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h₁ : m n 𝟙_ M) (h₂ : n m 𝟙_ M) (H : (h₁.hom 𝟙 m) (λ_ m).hom = (α_ m n m).hom (𝟙 m h₂.hom) (ρ_ m).hom) :
h₂ H).functor =
@[simp]
theorem category_theory.equiv_of_tensor_iso_unit_counit_iso {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h₁ : m n 𝟙_ M) (h₂ : n m 𝟙_ M) (H : (h₁.hom 𝟙 m) (λ_ m).hom = (α_ m n m).hom (𝟙 m h₂.hom) (ρ_ m).hom) :
h₂ H).counit_iso =
@[simp]
theorem category_theory.equiv_of_tensor_iso_unit_inverse {C : Type u} {M : Type u_1} (F : (C C)) (m n : M) (h₁ : m n 𝟙_ M) (h₂ : n m 𝟙_ M) (H : (h₁.hom 𝟙 m) (λ_ m).hom = (α_ m n m).hom (𝟙 m h₂.hom) (ρ_ m).hom) :
h₂ H).inverse =