Documentation

Mathlib.CategoryTheory.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
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.endofunctorMonoidalCategory_tensorMap_app (C : Type u) [Category.{v, u} C] {F G H K : Functor C C} {α : F G} {β : H K} (X : 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.μ_naturality₂ {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' n' : M} (f : m m') (g : n n') (X : C) [F.LaxMonoidal] :
    theorem CategoryTheory.μ_naturality₂_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' n' : M} (f : m m') (g : n n') (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m' n')).obj X Z) :
    @[simp]
    @[simp]
    @[simp]
    theorem CategoryTheory.δ_naturalityₗ_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n m' : M} (f : m m') (X : C) [F.OplaxMonoidal] {Z : C} (h : (F.obj n).obj ((F.obj m').obj X) Z) :
    @[simp]
    theorem CategoryTheory.δ_naturalityᵣ_assoc {C : Type u} [Category.{v, u} C] {M : Type u_1} [Category.{u_2, u_1} M] [MonoidalCategory M] (F : Functor M (Functor C C)) {m n n' : M} (g : n n') (X : C) [F.OplaxMonoidal] {Z : C} (h : (F.obj n').obj ((F.obj m).obj X) Z) :

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

    Equations
    Instances For

      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