AddMonCat.ext
theorem AddMonCat.ext : ∀ {X Y : AddMonCat} {f g : X ⟶ Y}, (∀ (x : ↑X), f x = g x) → f = g
This theorem, `AddMonCat.ext`, states that for any two objects `X` and `Y` in the category of additive monoids (`AddMonCat`), and for any two morphisms `f` and `g` from `X` to `Y`, if `f` and `g` have the same effect on all elements of `X` (i.e., for all `x` in `X`, `f(x) = g(x)`), then `f` and `g` must be the same morphism. This is a statement about the uniqueness of morphisms in the category of additive monoids subject to a certain condition on their action.
More concisely: In the category of additive monoids, two morphisms with the same effect on all elements are equivalent.
|
MonCat.ext
theorem MonCat.ext : ∀ {X Y : MonCat} {f g : X ⟶ Y}, (∀ (x : ↑X), f x = g x) → f = g
The theorem `MonCat.ext` states that for any two objects `X` and `Y` in the category of monoids `MonCat`, and for any two morphisms `f` and `g` from `X` to `Y`, if `f` and `g` agree on each element `x` of `X` (i.e., `f x = g x` for all `x` in `X`), then `f` and `g` must be the same morphism. This theorem establishes that morphisms in the category of monoids are determined by their action on the elements of the source monoid.
More concisely: In the category of monoids, two morphisms between objects agreeing on all elements are equal.
|