FreeAddMagma.hom_ext
theorem FreeAddMagma.hom_ext :
∀ {α : Type u} {β : Type v} [inst : Add β] {f g : AddHom (FreeAddMagma α) β},
⇑f ∘ FreeAddMagma.of = ⇑g ∘ FreeAddMagma.of → f = g
This theorem states that for any types `α` and `β`, where `β` has an addition operation, if we have two addition homomorphisms `f` and `g` from the free additive magma of `α` to `β`, then if the composition of `f` or `g` with the inclusion of `α` into the free additive magma is the same, it follows that `f` and `g` must be the same. In simpler terms, this theorem provides a uniqueness condition for homomorphisms from the free additive magma of one type to another type with addition.
More concisely: If `α` is any type with an addition operation and `f` and `g` are homomorphisms from the free additive magma of `α` to a type `β` with addition, then `f` and `g` are equal if and only if their compositions with the inclusion of `α` into the free additive magma are equal.
|
FreeAddSemigroup.hom_ext
theorem FreeAddSemigroup.hom_ext :
∀ {α : Type u} {β : Type v} [inst : Add β] {f g : AddHom (FreeAddSemigroup α) β},
⇑f ∘ FreeAddSemigroup.of = ⇑g ∘ FreeAddSemigroup.of → f = g
The theorem `FreeAddSemigroup.hom_ext` asserts that for any two types `α` and `β`, with `β` as an additive type, and any two additive homomorphisms `f` and `g` from the free additive semigroup of `α` to `β`, if these two homomorphisms agree on the embedding of `α` into the free additive semigroup of `α`, then these homomorphisms are identical. In other words, if two additive homomorphisms from the free additive semigroup of `α` to `β` coincide on the elements of `α` (viewed as elements of the free additive semigroup of `α` via the canonical embedding), then they are the same function.
More concisely: If `f` and `g` are additive homomorphisms from the free additive semigroup of `α` to an additive type `β`, and `f` and `g` agree on the embedding of `α` into the free additive semigroup of `α`, then `f` is equal to `g`.
|
FreeMagma.hom_ext
theorem FreeMagma.hom_ext :
∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeMagma α →ₙ* β},
⇑f ∘ FreeMagma.of = ⇑g ∘ FreeMagma.of → f = g
This theorem, "FreeMagma.hom_ext", states that for any two types α and β-- where β is a multiplication structure-- given any two functions `f` and `g` from the free magma of α to β, if the application of `f` after the "FreeMagma.of" function equals the application of `g` after the "FreeMagma.of" function, then `f` and `g` must be the same function. This theorem is a statement about function extensionality in the context of free magmas: two homomorphisms from a free magma to another structure are equal if they agree on the generator of the free magma.
More concisely: In the context of free magmas, two functions from a free magma to a multiplication structure are equal if they map the same elements to the same image under the "FreeMagma.of" function.
|
FreeSemigroup.hom_ext
theorem FreeSemigroup.hom_ext :
∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeSemigroup α →ₙ* β},
⇑f ∘ FreeSemigroup.of = ⇑g ∘ FreeSemigroup.of → f = g
This theorem states that for any types `α` and `β`, where `β` has a multiplication operation, and given two monoid homomorphisms `f` and `g` from the free semigroup over `α` to `β`, if these homomorphisms map elements from `α` (embedded into the free semigroup over `α` using `FreeSemigroup.of`) to the same element in `β`, then the two homomorphisms are identical. In other words, the theorem asserts the uniqueness of a monoid homomorphism from the free semigroup over a set, given its effect on the elements of the set.
More concisely: Given any types `α` and `β` with a multiplication operation, and given two monoid homomorphisms `f` and `g` from the free semigroup over `α` to `β`, if `f (FreeSemigroup.of x) = g (FreeSemigroup.of x)` for all `x` in `α`, then `f = g`.
|