Mathlib.CategoryTheory.Monoidal.Functor._auxLemma.2
theorem Mathlib.CategoryTheory.Monoidal.Functor._auxLemma.2 :
ā {C : Type u} [š : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (X : C) {Yā Yā : C}
(f : Yā ā¶ Yā),
CategoryTheory.MonoidalCategory.whiskerLeft X f =
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f
This theorem in the field of category theory states that for any category `C` which is also a monoidal category, and for any objects `X`, `Yā`, `Yā` in `C`, and a morphism `f` from `Yā` to `Yā`, the left whiskering of `f` with `X` (which is the act of pre-composing each morphism in the functor category with `f`) is equal to the tensor product of the identity morphism on `X` and the morphism `f`. This theorem thus provides a relation between the concepts of left whiskering and tensor product in the context of a monoidal category.
More concisely: In a monoidal category, for any object X and morphism f, the left whiskering of f with X is equal to the tensor product of the identity morphism on X and f.
|
CategoryTheory.LaxMonoidalFunctor.associativity
theorem CategoryTheory.LaxMonoidalFunctor.associativity :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{D : Type uā} [inst_2 : CategoryTheory.Category.{vā, uā} D] [inst_3 : CategoryTheory.MonoidalCategory D]
(self : CategoryTheory.LaxMonoidalFunctor C D) (X Y Z : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.Ī¼ X Y) (self.obj Z))
(CategoryTheory.CategoryStruct.comp (self.Ī¼ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)
(self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.Ī¼ Y Z))
(self.Ī¼ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
This theorem, named `CategoryTheory.LaxMonoidalFunctor.associativity`, states the associativity property for a Lax monoidal functor between two monoidal categories.
Given two categories `C` and `D` with monoidal structures, and a Lax monoidal functor `self` from `C` to `D`, for any three objects `X`, `Y` and `Z` in `C`, the composition of the functor's morphisms from `X ā Y` to `Z` and from `X` to `Y ā Z` is equal to the composition of the associator in `D` and the functor's morphisms from `X` to `Y` and from `Y` to `Z ā X`.
In mathematical terms, `(self.Ī¼ X Y) ā Z ā (X ā Y) ā Z ā X ā (Y ā Z) = Ī±_D(X,Y,Z) ā X ā (self.Ī¼ Y Z) ā self.Ī¼ X (Y ā Z)`, where `Ī±_D` is the associator in `D`, `ā` denotes the tensor product, and `self.Ī¼` is the morphism mapped by the functor.
More concisely: For any Lax monoidal functor `self` between monoidal categories `C` and `D`, and objects `X, Y, Z` in `C`, the composition of `self.Ī¼(X ā Y) ā Z ā X ā (Y ā Z)` equals the composition of `Ī±_D(X,Y,Z) ā X ā self.Ī¼(Y ā Z)`.
|
Mathlib.CategoryTheory.Monoidal.Functor._auxLemma.1
theorem Mathlib.CategoryTheory.Monoidal.Functor._auxLemma.1 :
ā {C : Type u} [š : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {Xā Xā : C}
(f : Xā ā¶ Xā) (Y : C),
CategoryTheory.MonoidalCategory.whiskerRight f Y =
CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)
This theorem, named `Mathlib.CategoryTheory.Monoidal.Functor._auxLemma.1`, is a statement about Monoidal Categories in Category Theory. For any type `C` that forms a category `š` and a Monoidal Category `inst`, and for any two objects `Xā` and `Xā` in `C` with a morphism `f` from `Xā` to `Xā`, and any object `Y` in `C`, the result of whiskering on the right by `f` on `Y` is equal to the tensor product of the morphism `f` and the identity morphism on `Y`. The equality here is in terms of morphisms in the Monoidal Category `C`. This theorem asserts that these two ways of manipulating morphisms and objects in a monoidal category are equivalent.
More concisely: For any Monoidal Category `C` with type `š`, object `Xā`, object `Xā`, morphism `f : Xā ā Xā`, and object `Y` in `C`, the right whiskering of `f` on `Y` is equal to the tensor product of `f` and the identity morphism on `Y`.
|
CategoryTheory.LaxMonoidalFunctor.Ī¼_natural
theorem CategoryTheory.LaxMonoidalFunctor.Ī¼_natural :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{D : Type uā} [inst_2 : CategoryTheory.Category.{vā, uā} D] [inst_3 : CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.LaxMonoidalFunctor C D) {X Y X' Y' : C} (f : X ā¶ Y) (g : X' ā¶ Y'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (F.Ī¼ Y Y') =
CategoryTheory.CategoryStruct.comp (F.Ī¼ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))
This theorem, `CategoryTheory.LaxMonoidalFunctor.Ī¼_natural`, states that for any two objects `X`, `X'`, `Y`, and `Y'` in a category `C` that has a monoidal category structure, and any two morphisms `f : X ā¶ Y` and `g : X' ā¶ Y'` in `C`, for a lax monoidal functor `F` from `C` to a category `D` that also has a monoidal category structure, the composition of the tensor product of the mappings of `f` and `g` with the `Ī¼` function of `F` applied to `Y` and `Y'` is equal to the composition of the `Ī¼` function of `F` applied to `X` and `X'` with the mapping of the tensor product of `f` and `g`. In terms of category theory, this asserts a form of coherence between the `Ī¼` function, the mapping function of `F`, and the composition and tensor product operations, which is a crucial property for lax monoidal functors.
More concisely: For any lax monoidal functor F between monoidal categories, and objects X, X', Y, and Y' with morphisms f : X ā¶ Y and g : X' ā¶ Y' in the source category, the diagram commutes: Ī¼F(Y, Y') ā (F(f) ā F(g)) ā” F(f ā g) ā Ī¼F(X, X').
|