GroupCat.ext
theorem GroupCat.ext : ∀ {X Y : GroupCat} {f g : X ⟶ Y}, (∀ (x : ↑X), f x = g x) → f = g
This theorem states that for any two group objects `X` and `Y` in the category of groups (denoted as `GroupCat`), and any two morphisms `f` and `g` from `X` to `Y`, if for every element `x` in `X` the morphisms `f` and `g` map `x` to the same element in `Y` (denoted by `f x = g x`), then the morphisms `f` and `g` are the same (denoted by `f = g`). In other words, two morphisms between the same two groups in the category of groups are equal if they agree on all elements of the domain group.
More concisely: In the category of groups, two morphisms between the same groups are equal if and only if they map every element in their domain to the same element in the target group.
|
CommGroupCat.ext
theorem CommGroupCat.ext : ∀ {X Y : CommGroupCat} {f g : X ⟶ Y}, (∀ (x : ↑X), f x = g x) → f = g
This theorem states that for any two commutative groups `X` and `Y` in the category of commutative groups (`CommGroupCat`), and any two morphisms `f` and `g` from `X` to `Y`, if the application of `f` and `g` to any element `x` of `X` gives the same result, then `f` and `g` must be the same morphism. In other words, two morphisms in the category of commutative groups are equal if they have the same action on all elements of the domain group.
More concisely: In the category of commutative groups, two morphisms between groups are equal if and only if they map every element in the domain to the same image.
|
AddGroupCat.ext
theorem AddGroupCat.ext : ∀ {X Y : AddGroupCat} {f g : X ⟶ Y}, (∀ (x : ↑X), f x = g x) → f = g
This theorem states that for any two objects `X` and `Y` in the category of additive groups (`AddGroupCat`), if two morphisms `f` and `g` from `X` to `Y` satisfy the property that for every element `x` in `X`, the image of `x` under `f` is the same as the image of `x` under `g`, then `f` and `g` are the same morphism. In other words, two morphisms in the category of additive groups are considered equal if they map every element of the source group to the same element in the target group.
More concisely: In the category of additive groups, two morphisms between objects are equal if and only if they map every group element to the same image.
|
AddCommGroupCat.ext
theorem AddCommGroupCat.ext : ∀ {X Y : AddCommGroupCat} {f g : X ⟶ Y}, (∀ (x : ↑X), f x = g x) → f = g
This theorem states that for any two objects `X` and `Y` in the category of additive commutative groups (`AddCommGroupCat`), if there are two morphisms `f` and `g` from `X` to `Y`, and for all elements `x` in `X`, `f(x)` is equal to `g(x)`, then the morphisms `f` and `g` are equal. In other words, it says that two morphisms between additive commutative groups are equal if they agree on all elements of the source group.
More concisely: In the category of additive commutative groups, if two morphisms between objects agree on all elements of the source group, then they are equal.
|