CategoryTheory.Bicategory.Equivalence.left_triangle
theorem CategoryTheory.Bicategory.Equivalence.left_triangle :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (self : CategoryTheory.Bicategory.Equivalence a b),
CategoryTheory.Bicategory.leftZigzagIso self.unit self.counit =
(CategoryTheory.Bicategory.leftUnitor self.hom).trans (CategoryTheory.Bicategory.rightUnitor self.hom).symm
The theorem `CategoryTheory.Bicategory.Equivalence.left_triangle` states that for any bicategory `B` and for any two objects `a` and `b` within this bicategory, the equivalence between `a` and `b` satisfies the following property: the composition of the unit and the counit of this equivalence is equal to the identity morphism, up to left and right unitor transformations. In other words, composing the unit (with the counit) and then applying the left unitor, followed by the inverse of the right unitor, is isotopic to the identity. This condition is often referred to as the "left triangle identity" in the theory of bicategories.
More concisely: For any bicategory B and objects a and b, the unit-counit pair of an equivalence between a and b satisfies the left triangle identity, that is, (unit $\circ$ counit) $\simeq$ id up to coherent isomorphisms.
|
CategoryTheory.Bicategory.Adjunction.right_triangle
theorem CategoryTheory.Bicategory.Adjunction.right_triangle :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
(self : CategoryTheory.Bicategory.Adjunction f g),
CategoryTheory.Bicategory.rightZigzag self.unit self.counit =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
(CategoryTheory.Bicategory.leftUnitor g).inv
This theorem, `CategoryTheory.Bicategory.Adjunction.right_triangle`, states that for any bicategory `B` and objects `a, b` in `B`, and any morphisms `f` from `a` to `b` and `g` from `b` to `a`, given an adjunction between `f` and `g`, the right zigzag composition of the unit and the counit of the adjunction is equal to the composition of the homomorphism of the right unitor of `g` and the inverse of the left unitor of `g`. This is a statement about the interplay of unitors and counits in an adjunction in bicategories, thus forming a kind of 'triangle' identity.
More concisely: For any bicategory `B` and objects `a, b` with adjunction `(f, g, η, ε)` between them, the composition of `ε` and `η` is equal to the right zigzag of `η` with the homomorphism of right unitor of `g` and the inverse of the left unitor of `g`. In symbols: `ε ∘ η = η' ∘ (hom (right_unit g) ∘ η'') ∘ inv (hom (left_unit g))`.
|
CategoryTheory.Bicategory.Adjunction.left_triangle
theorem CategoryTheory.Bicategory.Adjunction.left_triangle :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
(self : CategoryTheory.Bicategory.Adjunction f g),
CategoryTheory.Bicategory.leftZigzag self.unit self.counit =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
(CategoryTheory.Bicategory.rightUnitor f).inv
The theorem `CategoryTheory.Bicategory.Adjunction.left_triangle` states that in any bicategory B, for any objects a and b, and morphisms f from a to b and g from b to a, if there is an adjunction between f and g, then the left zigzag (another particular morphism defined in the context of bicategories) of the unit and the counit of this adjunction is equal (up to natural isomorphisms) to the composition of the homomorphism part of the left unitor of f and the inverse of the homomorphism part of the right unitor of f. The left and right unitors are specific isomorphisms associated with a morphism in a bicategory that involve the identity morphism on the object.
More concisely: In a bicategory B, for any adjunction between morphisms f and g with units η and ε, the left zigzag of η and ε is equal to the composition of the homomorphism part of f's left unitor and the inverse of the homomorphism part of f's right unitor.
|