mathlib3 documentation

category_theory.monoidal.End

Endofunctors as a monoidal category. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[simp]
theorem category_theory.obj_μ_inv_app {C : Type u} [category_theory.category C] {M : Type u_1} [category_theory.category M] [category_theory.monoidal_category M] (F : category_theory.monoidal_functor M (C C)) (m₁ m₂ m₃ : M) (X : C) :
(F.to_lax_monoidal_functor.to_functor.obj m₃).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)
noncomputable def category_theory.equiv_of_tensor_iso_unit {C : Type u} [category_theory.category C] {M : Type u_1} [category_theory.category M] [category_theory.monoidal_category M] (F : category_theory.monoidal_functor M (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