Mod_.Hom.ext

theorem Mod_.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {A : Mon_ C} {M N : Mod_ A} (x y : M.Hom N), x.hom = y.hom → x = y

This theorem, `Mod_.Hom.ext`, states that for any category `C` that is a monoidal category, and for any object `A` in the monoidal category `C`, with other objects `M` and `N` in the mod category of `A`, if we have two morphisms `x` and `y` from `M` to `N`, and if the underlying morphism of `x` is equal to the underlying morphism of `y`, then `x` and `y` are the same. In other words, it asserts the uniqueness of morphisms in the context of monoidal categories.

More concisely: In a monoidal category, two morphisms between objects in the monoidal category's module category with equal underlying morphisms are equal.