DistribMulActionHom.ext
theorem DistribMulActionHom.ext :
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4}
[inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B]
[inst_5 : DistribMulAction N B] {f g : A →ₑ+[φ] B}, (∀ (x : A), f x = g x) → f = g
This theorem, `DistribMulActionHom.ext`, states that for any monoid `M`, any two types `A` and `B` that are both additively monoid and have a distributive multiplication action by `M`, and any two distributive multiplication action homomorphisms from `A` to `B` denoted as `f` and `g`, if `f` and `g` are equal for all elements `x` of `A` then `f` and `g` are equal as homomorphisms. In simple terms, if two transformations from `A` to `B` are always equal when applied to any element of `A`, then these transformations are considered identical.
More concisely: If `f` and `g` are two distributive multiplication action homomorphisms from additively monoid `A` to additively monoid `B` with distributive multiplication over `M`, and `f(x) = g(x)` for all `x` in `A`, then `f = g` as homomorphisms.
|
MulSemiringActionHom.map_one'
theorem MulSemiringActionHom.map_one' :
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10}
[inst_2 : Semiring R] [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S]
[inst_5 : MulSemiringAction N S] (self : R →ₑ+*[φ] S), self.toFun 1 = 1
This theorem states that for any two types `M` and `N`, which are monoids, and any function `φ` mapping `M` to `N`, if `R` and `S` are semirings where `M` acts on `R` and `N` acts on `S` in a way that respects the semiring structure (i.e., a multiplication semiring action), then any semiring action homomorphism from `R` to `S` under `φ` preserves the multiplicative identity, i.e., the image of `1` under this homomorphism is also `1`.
More concisely: For any monoid homomorphism φ between monoids M and N, if M acts on semirings R and N via multiplication respecting their semiring structures, then any semiring homomorphism f from R to S under φ maps the multiplicative identity of R to that of S.
|
MulSemiringActionHom.map_mul'
theorem MulSemiringActionHom.map_mul' :
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10}
[inst_2 : Semiring R] [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S]
[inst_5 : MulSemiringAction N S] (self : R →ₑ+*[φ] S) (x y : R),
self.toFun (x * y) = self.toFun x * self.toFun y
The theorem `MulSemiringActionHom.map_mul'` states that for any two elements `x` and `y` of a semiring `R` acted on by a monoid `M`, and a homomorphism `φ` from `M` to another monoid `N` acting on a semiring `S`, a semiring homomorphism preserving the action of the monoids `M` and `N` preserves multiplication. Specifically, the result of applying this homomorphism to the product of `x` and `y` is equal to the product of the results of applying this homomorphism individually to `x` and `y`.
More concisely: Given a semiring `R`, a monoid `M` acting on `R`, a homomorphism `φ` from `M` to another monoid `N` acting on a semiring `S`, and semiring homomorphisms `ρ_R : R → S` and `ρ_N : M → N`, then `ρ_R (x * y) = ρ_R (x) * ρ_N (μ (x, y))`, where `μ` is the monoid multiplication in `M`.
|
DistribMulActionHom.map_zero'
theorem DistribMulActionHom.map_zero' :
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4}
[inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B]
[inst_5 : DistribMulAction N B] (self : A →ₑ+[φ] B), self.toFun 0 = 0
The theorem `DistribMulActionHom.map_zero'` states that, for any two monoids `M` and `N`, a function `φ` that maps `M` to `N`, and two additive monoids `A` and `B` that also have a distributive multiplication action from `M` and `N` respectively, if we have a function `self` that maps `A` to `B` preserving the addition and the multiplication action, then this function maps the zero element of `A` to the zero element of `B`. Essentially, it asserts that the function `self` preserves the zero element under these conditions.
More concisely: If `φ: M -> N` is a function between monoids `M` and `N`, `A` and `B` are additive monoids with distributive multiplication actions from `M` and `N` respectively, and `self: A -> B` preserves addition and multiplication actions of `M` and `N`, then `self(0_A) = 0_B`.
|
MulActionHom.map_smul'
theorem MulActionHom.map_smul' :
∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
(self : X →ₑ[φ] Y) (m : M) (x : X), self.toFun (m • x) = φ m • self.toFun x
This theorem, named `MulActionHom.map_smul'`, states that for any types `M`, `N`, `X`, and `Y`, along with a function `φ` from `M` to `N`, the function `self` (which is a equivariant map from `X` to `Y`) commutes with the scalar multiplication. More specifically, if `X` is a space on which `M` operates and `Y` is a space on which `N` operates, then applying `self` to the result of scaling `x` by `m` in `X` (notated as `m • x`) is the same as scaling the result of applying `self` to `x` by `φ m` in `Y` (notated as `φ m • self.toFun x`).
More concisely: For any equivariant map `self` from a module `X` over a type `M` to a module `Y` over a type `N`, and any `m` in `M` and `x` in `X`, `self (m • x) = φ m • self x`, where `φ` is a function from `M` to `N`.
|
DistribMulActionHom.map_add'
theorem DistribMulActionHom.map_add' :
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4}
[inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B]
[inst_5 : DistribMulAction N B] (self : A →ₑ+[φ] B) (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
This theorem states that for any two elements `x` and `y` of an additive monoid `A` which has a distributive multiplication action by a monoid `M`, any function that maps `A` to another additive monoid `B` (which also has a distributive multiplication action, but by a monoid `N`), and is a homomorphism between the multiplicative structures (`M →* N`), preserves the addition operation. In other words, if you add `x` and `y` and then apply the function, you get the same result as if you apply the function to `x` and `y` separately and then add the results.
More concisely: For any additive monoids A and B with distributive multiplication actions by monoids M and N, respectively, and any additive homomorphism f : M → N, the diagram commutes: x + y ↝ f(x + y) = f(x) + f(y).
|