CategoryTheory.Bicategory.Strict.id_comp
theorem CategoryTheory.Bicategory.Strict.id_comp :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [self : CategoryTheory.Bicategory.Strict B] {a b : B}
(f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f
The theorem `CategoryTheory.Bicategory.Strict.id_comp` states that for any bicategory `B` that is strict, and for any objects `a` and `b` in `B`, the composition of the identity morphism on `a` and any morphism from `a` to `b` is just the original morphism. This essentially means that the identity morphism acts as a left identity for the operation of composition in the bicategory `B`. In terms of category theory, this can be expressed as `Id_a ∘ f = f` for any morphism `f` from `a` to `b`.
More concisely: In a strict bicategory, the identity morphism's composition with any morphism equals the morphism itself.
|
CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso
theorem CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [self : CategoryTheory.Bicategory.Strict B] {a b : B}
(f : a ⟶ b), CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯
This theorem states that, for any bicategory `B` that is also strict, and any objects `a` and `b` in `B`, the left unitor of an arrow `f` from `a` to `b` is given by an isomorphism constructed from an equality. In more detail, the left unitor, which is a canonical isomorphism in a bicategory that involves the identity arrow of `a` and `f`, is equivalent to an isomorphism generated from an equality between certain objects in the bicategory. This equality to isomorphism conversion avoids issues related to dependent type theory.
More concisely: For any strict bicategory B and objects a, b, the left unitor isomorphism of an arrow f from a to b is equivalent to an isomorphism derived from an equality between appropriate objects in B.
|
CategoryTheory.Bicategory.Strict.comp_id
theorem CategoryTheory.Bicategory.Strict.comp_id :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [self : CategoryTheory.Bicategory.Strict B] {a b : B}
(f : a ⟶ b), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f
This theorem from Category Theory states that for every object `a` and `b` in any strict bicategory `B`, the composition of any morphism `f` from `a` to `b` with the identity morphism on `b` is `f` itself. In other words, the identity morphism acts as the right identity for the composition operation in a strict bicategory. This result is similar to the mathematical concept where multiplying any number by 1 (the identity element for multiplication) gives the number itself.
More concisely: In a strict bicategory, for all objects `a` and `b`, and morphism `f` from `a` to `b`, the composition `f` ∘ id\_b = f`, where `id_b` is the identity morphism on `b`.
|
CategoryTheory.Bicategory.Strict.associator_eqToIso
theorem CategoryTheory.Bicategory.Strict.associator_eqToIso :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [self : CategoryTheory.Bicategory.Strict B] {a b c d : B}
(f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯
This theorem, `CategoryTheory.Bicategory.Strict.associator_eqToIso`, states that for any strict bicategory `B` and objects `a`, `b`, `c`, `d` in `B`, the associator of three morphisms `f: a ⟶ b`, `g: b ⟶ c`, and `h: c ⟶ d` is equivalent, in the sense of isomorphism, to the isomorphism arising from an equality. The associator is a structural component of a bicategory that expresses how the composition of morphisms behaves with respect to parenthesization. The theorem essentially claims that in a strict bicategory, the associativity of morphisms is strict, not just up to isomorphism, but in fact up to literal equality.
More concisely: In a strict bicategory, the associator of three composable morphisms is equal, not just isomorphic, to the identity morphism obtained by composing the morphisms in a different order.
|
CategoryTheory.Bicategory.Strict.assoc
theorem CategoryTheory.Bicategory.Strict.assoc :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [self : CategoryTheory.Bicategory.Strict B] {a b c d : B}
(f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
The theorem `CategoryTheory.Bicategory.Strict.assoc` states that in any strict bicategory `B`, the composition of morphisms is associative. Given any four objects `a`, `b`, `c`, and `d` in the bicategory `B` and any three morphisms `f : a ⟶ b`, `g : b ⟶ c`, and `h : c ⟶ d`, the composition of `f` and `g` followed by `h` is the same as the composition of `f` with the result of the composition of `g` and `h`.
More concisely: In a strict bicategory, the order of composition of morphisms is irrelevant: `(f ∘ g) ∘ h = f ∘ (g ∘ h)` for all objects `a, b, c, d` and morphisms `f : a ⟶ b`, `g : b ⟶ c`, and `h : c ⟶ d`.
|
CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso
theorem CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso :
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [self : CategoryTheory.Bicategory.Strict B] {a b : B}
(f : a ⟶ b), CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯
This theorem states that in a strict bicategory, the right unitor of a morphism equals the isomorphism given by an equality. Specifically, for any objects `a` and `b` in this bicategory, and any morphism `f` from `a` to `b`, the right unitor of `f` (which characterizes the identity-on-right property of `f`) is equivalent to the isomorphism derived from an equality between certain objects in the category, as specified by the `CategoryTheory.eqToIso` function.
More concisely: In a strict bicategory, for any object `a`, object `b`, and morphism `f` from `a` to `b`, the right unitor of `f` is equivalent to the isomorphism derived from the equality of the objects `f.target` and `b`.
|