CategoryTheory.MonoidalCategory.associator_inv_naturality
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z'),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h))
(CategoryTheory.MonoidalCategory.associator X' Y' Z').inv =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h)
This theorem, `CategoryTheory.MonoidalCategory.associator_inv_naturality`, is a statement about the naturality of the inverse of the associator in a monoidal category. For any objects `X, Y, Z, X', Y', Z'` in a monoidal category `C` and morphisms `f : X ⟶ X'`, `g : Y ⟶ Y'`, and `h : Z ⟶ Z'`, the composition of the tensor product of `f` and the tensor product of `g` and `h` followed by the inverse of the associator of `X', Y', Z'` is equal to the composition of the inverse of the associator of `X, Y, Z` and the tensor product of the tensor product of `f` and `g` and `h`.
In mathematical terms, this corresponds to the following equality in the monoidal category `C`:
```
(f ⊗ (g ⊗ h)) ∘ α[X',Y',Z']⁻¹ = α[X,Y,Z]⁻¹ ∘ ((f ⊗ g) ⊗ h)
```
where `α[X,Y,Z]⁻¹` is the inverse of the associator of `X, Y, Z`, and `⊗` denotes the tensor product in the category.
More concisely: The inverse of the associator in a monoidal category is natural, i.e., for any objects X, Y, Z, X', Y', Z' and morphisms f : X ⟶ X', g : Y ⟶ Y', h : Z ⟶ Z', we have (f ⊗ (g ⊗ h)) ∘ α[X',Y',Z']⁻¹ = α[X,Y,Z]⁻¹ ∘ ((f ⊗ g) ⊗ h).
|
CategoryTheory.MonoidalCategory.tensor_comp
theorem CategoryTheory.MonoidalCategory.tensor_comp :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C]
{X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
(CategoryTheory.CategoryStruct.comp f₂ g₂) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂)
(CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)
This theorem states that in a monoidal category, the composition of tensor products is equivalent to the tensor product of compositions. More precisely, given any objects X₁, Y₁, Z₁, X₂, Y₂, Z₂ in a monoidal category C, and morphisms f₁ : X₁ ⟶ Y₁, f₂ : X₂ ⟶ Y₂, g₁ : Y₁ ⟶ Z₁, g₂ : Y₂ ⟶ Z₂, the tensor product of the compositions f₁ with g₁, and f₂ with g₂, is identical to the composition of the tensor product of f₁ with f₂, and g₁ with g₂. This can be represented as `(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)`.
More concisely: In a monoidal category, the tensor product of the compositions of morphisms is equal to the composition of their tensor products.
|
CategoryTheory.MonoidalCategory.id_whiskerLeft
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X Y : C}
(f : X ⟶ Y),
CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor Y).inv)
The theorem `CategoryTheory.MonoidalCategory.id_whiskerLeft` states that for any Category `C` (of type `Type u`) that is a Monoidal Category, and for any two objects `X` and `Y` in `C`, applying the `whiskerLeft` operation to the identity morphism (denoted `𝟙_ C`) and a given morphism `f` from `X` to `Y`, is equivalent to first applying the `hom` part of the `leftUnitor` to `X`, then composing that with the composition of `f` and the inverse (`inv`) of the `hom` part of the `leftUnitor` applied to `Y`. In essence, this theorem is about how the `whiskerLeft` operation interacts with the `leftUnitor` in a monoidal category.
More concisely: For any Monoidal Category `C`, the composition of the identity morphism with a morphism `f` via whisker composition is equal to the composition of the `hom` part of the left unitor at `X` with `f` followed by the inverse of the `hom` part of the left unitor at `Y`.
|
CategoryTheory.MonoidalCategory.inv_whiskerRight
theorem CategoryTheory.MonoidalCategory.inv_whiskerRight :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X Y : C}
(f : X ⟶ Y) (Z : C) [inst_1 : CategoryTheory.IsIso f],
CategoryTheory.inv (CategoryTheory.MonoidalCategory.whiskerRight f Z) =
CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv f) Z
This theorem states that in any monoidal category `C`, for any objects `X`, `Y` and `Z` in `C`, and any morphism `f` from `X` to `Y` that is an isomorphism, the inverse of the morphism obtained by whiskering `f` on the right with `Z` is equal to the morphism obtained by whiskering the inverse of `f` on the right with `Z`. In other words, the process of "whiskering" a morphism with another object is compatible with taking inverses of morphisms.
More concisely: In a monoidal category, whiskering an isomorphism with an object preserves inverse morphisms: for any objects X, Y, Z and isomorphism f : X ⟶ Y, the inverse of f ∘ tz for any morphism tz : Z ⟶ X is equal to the morphism s ∘ ft, where s : Y ⟶ Z is the inverse of f.
|
CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).inv Y =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv
(CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).inv
This theorem states that for any objects `X` and `Y` in a monoidal category `C`, the whisker right operation of the inverse of the left unitor of `X` with `Y` is the same as the composition of the inverse of the left unitor of the tensor product of `X` and `Y` and the inverse of the associator of the identity object with `X` and `Y`. In mathematical terms, this can be written as
\[
\eta_{X}^{-1} \circ Y = (\eta_{X \otimes Y}^{-1} \circ (1_{C} \otimes X \otimes Y)^{-1})
\]
Where `\eta_{X}` is the left unitor of `X`, `1_{C}` is the identity of `C`, and `\otimes` represents the tensor product operation.
More concisely: The inverse of the whisker right application of the left unitor of object `X` with `Y` equals the composition of the inverse of the left unitor of the tensor product of `X` and `Y`, and the inverse of the associator of the identity object with `X` and `Y`.
|
CategoryTheory.MonoidalCategory.triangle
theorem CategoryTheory.MonoidalCategory.triangle :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (X Y : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).hom
(CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) =
CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).hom Y
This theorem, known as the triangle theorem in monoidal category theory, states the following:
Given a category `C` with monoidal structure, and any two objects `X` and `Y` in `C`, the composite of the `associator` of `X`, the identity object `𝟙_ C` and `Y` with the `whiskerLeft` of `X` and the `leftUnitor` of `Y` is equal to the `whiskerRight` of the `rightUnitor` of `X` and `Y`.
In more intuitive terms, this theorem is about how identities behave under tensoring in a monoidal category. It asserts that certain sequences of tensoring and applying unitors (which are natural isomorphisms) are equal, capturing the interplay between the monoidal product and the identity object in the category. The 'triangle' in the theorem's name refers to the triangular diagram that this equality forms in the category.
More concisely: In a monoidal category, the composition of the associator, left unit, and object Y with the whisker left of X, is equal to the whisker right of the right unit and object Y for any objects X and Y.
|
CategoryTheory.MonoidalCategory.pentagon
theorem CategoryTheory.MonoidalCategory.pentagon :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (W X Y Z : C),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom
(CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom
(CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom
This theorem, also known as the pentagon identity, is a fundamental property in monoidal categories. Given a category `C`, assumed to be a monoidal category, and four objects `W`, `X`, `Y`, and `Z` in `C`, the theorem asserts the equality of two specific morphisms between the objects `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`. The first morphism is obtained by first applying the associator to `W`, `X`, `Y`, then whiskering with `Z` on the right, and finally composing with the compound morphism obtained by applying the associator to `W`, `X ⊗ Y`, `Z` and whiskering with `W` on the left on the associator on `X`, `Y`, `Z`. The second morphism is obtained by first applying the associator to `W ⊗ X`, `Y`, `Z` and then composing with the associator on `W`, `X`, `Y ⊗ Z`. This identity is one of the axioms that a monoidal category must satisfy.
More concisely: In a monoidal category, the morphisms from `X ⊗ (Y ⊗ Z)` to `((X ⊗ Y) ⊗ Z) ⊗ W` obtained by applying and composing associators are equal.
|
CategoryTheory.MonoidalCategory.whiskerLeft_eqToHom
theorem CategoryTheory.MonoidalCategory.whiskerLeft_eqToHom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
{Y Z : C} (f : Y = Z),
CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.eqToHom f) = CategoryTheory.eqToHom ⋯
This theorem states that in a monoidal category `C`, for any object `X` and any two objects `Y` and `Z` in `C` such that `Y = Z` (denoted by `f`), whiskering on the left by `X` to the morphism from `Y` to `Z` obtained from the equality `f` (using the `eqToHom` function) is the same as applying `eqToHom` to the relevant equality. In other words, `whiskerLeft` function commutes with the `eqToHom` function.
More concisely: In a monoidal category, whiskering on the left by an object X to the equality morphism between Y and Z is equal to applying the equality morphism to the identity morphism from Y to Z.
|
CategoryTheory.MonoidalCategory.whiskerLeft_comp
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (W : C) {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z),
CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W f)
(CategoryTheory.MonoidalCategory.whiskerLeft W g)
This theorem states that for any objects `W`, `X`, `Y`, and `Z` in a monoidal category `C`, the whisker left operation with a morphism `f` from `X` to `Y` and a morphism `g` from `Y` to `Z` is the composition of the whisker left operations with `f` and `g` respectively. In other words, the operation of whiskering on the left respects composition of morphisms.
In mathematical terms, if we take two morphisms `f: X ⟶ Y` and `g: Y ⟶ Z` in the category `C`, the whisker left operation applied to the composition `f ≫ g` is equal to the composition of the whisker left operation applied to `f` and the whisker left operation applied to `g`. The whisker left operation is a kind of "action" of the category on morphisms, changing them in a way that depends on another object `W`. This theorem says that this action respects the composition of morphisms.
More concisely: For any morphisms `f: X ⟶ Y` and `g: Y ⟶ Z` in a monoidal category `C`, the whisker left operation with their composition is equal to the composition of the whisker left operations with `f` and `g` respectively.
|
CategoryTheory.MonoidalCategory.tensorHom_id
theorem CategoryTheory.MonoidalCategory.tensorHom_id :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X₁ X₂ : C}
(f : X₁ ⟶ X₂) (Y : C),
CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y) =
CategoryTheory.MonoidalCategory.whiskerRight f Y
The theorem `CategoryTheory.MonoidalCategory.tensorHom_id` states that for any Category `C` with a Monoidal structure, and for any two objects `X₁` and `X₂` in `C`, if there's a morphism `f` from `X₁` to `X₂`, then tensoring `f` with the identity morphism on any object `Y` in `C` is the same as whiskering `f` on the right with `Y`. In other words, it expresses the equality between the two operations `tensorHom` and `whiskerRight` in a Monoidal Category when the second component of the tensor product is the identity morphism.
More concisely: For any monoidal category `C` and objects `X₁`, `X₂` in `C` with a morphism `f : X₁ → X₂`, the tensoring of `f` with the identity on any object `Y` is equal to whiskering `f` on the right with `Y`. That is, `tensorHom f idY = whiskerRight f Y`.
|
CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor Y).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).inv
(CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom
The given theorem, `CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor`, states that for any type `C` that forms a category and a monoidal category, for any two objects `X` and `Y` in this category, the left whiskering of the right unitor of `Y` with `X` is equal to the composition of the inverse of the associator of `X`, `Y`, and the identity object in the category, with the homomorphism of the right unitor of the tensor product of `X` and `Y`.
In other words, the theorem asserts an equality of two morphisms in a monoidal category where various structural morphisms such as unitors and associators, and operations such as tensor product and whiskering, are involved.
More concisely: For any monoidal category `C`, given objects `X` and `Y` in `C`, the left whiskering of the right unitor of `Y` with `X` equals the composition of the inverse of the associator of `X`, `Y`, and the identity object, with the homomorphism of the right unitor of `X ⊗ Y`.
|
Mathlib.CategoryTheory.Monoidal.Category._auxLemma.2
theorem Mathlib.CategoryTheory.Monoidal.Category._auxLemma.2 :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C]
{X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂)
(CategoryTheory.MonoidalCategory.tensorHom g₁ g₂) =
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
(CategoryTheory.CategoryStruct.comp f₂ g₂)
This theorem is a property of morphisms in a monoidal category. Specifically, for any given monoidal category `C`, and any objects `X₁, Y₁, Z₁, X₂, Y₂, Z₂` of `C`, it states that the tensor product of the composition of morphisms `f₁` and `f₂` from `X₁` to `Y₁` and `X₂` to `Y₂` respectively, and the composition of morphisms `g₁` and `g₂` from `Y₁` to `Z₁` and `Y₂` to `Z₂` respectively, is equal to the composition of the tensor product of `f₁` and `g₁` and the tensor product of `f₂` and `g₂`.
In more mathematical terms, it states that:
`(f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂) = (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂)`
where `⊗` represents the tensor product and `≫` signifies the composition of morphisms. This expresses a kind of distributivity property for the tensor product over morphism composition.
More concisely: In a monoidal category, the tensor product of the composition of two morphisms is equal to the composition of their tensor products.
|
CategoryTheory.MonoidalCategory.tensor_whiskerLeft
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (X Y : C)
{Z Z' : C} (f : Z ⟶ Z'),
CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y f))
(CategoryTheory.MonoidalCategory.associator X Y Z').inv)
This theorem, `CategoryTheory.MonoidalCategory.tensor_whiskerLeft`, in the field of category theory, states the following: for any category `C` that is also a monoidal category, and for any objects `X`, `Y`, `Z`, and `Z'` of `C`, and a morphism `f` from `Z` to `Z'`, the operation of whiskering on the left by the tensor product of `X` and `Y` and then applying the morphism `f` is equivalent to first applying the associator to `X`, `Y`, and `Z`, then whiskering on the left by `X` and then `Y` and applying `f`, and finally applying the inverse of the associator to `X`, `Y`, and `Z'`. This theorem essentially shows the coherence of the whiskering operation with the tensor product and the associator in a monoidal category.
More concisely: For any monoidal category C and objects X, Y, Z, Z' along with a morphism f from Z to Z', the left whiskering of f with the tensor product X ⊗ Y is equivalent to applying the associator (left identity natural transformation) with X, Y, and Z, whiskering on the left with X and then Y, and finally the inverse associator with X, Y, and Z'.
|
CategoryTheory.MonoidalCategory.whiskerRight_id
theorem CategoryTheory.MonoidalCategory.whiskerRight_id :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X Y : C}
(f : X ⟶ Y),
CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor Y).inv)
The theorem `CategoryTheory.MonoidalCategory.whiskerRight_id` states that for any category `C` that is also a monoidal category, and for any two objects `X` and `Y` in `C`, the whisker right of a morphism `f` from `X` to `Y` with the identity morphism of `C` is equal to the composition of the right unitor of `X` and the composition of `f` and the inverse of the right unitor of `Y`.
In other words, this theorem concerns the interaction of morphisms and unitors in a monoidal category. The "whisker right" operation corresponds to the "precomposition with an identity morphism" operation in the monoidal category, and the "right unitor" is a specific isomorphism associated with each object of the monoidal category, witnessing the identity law for tensoring with a unit object. This theorem asserts a specific equality involving these concepts, which is part of the structure of a monoidal category.
More concisely: In a monoidal category `C`, for all objects `X` and `Y` and morphisms `f : X → Y`, the whisker right of `f` with the identity morphism is equal to the composition of the right unitor of `X` with `f` and the inverse of the right unitor of `Y`.
|
CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight
theorem CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).hom Y =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).hom
(CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom
This theorem, `CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight`, states that for any monoidal category `C` and for any objects `X` and `Y` in `C`, whiskering the left unitor of `X` on the right by `Y` is equal to the composition of the associator of the identity of `C`, `X` and `Y`, with the left unitor of the tensor of `X` and `Y`. Here, whiskering is essentially a way of composing morphisms, the left unitor is a specific morphism that acts like the multiplicative identity in a monoidal category, and the associator is a morphism that expresses the associativity of the tensor product. This theorem is a categorical version of the left identity law.
More concisely: For any monoidal category `C`, the whiskered composition of the left unitor of object `X` with the identity of `Y` and the associator of `X`, `Y`, and their tensor product is equal to the left unitor of the tensor product of `X` and `Y`.
|
CategoryTheory.MonoidalCategory.inv_whiskerLeft
theorem CategoryTheory.MonoidalCategory.inv_whiskerLeft :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
(f : Y ⟶ Z) [inst_1 : CategoryTheory.IsIso f],
CategoryTheory.inv (CategoryTheory.MonoidalCategory.whiskerLeft X f) =
CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.inv f)
This theorem, `CategoryTheory.MonoidalCategory.inv_whiskerLeft`, states that for any type `C` that is a category `𝒞` and a monoidal category, and for any objects `X`, `Y`, and `Z` in `C`, if there is a morphism `f` from `Y` to `Z` which is an isomorphism, then the inverse of the whiskerLeft operation applied to `X` and `f` (noted `CategoryTheory.inv (CategoryTheory.MonoidalCategory.whiskerLeft X f)`) is equal to the whiskerLeft operation applied to `X` and the inverse of `f` (expressed as `CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.inv f)`).
In simpler terms, this theorem captures the idea that "whiskering" on the left with a fixed object commutes with taking inverses of morphisms in a monoidal category.
More concisely: In a monoidal category, whiskering on the left with a fixed object commutes with taking morphism inverses. That is, for any objects `X`, `Y`, and `Z` and an isomorphism `f : Y ⟶ Z`, `CategoryTheory.inv (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.inv f)`.
|
CategoryTheory.MonoidalCategory.associator_conjugation
theorem CategoryTheory.MonoidalCategory.associator_conjugation :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z'),
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h))
(CategoryTheory.MonoidalCategory.associator X' Y' Z').inv)
This theorem states that in any monoidal category `C`, for any objects `X`, `X'`, `Y`, `Y'`, `Z`, and `Z'`, and any morphisms `f : X ⟶ X'`, `g : Y ⟶ Y'`, and `h : Z ⟶ Z'`, the composition of the tensor product of `f`, `g`, and `h` is equal to the composition of the associator of `X`, `Y`, `Z` and the tensor product of `f`, `g`, `h` followed by the inverse of the associator of `X'`, `Y'`, `Z'`.
In other words, it is asserting the coherence condition for the associativity of the tensor product operation in a monoidal category. This condition is essentially saying that the result is the same whether we first resolve the tensor product of `X` and `Y` and then tensor the result with `Z`, or if we first resolve the tensor product of `Y` and `Z` and then tensor `X` with the result.
More concisely: In any monoidal category, the composition of the associator with the tensor product of morphisms is equal to the tensor product of the morphisms followed by the inverse of the associator.
|
CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
(f : Y ≅ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f.inv)
(CategoryTheory.MonoidalCategory.whiskerLeft X f.hom) =
CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Z)
This theorem, named `CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom`, states that for any Category `C` that is also a Monoidal Category, and for any objects `X`, `Y` and `Z` in `C`, if there is an isomorphism `f` from `Y` to `Z`, then the composition of `whiskerLeft` applied to `X` and `f.inv`, followed by `whiskerLeft` applied to `X` and `f.hom`, is equal to the identity on the tensor product of `X` and `Z`.
In more mathematical terms, the theorem is stating that $(f^{-1} * f) \otimes X = I_{X\otimes Z}$ in the context of a monoidal category, where $*$ denotes composition, $\otimes$ is the tensor product, and $I_{X\otimes Z}$ is the identity morphism on the tensor product of `X` and `Z`. This encapsulates one of the fundamental properties of monoidal categories.
More concisely: In a monoidal category, the composition of the inverse and the morphism of any object with an isomorphism is equal to the identity morphism on their tensor product.
|
CategoryTheory.MonoidalCategory.whiskerRight_iff
theorem CategoryTheory.MonoidalCategory.whiskerRight_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
(f g : X ⟶ Y),
CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C) = CategoryTheory.MonoidalCategory.whiskerRight g (𝟙_ C) ↔
f = g
This theorem states that for any category `C` that is also a monoidal category, and for any two morphisms `f` and `g` from object `X` to `Y` in `C`, the equality of the results of "whiskering" `f` and `g` on the right by the identity morphism of `C` implies the equality of `f` and `g` themselves. In other words, if whiskering `f` and `g` on the right with the identity morphism yields the same result, then `f` and `g` must be identical. This theorem provides a condition for testing the equivalence of morphisms in a monoidal category, using the concept of whiskering - a form of "shaping" or "manipulating" morphisms in a category.
More concisely: In a monoidal category `C`, if for any morphisms `f` and `g` from object `X` to `Y`, the equality of `(f ⊠ id_Y) = (g ⊠ id_Y)` implies `f = g`, where `⊠` is the whiskering operation, then `C` satisfies the equality of whiskering and identity morphisms.
|
CategoryTheory.MonoidalCategory.whiskerLeft_iff
theorem CategoryTheory.MonoidalCategory.whiskerLeft_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
(f g : X ⟶ Y),
CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f = CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) g ↔
f = g
This theorem deals with category theory in the context of a monoidal category. It states that, for any type `C` equipped with both a category structure and a monoidal category structure, and for objects `X` and `Y` in `C`, if two morphisms `f` and `g` from `X` to `Y` are such that the whisker left operation with the identity morphism on `C` applied to `f` equals the same operation applied to `g`, then `f` and `g` must be equal. The whisker left operation is a type of operation in category theory that modifies a morphism in a certain way.
More concisely: In a monoidal category, if two morphisms from object X to object Y have equal whisker left compositions with the identity morphism, then they are equal.
|
Mathlib.CategoryTheory.Monoidal.Category._auxLemma.1
theorem Mathlib.CategoryTheory.Monoidal.Category._auxLemma.1 :
∀ {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
The theorem `Mathlib.CategoryTheory.Monoidal.Category._auxLemma.1` states that for any category `C` of Type `u` which is a monoidal category, for any object `X` in `C` and any morphism `f` from object `Y₁` to object `Y₂` in `C`, the operation of whiskering on the left with `X` on `f` is equal to the tensor product of the identity morphism on `X` and `f`. This is a key property in the theory of monoidal categories, connecting the concepts of whiskering and tensor product of morphisms.
More concisely: For any object X in a monoidal category C and any morphism f in C, the whiskering of X with f is equal to the tensor product of the identity morphism on X and f.
|
CategoryTheory.MonoidalCategory.id_tensorHom
theorem CategoryTheory.MonoidalCategory.id_tensorHom :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (X : C) {Y₁ Y₂ : C}
(f : Y₁ ⟶ Y₂),
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f =
CategoryTheory.MonoidalCategory.whiskerLeft X f
This theorem states that for any category `C` that is also a monoidal category, and for any objects `X`, `Y₁`, `Y₂` in `C`, with a morphism `f` from `Y₁` to `Y₂`, applying the tensorHom function to the identity morphism on `X` and `f` is the same as whiskering on the left of `X` with `f`. In other words, using the identity morphism on `X` in a tensor operation is equivalent to a left whiskering operation on `X`. This corresponds to the naturality condition for monoidal categories in category theory.
More concisely: For any monoidal category C and objects X, Y₁, Y₂ with morphism f : Y₁ → Y₂, the tensorHom identity morphism X → Hom(C(X, Y₁), C(X, Y₂)) ≅ left whiskering of X with f.
|
CategoryTheory.MonoidalCategory.tensor_id
theorem CategoryTheory.MonoidalCategory.tensor_id :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C),
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁)
(CategoryTheory.CategoryStruct.id X₂) =
CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)
This theorem states that in any monoidal category, the tensor product of identity morphisms is the identity morphism of the tensor product. Formally, for any objects `X₁` and `X₂` in a category `C` which has a monoidal structure, the tensor product of the identity morphism on `X₁` and the identity morphism on `X₂` is equal to the identity morphism on the tensor product of `X₁` and `X₂`. That is, `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)`.
More concisely: In any monoidal category, the identity morphisms on objects commute with the tensor product, i.e., `𝟙 X ⊗ 𝟙 Y = 𝟙 (X ⊗ Y)` for all objects `X` and `Y`.
|
CategoryTheory.MonoidalCategory.tensorHom_def'
theorem CategoryTheory.MonoidalCategory.tensorHom_def' :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C}
(f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
CategoryTheory.MonoidalCategory.tensorHom f g =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X₁ g)
(CategoryTheory.MonoidalCategory.whiskerRight f Y₂)
This theorem in category theory states that for any category `C` with monoidal structure, and any four objects `X₁`, `Y₁`, `X₂`, `Y₂` in `C`, and morphisms `f : X₁ ⟶ Y₁` and `g : X₂ ⟶ Y₂`, the tensor product of `f` and `g` is equal to the composition of the left whiskering of `g` with `X₁` and the right whiskering of `f` with `Y₂`. Here, whiskering refers to a certain operation involving a morphism and an object in a category, and the tensor product of morphisms is a way of combining two morphisms into one.
More concisely: For any category with monoidal structure, the tensor product of morphisms `f : X₁ ⟶ Y₁` and `g : X₂ ⟶ Y₂` is equal to the composition of the left whiskering of `g` with `X₁` and the right whiskering of `f` with `Y₂`.
|
CategoryTheory.MonoidalCategory.inv_hom_whiskerRight
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X Y : C}
(f : X ≅ Y) (Z : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f.inv Z)
(CategoryTheory.MonoidalCategory.whiskerRight f.hom Z) =
CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z)
This theorem is named `CategoryTheory.MonoidalCategory.inv_hom_whiskerRight` in Lean 4 and belongs to the area of Category Theory, specifically Monoidal Categories. It states that for any Category `C` (with the Monoidal structure), and for any objects `X`, `Y`, and `Z` in `C`, given a natural isomorphism `f` between `X` and `Y`, the composition of `f.inv` whiskerRight `Z` and `f.hom` whiskerRight `Z` (i.e., first applying `f.inv` then `f.hom` along the right side of `Z` in the tensor product) equals the identity morphism on the tensor product of `Y` and `Z`. Essentially, this theorem encapsulates the idea that whiskering (tensoring with an object) respects the inverse property of isomorphisms in a monoidal category.
More concisely: For any monoidal category C, given an object X and natural isomorphisms f : X ≅ Y, the composition of f.inv ⊛ Z and f.hom ⊛ Z (whiskered right along Z) equals the identity morphism on X ⊗ Y, where ⊛ denotes composition in the 2-category of C and ⊗ denotes the monoidal product.
|
CategoryTheory.MonoidalCategory.whisker_exchange
theorem CategoryTheory.MonoidalCategory.whisker_exchange :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
(f : W ⟶ X) (g : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W g)
(CategoryTheory.MonoidalCategory.whiskerRight f Z) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Y)
(CategoryTheory.MonoidalCategory.whiskerLeft X g)
The theorem `CategoryTheory.MonoidalCategory.whisker_exchange` states that, given a category `C` which is also a monoidal category, and morphisms `f` from `W` to `X` and `g` from `Y` to `Z` (where `W`, `X`, `Y`, `Z` are objects in the category `C`), the composition of whisker-left operation applied to `W` and `g`, followed by the whisker-right operation applied to `f` and `Z`, is equal to the composition of the whisker-right operation applied to `f` and `Y`, followed by the whisker-left operation applied to `X` and `g`.
In other words, in a monoidal category, you can exchange the order of the whiskering operations, as long as you adjust the objects appropriately. This is an important property in category theory, particularly in the context of monoidal categories.
More concisely: In a monoidal category, the composition of whisker-left on object W with morphism g, followed by whisker-right on f and Z, equals the composition of whisker-right on f and object Y with whisker-left on X and morphism g.
|
CategoryTheory.MonoidalCategory.rightUnitor_naturality
theorem CategoryTheory.MonoidalCategory.rightUnitor_naturality :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X Y : C}
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C))
(CategoryTheory.MonoidalCategory.rightUnitor Y).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f
This theorem is known as the "Naturality of the right unitor" in category theory, particularly in the context of monoidal categories. It asserts that for any category `C` which has a monoidal structure, any two objects `X` and `Y` within `C`, and any morphism `f` from `X` to `Y`, the following two paths are equivalent:
First, taking `f` whiskerRight with the identity on `C`, and then applying the right unitor on `Y`.
Second, applying the right unitor on `X` and then `f`.
In other words, the diagram commutes for the right unitor, showing that the process of applying the right unitor is natural with respect to the morphism `f`.
More concisely: In any monoidal category, for all objects X, Y, and morphism f, the diagram commutes for the right unitor, i.e., (id\_Y ∘ f) ⊓ r ~r (X) = f ∘ r ~r (X), where id\_Y is the identity morphism on Y, "∘" denotes composition, "⊓" denotes the monoidal product or tensor, and r ~r (X) represents the right unitor on X.
|
CategoryTheory.MonoidalCategory.whiskerRight_tensor
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X X' : C}
(f : X ⟶ X') (Y Z : C),
CategoryTheory.MonoidalCategory.whiskerRight f (CategoryTheory.MonoidalCategory.tensorObj Y Z) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f Y) Z)
(CategoryTheory.MonoidalCategory.associator X' Y Z).hom)
The theorem `CategoryTheory.MonoidalCategory.whiskerRight_tensor` states that for any category `C` with monoidal structure and objects `X`, `X'`, `Y`, `Z` of `C` and a morphism `f` from `X` to `X'`, the whiskering on the right of `f` with the tensor product of `Y` and `Z` is equivalent to the composition of the inverse of the associator of `X`, `Y`, `Z` and the composition of the whiskering on the right of `f` whiskered on the right with `Y` on `Z` and the homomorphism given by the associator of `X'`, `Y`, `Z`.
In terms of category theory, this theorem is about the interaction of the whiskering-right operation with the tensor product operation in a monoidal category. The theorem demonstrates how these two operations are related through the associator, which is part of the structure of a monoidal category and provides the coherence conditions for the tensor product.
More concisely: For any monoidal category `C` and objects `X`, `X'`, `Y`, `Z` in `C`, and morphism `f : X → X'`, the right whiskering of `f` with the tensor product of `Y` and `Z` is equivalent to the composition of the inverse of the associator of `X`, `Y`, `Z`, `f`, the associator of `X'`, `Y`, `Z`, and the right whiskering of `f` with `Y` on `Z`.
|
CategoryTheory.MonoidalCategory.whisker_assoc
theorem CategoryTheory.MonoidalCategory.whisker_assoc :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
(f : Y ⟶ Y') (Z : C),
CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X f) Z =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerRight f Z))
(CategoryTheory.MonoidalCategory.associator X Y' Z).inv)
The theorem `CategoryTheory.MonoidalCategory.whisker_assoc` states that for any category `C` that also has a monoidal structure, and any objects `X`, `Y`, `Y'`, `Z` in `C`, and a morphism `f` from `Y` to `Y'`, the process of first whiskering `f` on the left by `X` and then on the right by `Z` (expressed as `CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X f) Z`) is equivalent to another process. The other process involves taking the composition of the homeomorphism part of the associator for `X`, `Y`, `Z` and then the composition of the left whiskering of `X` by the right whiskering of `f` by `Z`, and the inverse of the associator for `X`, `Y'`, `Z`. Here, the associator provides a specific isomorphism that enforces the associativity property in the monoidal category, and whiskering refers to the act of pre- or post-composing a given morphism with a fixed morphism.
More concisely: For any monoidal category `C` and objects `X`, `Y`, `Y'`, `Z` in `C`, and a morphism `f` from `Y` to `Y'`, the diagram commuting between `CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerRight f Z)` and `(CategoryTheory.MonoidalCategory.associator X Y Z) o (CategoryTheory.MonoidalCategory.left_whisker X (CategoryTheory.MonoidalCategory.right_whisker f Z)) o (CategoryTheory.MonoidalCategory.associator X Y' Z).inv` holds.
|
CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor Y).inv =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv
(CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).hom
This theorem, which is given for any monoidal category, states that for any two objects, X and Y, in the category, the left whisker of the inverse of the right unitor of Y with respect to X is equal to the composition of the inverse of the right unitor of the tensor product of X and Y and the homomorphism of the associator of X, Y, and the identity object.
In more detail, in the context of category theory, a "whiskering" operation is a way to apply a functor to a natural transformation. Here, the "left whisker" operation applies a functor (coming from object X) to a natural transformation (the inverse of the right unitor for Y). This is proven to be equal to a certain composition of morphisms, specifically the composition of the inverse of the right unitor of the tensor product of X and Y, with the homomorphism (morphism) of an associator with X, Y and the monoidal unit (𝟙_ C) as arguments. The right unitor and associator are specific structures associated with a monoidal category, which is a category equipped with a tensor product operation and certain axiomatic transformations.
More concisely: For any monoidal category, the left whisker of the inverse of the right unitor of object Y with respect to X equals the composition of the inverse of the right unitor of X ⊗ Y, the homomorphism of the associator of X, Y, and 𝟙\_C.
|
CategoryTheory.MonoidalCategory.comp_whiskerRight
theorem CategoryTheory.MonoidalCategory.comp_whiskerRight :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {W X Y : C}
(f : W ⟶ X) (g : X ⟶ Y) (Z : C),
CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Z =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z)
(CategoryTheory.MonoidalCategory.whiskerRight g Z)
This theorem, named `CategoryTheory.MonoidalCategory.comp_whiskerRight`, states that in any monoidal category `C`, for any three objects `W`, `X`, `Y` in `C`, and any two morphisms `f` from `W` to `X` and `g` from `X` to `Y`, the whiskering of the composition of `f` and `g` on the right by any object `Z` in `C` (denoted `CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Z`) is equal to the composition of the whiskering of `f` and `g` on the right by `Z` (denoted `CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (CategoryTheory.MonoidalCategory.whiskerRight g Z)`). Here, "whiskering" refers to a specific binary operation on morphisms in a monoidal category, and "composition" refers to the standard composition of morphisms in a category.
More concisely: In any monoidal category, for all objects W, X, Y, and morphisms f : W -> X and g : X -> Y, the whiskering of the composition f * g on the right by any object Z is equal to the composition of the whiskered morphisms f \*_Z and g \*_Z.
|
CategoryTheory.MonoidalCategory.leftUnitor_naturality
theorem CategoryTheory.MonoidalCategory.leftUnitor_naturality :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X Y : C}
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f)
(CategoryTheory.MonoidalCategory.leftUnitor Y).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f
This theorem is about the naturality of the left unitor in a monoidal category. In essence, it states that for any objects `X`, `Y` in a monoidal category `C`, and any morphism `f` from `X` to `Y`, the composition of the whiskerLeft operation on `f` with the identity object of `C` and the hom morphism of the left unitor of `Y` is equal to the composition of the hom morphism of the left unitor of `X` and `f`. This can be seen as a kind of commutative property involving the left unitor and the morphism `f`.
More concisely: For any object `X` and `Y` in a monoidal category `C`, and any morphism `f : X → Y`, the diagram commutes:
```
leftUnitX _ ∘ f
| = |
| / \
| / \
| / \
leftUnitY _ ∘ _
```
Where `leftUnitX` and `leftUnitY` denote the left unitor morphisms at objects `X` and `Y`, respectively.
|
Mathlib.CategoryTheory.Monoidal.Category._auxLemma.3
theorem Mathlib.CategoryTheory.Monoidal.Category._auxLemma.3 :
∀ {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)
The theorem, `Mathlib.CategoryTheory.Monoidal.Category._auxLemma.3`, states that for any category `C` of type `u` equipped with the structure of a monoidal category, for any two objects `X₁` and `X₂` in `C` and any morphism `f` from `X₁` to `X₂`, and for any object `Y` in `C`, the operation of whiskering on the right by `f` on `Y` is equal to the tensor product of `f` and the identity morphism on `Y`. In other words, for all `f` and `Y`, we have: `CategoryTheory.MonoidalCategory.whiskerRight f Y = CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)`. In simpler terms, this theorem is asserting a specific property about how morphisms interact with the tensor product and identity morphism in a monoidal category.
More concisely: In a monoidal category, whiskering a morphism on the right by another morphism is equivalent to the tensor product of the two morphisms.
|
CategoryTheory.MonoidalCategory.associator_naturality
theorem CategoryTheory.MonoidalCategory.associator_naturality :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) f₃)
(CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom
(CategoryTheory.MonoidalCategory.tensorHom f₁ (CategoryTheory.MonoidalCategory.tensorHom f₂ f₃))
This theorem, known as the naturality of the associator isomorphism in a monoidal category, states that for any category `C` with a monoidal structure, and any six objects `X₁`, `X₂`, `X₃`, `Y₁`, `Y₂`, `Y₃` in `C`, if there are morphisms `f₁` from `X₁` to `Y₁`, `f₂` from `X₂` to `Y₂`, and `f₃` from `X₃` to `Y₃`, then the composition of the tensor product of the morphisms `f₁ ⊗ f₂` and `f₃` with the associator of `Y₁`, `Y₂`, and `Y₃` is equal to the composition of the associator of `X₁`, `X₂`, and `X₃` with the tensor product of the morphisms `f₁` and `f₂ ⊗ f₃`.
In simpler terms, this theorem is expressing that tensoring with a morphism and then reassociating the result is the same as first reassociating and then tensoring with the morphism, preserving the associativity property in the context of category theory.
More concisely: For any monoidal category `C` and morphisms `f₁ : X₁ → Y₁`, `f₂ : X₂ → Y₂`, `f₃ : X₃ → Y₃`, the diagram commuting with the associator isomorphisms commutes, i.e., (f₁ ⊗ f₂) ⊗ f₃ ≈ f₁ ⊗ (f₂ ⊗ f₃).
|