CategoryTheory.Bicategory.whiskerLeft_rightUnitor
theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv
(CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
This theorem, `CategoryTheory.Bicategory.whiskerLeft_rightUnitor`, states that for any bicategory `B` with objects `a`, `b`, and `c`, and morphisms `f : a ⟶ b` and `g : b ⟶ c`, the homomorphism associated with the left whiskering of `f` with the right unitor of `g` is equal to the composition of the inverse of the associator of `f`, `g`, and the identity on `c` with the homomorphism of the right unitor of the composition of `f` and `g`. This equality follows from the coherence conditions in the definition of bicategories, and the whiskering and unitors are specific isomorphisms that exist in any bicategory.
More concisely: For any bicategory B and morphisms f : a ⟶ b, g : b ⟶ c, the homomorphism of the left whiskering of f with the right unitor of g equals the composition of the inverse of the associator of f, g, and the identity on c, with the homomorphism of the right unitor of the composition of f and g.
|
CategoryTheory.Bicategory.leftUnitor_whiskerRight
theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom
(CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
This theorem, `CategoryTheory.Bicategory.leftUnitor_whiskerRight`, states that in any bicategory `B`, for any objects `a`, `b`, and `c` and for any morphisms `f : a ⟶ b` and `g : b ⟶ c`, the morphism obtained by whiskering on the right by `g` of the homomorphism component of the left unitor of `f`, is equivalent to the composition of the homomorphism component of the associator of the identity morphism on `a`, `f`, and `g`, and the homomorphism component of the left unitor of the composite morphism `f ≫ g`. In mathematical terms, it says that the following equality holds: `(𝟙 f) ▷ g = (id_a * f * g) ⋅ (𝟙 (f ≫ g))`, where `*` denotes morphism composition, `⋅` denotes the composition of natural transformations, and `𝟙` denotes the identity morphism.
More concisely: In any bicategory, the right whiskering of the left unitor morphism of a composition of morphisms is equivalent to the composition of the associator of the identity morphism with the left unitor morphisms of the involved morphisms.
|
CategoryTheory.Bicategory.inv_hom_whiskerRight
theorem CategoryTheory.Bicategory.inv_hom_whiskerRight :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h)
(CategoryTheory.Bicategory.whiskerRight η.hom h) =
CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp g h)
This theorem is in the field of category theory and it expresses a property of bicategories. Specifically, it states that for any bicategory `B` and any three objects `a`, `b`, and `c` in `B`, and any two morphisms `f` and `g` from `a` to `b` that are inverses of each other (denoted `η : f ≅ g`), and any morphism `h` from `b` to `c`, the composition of "whiskering" `η.inv` and `η.hom` on the right with `h` (i.e., `CategoryTheory.Bicategory.whiskerRight η.inv h` and `CategoryTheory.Bicategory.whiskerRight η.hom h`) is the identity on the composition of `g` and `h` (i.e., `CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp g h)`).
"Whiskering" in this context is a specific type of operation in category theory that involves the composition of morphisms. And the identity on a composition signifies that the composition operation doesn't change the involved morphisms. Therefore, this theorem essentially says that in a bicategory, if you whisker the inverse of a morphism and the morphism itself on the right with another morphism, you get back the original pair of morphisms.
More concisely: For any bicategory `B`, given objects `a`, `b`, `c`, morphisms `f : a -> b`, `g : a -> b` with `f ≅ g`, and morphism `h : b -> c`, we have `CategoryTheory.CategoryStruct.id (CategoryTheory.Bicategory.whiskerRight η.inv h) * CategoryTheory.Bicategory.whiskerRight η.hom h = (g * h)`.
|
CategoryTheory.Bicategory.whiskerLeft_inv_hom
theorem CategoryTheory.Bicategory.whiskerLeft_inv_hom :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv)
(CategoryTheory.Bicategory.whiskerLeft f η.hom) =
CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)
This theorem states that for any bicategory `B` and any objects `a`, `b`, and `c` in `B`, for any morphism `f` from `a` to `b` and any isomorphism `η` from morphism `g` to `h` (both `g` and `h` are morphisms from `b` to `c`), the composition of `whiskerLeft f η.inv` with `whiskerLeft f η.hom` is equivalent to the identity morphism on the composite `f h`, where `whiskerLeft f η.inv` represents the whiskering on the left of `f` with the inverse of `η` and `whiskerLeft f η.hom` represents the whiskering on the left of `f` with `η`.
The symbol `≅` denotes an isomorphism in category theory, thus `η : g ≅ h` means `η` is an isomorphism from `g` to `h`. The whiskering of a morphism with another one, denoted `whiskerLeft f η.inv` or `whiskerLeft f η.hom`, is a concept in bicategory that generally represents a kind of transformation induced by `f`.
In simpler terms, this theorem is about a property of the whiskering operation in a bicategory, which ensures that whiskering a morphism with the inverse of an isomorphism and then whiskering the result with the original isomorphism gives you the identity morphism, keeping the morphism unchanged. This is analogous to the property of multiplication by the inverse in group theory.
More concisely: For any bicategory `B`, objects `a`, `b`, `c`, morphisms `f : a → b`, `g, h : b → c`, and isomorphism `η : g ≅ h`, the composition of `whiskerLeft f η.inv` with `whiskerLeft f η.hom` is equal to the identity morphism `id_(f h)`.
|