CategoryTheory.MonoidalNatTrans.unit_assoc
theorem CategoryTheory.MonoidalNatTrans.unit_assoc :
∀ {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 G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) {Z : D}
(h : G.obj (𝟙_ C) ⟶ Z),
CategoryTheory.CategoryStruct.comp F.ε (CategoryTheory.CategoryStruct.comp (self.app (𝟙_ C)) h) =
CategoryTheory.CategoryStruct.comp G.ε h
The theorem `CategoryTheory.MonoidalNatTrans.unit_assoc` states that for any two lax monoidal functors `F` and `G` from a monoidal category `C` to another monoidal category `D`, and a monoidal natural transformation `self` from `F` to `G`, if we have a morphism `h` from the monoidal unit object of `G` to any object `Z` of `D`, then the composition of the unit morphism of `F`, `self` applied to the unit object of `C`, and `h` is equal to the composition of the unit morphism of `G` and `h`. This is a property of natural transformations between lax monoidal functors in category theory.
More concisely: For any lax monoidal functors F and G between monoidal categories C and D, and a monoidal natural transformation self from F to G, the composition of the unit morphism of F, self applied to the unit object of C, and any morphism h from the unit object of G to an object Z in D equals the composition of the unit morphism of G and h.
|
CategoryTheory.MonoidalNatTrans.tensor
theorem CategoryTheory.MonoidalNatTrans.tensor :
∀ {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 G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) (X Y : C),
CategoryTheory.CategoryStruct.comp (F.μ X Y) (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y))
(G.μ X Y)
The theorem `CategoryTheory.MonoidalNatTrans.tensor` is a statement about the tensor condition for a monoidal natural transformation in category theory. Given a category `C` with a monoidal structure and a category `D` also with a monoidal structure, as well as two lax monoidal functors `F` and `G` from `C` to `D` and a monoidal natural transformation `self` from `F` to `G`, this theorem states that for any objects `X` and `Y` in `C`, the composition of the monoidal structure of `F` applied to `X` and `Y` with the application of the natural transformation `self` to the tensor product of `X` and `Y` is equal to the composition of the tensor product of the application of `self` to `X` and `self` to `Y` with the monoidal structure of `G` applied to `X` and `Y`. This theorem hence captures an important property of tensoring in the context of monoidal categories and natural transformations.
More concisely: Given monoidal categories (C, ⊗\_C) and (D, ⊗\_D), lax monoidal functors F, G : C -> D, and a monoidal natural transformation self : F ⊗\_C Id -> Id ⊗\_D . G, the diagram commutes: (F(X) ⊗\_C F(Y)) ⊗\_D self(X, Y) ≈ self(F(X), F(Y)) ⊗\_D (G(X) ⊗\_D G(Y)).
|
CategoryTheory.MonoidalNatTrans.tensor_assoc
theorem CategoryTheory.MonoidalNatTrans.tensor_assoc :
∀ {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 G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) (X Y : C) {Z : D}
(h : G.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z),
CategoryTheory.CategoryStruct.comp (F.μ X Y)
(CategoryTheory.CategoryStruct.comp (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y))
(CategoryTheory.CategoryStruct.comp (G.μ X Y) h)
This theorem, `CategoryTheory.MonoidalNatTrans.tensor_assoc`, states that for any types `C` and `D` which are categories and monoidal categories, and any lax monoidal functors `F` and `G` from `C` to `D`, every monoidal natural transformation `self` from `F` to `G`, and any objects `X` and `Y` in `C` and object `Z` in `D` with a morphism `h` from `G` applied to the tensor product of `X` and `Y` to `Z`, the composition of the morphism `F.μ X Y` and the morphism from applying `self` to `X` tensor `Y` to `h` is equal to the composition of the tensor product of applying `self` to `X` and applying `self` to `Y` with the composition of `G.μ X Y` and `h`. In terms of category theory, this theorem is asserting the associativity of tensoring in the context of monoidal natural transformations.
More concisely: For any categories and monoidal categories C and D, lax monoidal functors F and G, monoidal natural transformation self from F to G, objects X, Y in C, and object Z in D with a morphism h from G(X) ⊗(C) Y to Z, we have F(μ X Y) ⊗(D) h = (G(μ X Y) ⊗ h) ∘ (self(X) ⊗ self(Y)).
|
CategoryTheory.MonoidalNatTrans.ext
theorem CategoryTheory.MonoidalNatTrans.ext :
∀ {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 G : CategoryTheory.LaxMonoidalFunctor C D} (x y : CategoryTheory.MonoidalNatTrans F G),
x.app = y.app → x = y
This theorem is a statement about category theory, specifically monoidal categories and natural transformations. It states that for any two categories `C` and `D`, where `C` and `D` are both monoidal categories, and for any two lax monoidal functors `F` and `G` from `C` to `D`, if we have two monoidal natural transformations `x` and `y` from `F` to `G`, then if the application function (`app`) of `x` is equal to the application function of `y`, `x` and `y` must be the same. In other words, a monoidal natural transformation is determined by its application function.
More concisely: If `F` and `G` are lax monoidal functors between monoidal categories `C` and `D`, and `x` and `y` are monoidal natural transformations from `F` to `G` with equal application functions, then `x = y`.
|
CategoryTheory.MonoidalNatTrans.unit
theorem CategoryTheory.MonoidalNatTrans.unit :
∀ {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 G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G),
CategoryTheory.CategoryStruct.comp F.ε (self.app (𝟙_ C)) = G.ε
This theorem is about the unit condition for a monoidal natural transformation in category theory. Specifically, it states that for any categories `C` and `D` equipped with monoidal structures, and for any lax monoidal functors `F, G` from `C` to `D`, if there is a monoidal natural transformation `self` from `F` to `G`, then the composition of the unit (or identity) morphism of `F` and the application of `self` to the identity object of `C` equals to the unit morphism of `G`. In other words, for all such settings, we have `F.ε ≫ self.app (𝟙_ C) = G.ε`, where `≫` denotes composition of morphisms, and `𝟙_ C` denotes the identity object in the category `C`.
More concisely: For any lax monoidal functors F, G between monoidal categories C and D, and any monoidal natural transformation self from F to G, the compositions of the identity morphisms of F and self applied to the identity object of C equal the identity morphism of G. That is, F.ε ≫ self.app (id\_C) = G.ε.
|