CategoryTheory.Center.comp_f
theorem CategoryTheory.Center.comp_f :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X Y Z : CategoryTheory.Center C} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
This theorem, `CategoryTheory.Center.comp_f`, states that for any category `C` with structure of a monoidal category, and any three objects `X`, `Y`, and `Z` in the Drinfeld center of `C`, if we have a morphism `f` from `X` to `Y` and a morphism `g` from `Y` to `Z`, then the function component of the composition of `f` and `g` is equal to the composition of the function components of `f` and `g`. In other words, the theorem states an equality between the function part of the composed morphisms and the composition of the function parts of the morphisms, in the context of the Drinfeld center of a monoidal category.
More concisely: In the Drinfeld center of a monoidal category, the function component of the composition of two morphisms is equal to the composition of their function components.
|
CategoryTheory.Center.ext
theorem CategoryTheory.Center.ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X Y : CategoryTheory.Center C} (f g : X ⟶ Y), f.f = g.f → f = g
The theorem `CategoryTheory.Center.ext` states that for any type `C` that is a category and a monoidal category, and for any two objects `X` and `Y` in the Drinfeld center of `C`, if two morphisms `f` and `g` from `X` to `Y` have the same underlying function, then `f` and `g` are equal. In other words, in the context of the Drinfeld center of a monoidal category, morphisms between objects are uniquely determined by their underlying function.
More concisely: In the Drinfeld center of a monoidal category, morphisms between objects are equal if and only if they have the same underlying function.
|