CategoryTheory.LaxMonoidal.right_unitality
theorem CategoryTheory.LaxMonoidal.right_unitality :
∀ {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 : C → D} [inst_4 : CategoryTheory.Functorial F] [self : CategoryTheory.LaxMonoidal F] (X : C),
(CategoryTheory.MonoidalCategory.rightUnitor (F X)).hom =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft (F X) CategoryTheory.LaxMonoidal.ε)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ X (𝟙_ C))
(CategoryTheory.map F (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
This theorem, referred to as "right unitality", establishes a property of lax monoidal functors between two monoidal categories. In particular, for any object `X` in category `C` and a functor `F` from `C` to `D`, it states that the right unitor morphism for `(F X)` in category `D` is equivalent to the composition of a certain sequence of morphisms involving the unit natural transformation `ε`, the multiplication natural transformation `μ`, and the image of the right unitor for `X` under `F`. This is an identity often required in the theory of monoidal categories and lax monoidal functors.
More concisely: The right unitor morphism of a lax monoidal functor `F` from category `C` to category `D` for object `X` in `C` is equivalent to the composition of `F(ιx)`, `μ(X, F(X), F(X))`, and `F(ρx)`.
|
CategoryTheory.LaxMonoidal.associativity
theorem CategoryTheory.LaxMonoidal.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]
{F : C → D} [inst_4 : CategoryTheory.Functorial F] [self : CategoryTheory.LaxMonoidal F] (X Y Z : C),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.LaxMonoidal.μ X Y) (F Z))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)
(CategoryTheory.map F (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F X) (F Y) (F Z)).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft (F X) (CategoryTheory.LaxMonoidal.μ Y Z))
(CategoryTheory.LaxMonoidal.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
This theorem, called `CategoryTheory.LaxMonoidal.associativity`, is about the associativity property in the context of category theory, specifically for lax monoidal functors. Given two categories `C` and `D`, both equipped with monoidal structures, and a functor `F` from `C` to `D` that is also lax monoidal, for any three objects `X`, `Y`, `Z` in `C`, the theorem asserts that two certain complex compositions of morphisms are equal. More specifically, the composition of the 'tensoring' of the functor `F` with the 'associator' in `C`, followed by the 'associator' in `D` and the 'tensoring' of `F`, is the same as the composition of the 'associator' in `C` followed by the 'tensoring' of the functor `F` with the 'associator' in `D`. The associator here is a specific isomorphism in a monoidal category which expresses the associativity of the tensor product.
More concisely: Given two lax monoidal functors between monoidal categories, the composition of their associators with the tensoring of the functor is equal to the composition of the tensoring of the functor with the associators.
|
CategoryTheory.LaxMonoidal.left_unitality
theorem CategoryTheory.LaxMonoidal.left_unitality :
∀ {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 : C → D} [inst_4 : CategoryTheory.Functorial F] [self : CategoryTheory.LaxMonoidal F] (X : C),
(CategoryTheory.MonoidalCategory.leftUnitor (F X)).hom =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.LaxMonoidal.ε (F X))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ (𝟙_ C) X)
(CategoryTheory.map F (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
This theorem, referred to as "left unitality", states that for any categories `C` and `D` that have monoidal structures, and any functor `F` from `C` to `D` that is equipped with a structure of a lax monoidal functor, the morphism corresponding to the left unit of the monoidal structure on `F(X)` (where `X` is an object in `C`) can be expressed as a composition of three other morphisms: first, the whiskering of the unit natural transformation of the lax monoidal functor `F` with `F(X)`; then, the morphism associated with the lax monoidal functor applied to the unit of `C` and `X`; and finally, the morphism obtained by applying `F` to the left unit morphism in `C` at `X`. This is a condition that is expected to hold in any monoidal category and is often used in the study of monoidal categories and functors between them.
More concisely: For any lax monoidal functor F between monoidal categories C and D, the left unit of F(X) can be expressed as the composition of whiskering F's unit transformation with F(1\_C(X)), and F(1\_C) applied to X, followed by F(1\_C(X)).
|