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.

source

def CategoryTheory.endofunctorMonoidalCategory (C : Type u) [Category.{v, u} C] :

MonoidalCategory (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).

Note: due to the fact that composition of functors in mathlib is reversed compared to the one usually found in the literature, this monoidal structure is in fact the monoidal opposite of the one usually considered in the literature.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj (C : Type u) [Category.{v, u} C] (X : C) :

(MonoidalCategoryStruct.tensorUnit (Functor C C)).obj X = X

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map (C : Type u) [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) :

(MonoidalCategoryStruct.tensorUnit (Functor C C)).map f = f

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj (C : Type u) [Category.{v, u} C] (F G : Functor C C) (X : C) :

(MonoidalCategoryStruct.tensorObj F G).obj X = G.obj (F.obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_map (C : Type u) [Category.{v, u} C] (F G : Functor C C) {X Y : C} (f : X ⟶ Y) :

(MonoidalCategoryStruct.tensorObj F G).map f = G.map (F.map f)

source

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

(MonoidalCategoryStruct.tensorHom α β).app X = CategoryStruct.comp (β.app (F.obj X)) (K.map (α.app X))

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_whiskerLeft_app (C : Type u) [Category.{v, u} C] {F H K : Functor C C} {β : H ⟶ K} (X : C) :

(MonoidalCategoryStruct.whiskerLeft F β).app X = β.app (F.obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_whiskerRight_app (C : Type u) [Category.{v, u} C] {F G H : Functor C C} {α : F ⟶ G} (X : C) :

(MonoidalCategoryStruct.whiskerRight α H).app X = H.map (α.app X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_associator_hom_app (C : Type u) [Category.{v, u} C] (F G H : Functor C C) (X : C) :

(MonoidalCategoryStruct.associator F G H).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj F G) H).obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_associator_inv_app (C : Type u) [Category.{v, u} C] (F G H : Functor C C) (X : C) :

(MonoidalCategoryStruct.associator F G H).inv.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj F (MonoidalCategoryStruct.tensorObj G H)).obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_hom_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) :

(MonoidalCategoryStruct.leftUnitor F).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (Functor C C)) F).obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) :

(MonoidalCategoryStruct.leftUnitor F).inv.app X = CategoryStruct.id (F.obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_rightUnitor_hom_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) :

(MonoidalCategoryStruct.rightUnitor F).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj F (MonoidalCategoryStruct.tensorUnit (Functor C C))).obj X)

source

@[simp]

theorem CategoryTheory.endofunctorMonoidalCategory_rightUnitor_inv_app (C : Type u) [Category.{v, u} C] (F : Functor C C) (X : C) :

(MonoidalCategoryStruct.rightUnitor F).inv.app X = CategoryStruct.id (F.obj X)

source

instance CategoryTheory.MonoidalCategory.instMonoidalFunctorTensoringRight (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :

(tensoringRight C).Monoidal

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.

source

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_ε (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :

Functor.LaxMonoidal.ε (tensoringRight C) = (rightUnitorNatIso C).inv

source

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_η (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :

Functor.OplaxMonoidal.η (tensoringRight C) = (rightUnitorNatIso C).hom

source

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_μ (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) :

(Functor.LaxMonoidal.μ (tensoringRight C) X Y).app Z = (associator Z X Y).hom

source

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_δ (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) :

(Functor.OplaxMonoidal.δ (tensoringRight C) X Y).app Z = (associator Z X Y).inv

source

@[simp]

theorem CategoryTheory.μ_δ_app {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)) (i j : M) (X : C) [F.Monoidal] :

CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) ((Functor.OplaxMonoidal.δ F i j).app X) = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X)

source

@[simp]

theorem CategoryTheory.μ_δ_app_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)) (i j : M) (X : C) [F.Monoidal] {Z : C} (h : (MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X ⟶ Z) :

CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) h) = h

source

@[simp]

theorem CategoryTheory.δ_μ_app {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)) (i j : M) (X : C) [F.Monoidal] :

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) ((Functor.LaxMonoidal.μ F i j).app X) = CategoryStruct.id ((F.obj (MonoidalCategoryStruct.tensorObj i j)).obj X)

source

@[simp]

theorem CategoryTheory.δ_μ_app_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)) (i j : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj i j)).obj X ⟶ Z) :

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) h) = h

source

@[simp]

theorem CategoryTheory.ε_η_app {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)) (X : C) [F.Monoidal] :

CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) ((Functor.OplaxMonoidal.η F).app X) = CategoryStruct.id ((MonoidalCategoryStruct.tensorUnit (Functor C C)).obj X)

source

@[simp]

theorem CategoryTheory.ε_η_app_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)) (X : C) [F.Monoidal] {Z : C} (h : (MonoidalCategoryStruct.tensorUnit (Functor C C)).obj X ⟶ Z) :

CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) h) = h

source

@[simp]

theorem CategoryTheory.η_ε_app {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)) (X : C) [F.Monoidal] :

CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) ((Functor.LaxMonoidal.ε F).app X) = CategoryStruct.id ((F.obj (MonoidalCategoryStruct.tensorUnit M)).obj X)

source

@[simp]

theorem CategoryTheory.η_ε_app_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)) (X : C) [F.Monoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorUnit M)).obj X ⟶ Z) :

CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) h) = h

source

@[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)) {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] :

CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) ((F.obj (MonoidalCategoryStruct.tensorUnit M)).map f) = CategoryStruct.comp f ((Functor.LaxMonoidal.ε F).app Y)

source

@[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)) {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorUnit M)).obj Y ⟶ Z) :

CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorUnit M)).map f) h) = CategoryStruct.comp f (CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app Y) h)

source

@[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)) {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] :

CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) ((MonoidalCategoryStruct.tensorUnit (Functor C C)).map f) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) f

source

@[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)) {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] {Z : C} (h : (MonoidalCategoryStruct.tensorUnit (Functor C C)).obj Y ⟶ Z) :

CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp ((MonoidalCategoryStruct.tensorUnit (Functor C C)).map f) h) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f h)

source

@[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} {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] :

CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) ((Functor.LaxMonoidal.μ F m n).app Y) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f)

source

@[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} {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m n)).obj Y ⟶ Z) :

CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app Y) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) h)

source

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} {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] :

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.obj n).map ((F.obj m).map f)) = CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) ((Functor.OplaxMonoidal.δ F m n).app Y)

source

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} {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] {Z : C} (h : (F.obj n).obj ((F.obj m).obj Y) ⟶ Z) :

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) h) = CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app Y) h)

source

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] :

CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((Functor.LaxMonoidal.μ F m' n').app X)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.tensorHom f g)).app X)

source

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) :

CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m' n').app X) h)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.tensorHom f g)).app X) h)

source

@[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' : M} (f : m ⟶ m') (X : C) [F.LaxMonoidal] :

CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) ((Functor.LaxMonoidal.μ F m' n).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X)

source

@[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.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m' n)).obj X ⟶ Z) :

CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m' n).app X) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) h)

source

@[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 n' : M} (g : n ⟶ n') (X : C) [F.LaxMonoidal] :

CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) ((Functor.LaxMonoidal.μ F m n').app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X)

source

@[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.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m n')).obj X ⟶ Z) :

CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n').app X) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) h)

source

@[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' : M} (f : m ⟶ m') (X : C) [F.OplaxMonoidal] :

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.obj n).map ((F.map f).app X)) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) ((Functor.OplaxMonoidal.δ F m' n).app X)

source

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

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) h) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m' n).app X) h)

source

@[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 n' : M} (g : n ⟶ n') (X : C) [F.OplaxMonoidal] :

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.map g).app ((F.obj m).obj X)) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) ((Functor.OplaxMonoidal.δ F m n').app X)

source

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

CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) h) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n').app X) h)

source

theorem CategoryTheory.left_unitality_app {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)) (n : M) (X : C) [F.LaxMonoidal] :

CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit M) n).app X) ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X)) = CategoryStruct.id ((F.obj n).obj ((MonoidalCategoryStruct.tensorUnit (Functor C C)).obj X))

source

theorem CategoryTheory.left_unitality_app_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)) (n : M) (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj n).obj X ⟶ Z) :

CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit M) n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X) h)) = h

source

@[simp]

theorem CategoryTheory.obj_ε_app {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)) (n : M) (X : C) [F.Monoidal] :

(F.obj n).map ((Functor.LaxMonoidal.ε F).app X) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).inv).app X) ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorUnit M) n).app X)

source

theorem CategoryTheory.obj_ε_app_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)) (n : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj n).obj ((F.obj (MonoidalCategoryStruct.tensorUnit M)).obj X) ⟶ Z) :

CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) h = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).inv).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorUnit M) n).app X) h)

source

@[simp]

theorem CategoryTheory.obj_η_app {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)) (n : M) (X : C) [F.Monoidal] :

(F.obj n).map ((Functor.OplaxMonoidal.η F).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit M) n).app X) ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X)

source

theorem CategoryTheory.obj_η_app_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)) (n : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj n).obj ((MonoidalCategoryStruct.tensorUnit (Functor C C)).obj X) ⟶ Z) :

CategoryStruct.comp ((F.obj n).map ((Functor.OplaxMonoidal.η F).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit M) n).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X) h)

source

theorem CategoryTheory.right_unitality_app {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)) (n : M) (X : C) [F.Monoidal] :

CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app ((F.obj n).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (MonoidalCategoryStruct.tensorUnit M)).app X) ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X)) = CategoryStruct.id ((MonoidalCategoryStruct.tensorUnit (Functor C C)).obj ((F.obj n).obj X))

source

theorem CategoryTheory.right_unitality_app_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)) (n : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj n).obj X ⟶ Z) :

CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app ((F.obj n).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (MonoidalCategoryStruct.tensorUnit M)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X) h)) = h

source

@[simp]

theorem CategoryTheory.ε_app_obj {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)) (n : M) (X : C) [F.Monoidal] :

(Functor.LaxMonoidal.ε F).app ((F.obj n).obj X) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor n).inv).app X) ((Functor.OplaxMonoidal.δ F n (MonoidalCategoryStruct.tensorUnit M)).app X)

source

@[simp]

theorem CategoryTheory.η_app_obj {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)) (n : M) (X : C) [F.Monoidal] :

(Functor.OplaxMonoidal.η F).app ((F.obj n).obj X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (MonoidalCategoryStruct.tensorUnit M)).app X) ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X)

source

theorem CategoryTheory.associativity_app {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₁ m₂ m₃ : M) (X : C) [F.LaxMonoidal] :

CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)

source

theorem CategoryTheory.associativity_app_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₁ m₂ m₃ : M) (X : C) [F.LaxMonoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃))).obj X ⟶ Z) :

CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) h)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) h)

source

@[simp]

theorem CategoryTheory.obj_μ_app {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₁ m₂ m₃ : M) (X : C) [F.Monoidal] :

(F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X) ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)))

source

theorem CategoryTheory.obj_μ_app_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₁ m₂ m₃ : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj m₃).obj ((F.obj (MonoidalCategoryStruct.tensorObj m₁ m₂)).obj X) ⟶ Z) :

CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) h)))

source

@[simp]

theorem CategoryTheory.obj_μ_inv_app {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₁ m₂ m₃ : M) (X : C) [F.Monoidal] :

(F.obj m₃).map ((Functor.OplaxMonoidal.δ F m₁ m₂).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) ((Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X))))

source

theorem CategoryTheory.obj_μ_inv_app_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₁ m₂ m₃ : M) (X : C) [F.Monoidal] {Z : C} (h : (F.obj m₃).obj ((MonoidalCategoryStruct.tensorObj (F.obj m₁) (F.obj m₂)).obj X) ⟶ Z) :

CategoryStruct.comp ((F.obj m₃).map ((Functor.OplaxMonoidal.δ F m₁ m₂).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X)) h)))

source

@[simp]

theorem CategoryTheory.obj_zero_map_μ_app {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 : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) [F.Monoidal] :

CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorUnit M)).map f) ((Functor.LaxMonoidal.μ F m (MonoidalCategoryStruct.tensorUnit M)).app Y) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f ((F.map (MonoidalCategoryStruct.rightUnitor m).inv).app Y))

source

@[simp]

theorem CategoryTheory.obj_zero_map_μ_app_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 : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) [F.Monoidal] {Z : C} (h : (F.obj (MonoidalCategoryStruct.tensorObj m (MonoidalCategoryStruct.tensorUnit M))).obj Y ⟶ Z) :

CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorUnit M)).map f) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m (MonoidalCategoryStruct.tensorUnit M)).app Y) h) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor m).inv).app Y) h))

source

@[simp]

theorem CategoryTheory.obj_μ_zero_app {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₁ m₂ : M) (X : C) [F.Monoidal] :

source

noncomputable def CategoryTheory.unitOfTensorIsoUnit {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) (h : MonoidalCategoryStruct.tensorObj m n ≅ MonoidalCategoryStruct.tensorUnit M) [F.Monoidal] :

(F.obj m).comp (F.obj n) ≅ 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 = CategoryTheory.Functor.Monoidal.μIso F m n ≪≫ F.mapIso h ≪≫ (CategoryTheory.Functor.Monoidal.εIso F).symm

Instances For

source

@[simp]

theorem CategoryTheory.unitOfTensorIsoUnit_inv_app {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) (h : MonoidalCategoryStruct.tensorObj m n ≅ MonoidalCategoryStruct.tensorUnit M) [F.Monoidal] (X : C) :

(unitOfTensorIsoUnit F m n h).inv.app X = CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((F.map h.inv).app X) ((Functor.OplaxMonoidal.δ F m n).app X))

source

@[simp]

theorem CategoryTheory.unitOfTensorIsoUnit_hom_app {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) (h : MonoidalCategoryStruct.tensorObj m n ≅ MonoidalCategoryStruct.tensorUnit M) [F.Monoidal] (X : C) :

(unitOfTensorIsoUnit F m n h).hom.app X = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) (CategoryStruct.comp ((F.map h.hom).app X) ((Functor.OplaxMonoidal.η F).app X))

source

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

source

@[simp]

(equivOfTensorIsoUnit F m n h₁ h₂ H).unitIso = (unitOfTensorIsoUnit F m n h₁).symm

source

@[simp]

(equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.obj m

source

@[simp]

(equivOfTensorIsoUnit F m n h₁ h₂ H).counitIso = unitOfTensorIsoUnit F n m h₂

source

@[simp]

(equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.obj n

Documentation

Mathlib.CategoryTheory.Monoidal.End

Endofunctors as a monoidal category. #

TODO #