Mon_.Hom.ext
theorem Mon_.Hom.ext :
∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
{M N : Mon_ C} (x y : M.Hom N), x.hom = y.hom → x = y
This theorem, `Mon_.Hom.ext`, states that for any category `C` (of a certain type `u₁`), given we have a monoidal structure over `C`, and two monoidal objects `M` and `N` in `C`, if we have two morphisms `x` and `y` from `M` to `N`, then if the underlying homomorphisms of these two morphisms are equal, the morphisms themselves must also be equal. Essentially, it states that for monoidal objects, the morphism between them is determined uniquely by its underlying homomorphism.
More concisely: Given a monoidal category `C` and monoidal objects `M` and `N` in `C` with equal underlying homomorphisms from `M` to `N`, the morphisms from `M` to `N` are equal.
|
Mon_.ext
theorem Mon_.ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
{X Y : Mon_ C} {f g : X ⟶ Y}, f.hom = g.hom → f = g
This theorem states that for any given type `C` (which is a category and a monoidal category) and any two objects `X` and `Y` of the monoidal category `Mon_ C`, if you have two morphisms `f` and `g` from `X` to `Y` such that their corresponding 'hom' fields are equal, then `f` and `g` themselves must be equal. In other words, the 'hom' field uniquely determines the morphism in this context.
More concisely: Given a monoidal category `C` and objects `X`, `Y` in `C`, if there exist morphisms `f` and `g` from `X` to `Y` with equal 'hom' fields, then `f` and `g` are equal.
|