Bimod.TensorBimod.X.proof_1
theorem Bimod.TensorBimod.X.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : Mon_ C} (P : Bimod R S) (Q : Bimod S T),
CategoryTheory.Limits.HasColimit
(CategoryTheory.Limits.parallelPair (CategoryTheory.MonoidalCategory.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator P.X S.X Q.X).hom
(CategoryTheory.MonoidalCategory.whiskerLeft P.X Q.actLeft)))
This theorem, named `Bimod.TensorBimod.X.proof_1`, states that for a given category `C` that is equipped with a monoidal structure and has coequalizers, and given monoidal objects `R`, `S`, and `T` in `C`, along with bimodules `P` from `R` to `S` and `Q` from `S` to `T`, there is a colimit for the parallel pair of morphisms. The first morphism is derived by applying the right whiskering of `P`'s action with `Q`'s object, and the second morphism is obtained by composing the associator of `P`, `S`, and `Q` with the left whiskering of `P`'s object with `Q`'s action.
More concisely: Given a monoidal category `C` with coequalizers, there exists a colimit for the parallel pair of morphisms obtained by right whiskering and left whiskering of a bimodule's action between monoidal objects in `C`.
|
Bimod.Hom.ext
theorem Bimod.Hom.ext :
∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
{A B : Mon_ C} {M N : Bimod A B} (x y : M.Hom N), x.hom = y.hom → x = y
This theorem states that for any given category `C` (with `C` being a Monoidal Category), and any given monoidal objects `A` and `B` in `C`, and any two given Bimodules `M` and `N` over `A` and `B`, if we have two Bimodule homomorphisms `x` and `y` from `M` to `N`, then if the underlying morphisms of `x` and `y` are equal, it implies that `x` and `y` themselves are equal. In other words, it asserts the principle of equality of Bimodule morphisms in the context of Category Theory.
More concisely: In a monoidal category, if two bimodule homomorphisms between bimodules over the same monoidal objects have equal underlying morphisms, then they are equal as bimodule homomorphisms.
|