NonUnitalAlgHom.ext
theorem NonUnitalAlgHom.ext :
∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
[inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
[inst_5 : DistribMulAction S B] {f g : A →ₛₙₐ[φ] B}, (∀ (x : A), f x = g x) → f = g
The theorem `NonUnitalAlgHom.ext` states that for any types `R`, `A`, and `B`, given that `R` is a monoid, `A` and `B` are non-unital non-associative semirings, and `A` and `B` are also both distributive mul-action over `R`, then for any two functions `f` and `g` from `A` to `B` that preserve the ring structure and scalar multiplication (`A →ₙₐ[R] B`), if `f` and `g` are equal for every element of `A`, then `f` and `g` are identical functions. In other words, two such ring homomorphisms `f` and `g` are determined by their action on the elements of `A`.
More concisely: If `R` is a monoid, `A` and `B` are non-unital non-associative semirings, and `A` and `B` are distributive over `R`, then any two `R`-homomorphisms from `A` to `B` that agree on all elements of `A` are equal.
|
NonUnitalAlgHom.map_mul'
theorem NonUnitalAlgHom.map_mul' :
∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
[inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
[inst_5 : DistribMulAction S B] (self : A →ₛₙₐ[φ] B) (x y : A),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that for any types `R`, `S`, `A`, and `B`, given monoid structures on `R` and `S`, non-unital non-associative semiring structures on `A` and `B`, distributive multiplication actions of `R` on `A` and `S` on `B`, and a non-unital algebra homomorphism `self` from `A` to `B` that respects a given monoid homomorphism `φ` from `R` to `S`, the function represented by `self` preserves multiplication. In other words, applying `self` to the product of two elements in `A` is the same as multiplying the results of applying `self` to the individual elements.
More concisely: For monoids R and S, semirings A and B with distributive R-action on A and S-action on B, and a non-unital algebra homomorphism self from A to B respecting a given monoid homomorphism φ from R to S, self preserves multiplication: self (a1 \* a2) = self a1 \* self a2.
|