CategoryTheory.comp_leftAdjointMate
theorem CategoryTheory.comp_leftAdjointMate :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
[inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y]
[inst_4 : CategoryTheory.HasLeftDual Z] {f : X ⟶ Y} {g : Y ⟶ Z},
(ᘁCategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (ᘁg) (ᘁf)
This theorem, in the Category Theory, states that for any type `C` which is a category and also a monoidal category, with objects `X`, `Y`, and `Z` where each object has a left dual, the composition of left adjoint mates of morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, is equivalent to the composition of the left adjoint of `g` and the left adjoint of `f`. Here, `ᘁCategoryTheory.CategoryStruct.comp f g` denotes the left adjoint mate of the composition of `f` and `g`, and `CategoryTheory.CategoryStruct.comp (ᘁg) (ᘁf)` denotes the composition of the left adjoints of `g` and `f`. Therefore, we can say that the process of taking left adjoint mates commutes with composition in the category.
More concisely: For any category `C` with objects `X`, `Y`, `Z` having left duals, the left adjoint mates of morphisms `f: X ↔ Y` and `g: Y ↔ Z` commute, i.e., `ᘁCategoryTheory.CategoryStruct.comp f g ≈ ᘁCategoryTheory.CategoryStruct.comp (ᘁg) (ᘁf)`.
|
CategoryTheory.leftAdjointMate_id
theorem CategoryTheory.leftAdjointMate_id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
[inst_2 : CategoryTheory.HasLeftDual X],
(ᘁCategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ᘁX
This theorem, `CategoryTheory.leftAdjointMate_id`, states that for any type `C` that has instances of a `CategoryTheory.Category` and a `CategoryTheory.MonoidalCategory`, and for any object `X` of type `C` that has a left dual, the antipode or antidual (denoted by `ᘁ`) of the identity morphism on `X` is equal to the identity morphism on the antidual of `X`. In the language of category theory, this is expressing a property of dual objects in a monoidal category, where the dual of a morphism is related to the morphism on the dual object.
More concisely: In a monoidal category with objects having left duals, the antipode of the identity morphism on an object is equal to the identity morphism on the object's left dual.
|
CategoryTheory.tensorLeftHomEquiv_tensor
theorem CategoryTheory.tensorLeftHomEquiv_tensor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X X' Y Y' Z Z' : C} [inst_2 : CategoryTheory.ExactPairing Y Y']
(f : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y Z) (g : X' ⟶ Z'),
(CategoryTheory.tensorLeftHomEquiv (CategoryTheory.MonoidalCategory.tensorObj X X') Y Y'
(CategoryTheory.MonoidalCategory.tensorObj Z Z')).symm
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g)
(CategoryTheory.MonoidalCategory.associator Y Z Z').hom) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y' X X').inv
(CategoryTheory.MonoidalCategory.tensorHom ((CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm f) g)
This theorem, `CategoryTheory.tensorLeftHomEquiv_tensor`, states that within a monoidal category `C`, where `Y` and `Y'` form an exact pairing, the operation `tensorLeftHomEquiv`, which is a homomorphism from the tensor product of `X` and `X'` to the tensor product of `Y` and `Y'`, commutes with the tensor product operation on the right.
More explicitly, given any morphisms `f` from `X` to the tensor product of `Y` and `Z`, and `g` from `X'` to `Z'`, the composition of `tensorHom f g` followed by the associator `Y Z Z'` under `tensorLeftHomEquiv` is equal to the composition of the inverse of the associator `Y' X X'` followed by the tensor product of `tensorLeftHomEquiv.symm f` and `g`. The associator is a natural isomorphism expressing one of the axioms of a monoidal category, specifically the coherence condition for the tensor product.
More concisely: In a monoidal category with exact pairing `Y` and `Y'`, the homomorphism `tensorLeftHomEquiv` from the tensor product of `X` and `X'` to the tensor product of `Y` and `Y'` commutes with the tensor product operation on the right, i.e., `(tensorHom f g) . associatorYZZ' = inverseAssociatorY'XX'. tensorProduct (tensorLeftHomEquiv.symm f) g`, where `f` is a morphism from `X` to `Y ⊗ Z`, `g` is a morphism from `X'` to `Z'`, and `associatorYZZ'` and `inverseAssociatorY'XX'` are associators.
|
CategoryTheory.rightAdjointMate_id
theorem CategoryTheory.rightAdjointMate_id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
[inst_2 : CategoryTheory.HasRightDual X],
CategoryTheory.CategoryStruct.id Xᘁ = CategoryTheory.CategoryStruct.id Xᘁ
This theorem, `CategoryTheory.rightAdjointMate_id`, states that for any type `C` that is a category and a monoidal category, and any object `X` in `C` that has a right dual, the identity morphism on the right dual of `X` (denoted `Xᘁ`) is equal to itself. In other words, the identity morphism on the right dual of an object is idempotent in the category theory context.
More concisely: In any monoidal category `C` with objects `C` and `X` having right duals `Xᘁ`, the identity morphism on the right dual of `X`, `id Xᘁ`, is equal to itself.
|
CategoryTheory.tensorRightHomEquiv_tensor
theorem CategoryTheory.tensorRightHomEquiv_tensor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X X' Y Y' Z Z' : C} [inst_2 : CategoryTheory.ExactPairing Y Y']
(f : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Z Y') (g : X' ⟶ Z'),
(CategoryTheory.tensorRightHomEquiv (CategoryTheory.MonoidalCategory.tensorObj X' X) Y Y'
(CategoryTheory.MonoidalCategory.tensorObj Z' Z)).symm
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f)
(CategoryTheory.MonoidalCategory.associator Z' Z Y').inv) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X' X Y).hom
(CategoryTheory.MonoidalCategory.tensorHom g ((CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm f))
The theorem `CategoryTheory.tensorRightHomEquiv_tensor` states that for any category `C` which is also a monoidal category, and for any objects `X`, `X'`, `Y`, `Y'`, `Z`, `Z'` in `C` with an exact pairing on `Y` and `Y'`, and any morphisms `f` from `X` to the tensor object of `Z` and `Y'` and `g` from `X'` to `Z'`, the inverse of `tensorRightHomEquiv` applied to the tensor object of `X'` and `X`, `Y`, `Y'`, `Z'` and `Z`, and the composition of `tensorHom` of `g` and `f` with the inverse of the associator of `Z'`, `Z` and `Y'` is equal to the composition of the hom of the associator of `X'`, `X` and `Y` with the tensor of `g` and the inverse of `tensorRightHomEquiv` applied to `X`, `Y`, `Y'`, `Z` and `f`. This essentially proves that the `tensorRightHomEquiv` operation commutes with tensoring on the left.
More concisely: For any monoidal category `C` with exact pairings and objects `X`, `X'`, `Y`, `Y'`, `Z`, `Z'`, morphisms `f` from `X` to `Z ⊗ Y'` and `g` from `X'` to `Z'`, the following diagram commutes:
```
tensorHom(g) ∘ tensorRightHomEquiv(X, Y, Y', Z, Z) ∘ f ≈ tensor(g) ∘ inverseAssociator(X', X, Y) ∘ tensorRightHomEquiv(X, Y, Y', Z, f)
```
|
CategoryTheory.comp_rightAdjointMate
theorem CategoryTheory.comp_rightAdjointMate :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
[inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y]
[inst_4 : CategoryTheory.HasRightDual Z] {f : X ⟶ Y} {g : Y ⟶ Z},
CategoryTheory.CategoryStruct.comp f gᘁ = CategoryTheory.CategoryStruct.comp (gᘁ) (fᘁ)
This theorem is set within the context of category theory and monoidal categories. It states that for any objects X, Y, and Z in a monoidal category C, if X, Y, and Z each have a right dual, then the composition of the right adjoint mates of the morphisms f : X ⟶ Y and g : Y ⟶ Z is equal to the right adjoint mate of the composition of f and g. Here, the right adjoint mate of a morphism is denoted by the superscript dagger (ᘁ). This property is fundamental to the concept of adjoint functors in category theory.
More concisely: In a monoidal category, if objects X, Y, and Z have right duals, then (f^! ∘ g^!) = (f ∘ g)^!, where f : X ⟶ Y, g : Y ⟶ Z, and the superscript "!" denotes the right adjoint mate.
|