algebraMap_smul
theorem algebraMap_smul :
∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
[inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : IsScalarTower R A M] (r : R)
(m : M), (algebraMap R A) r • m = r • m
This theorem, `algebraMap_smul`, states that for any commutative semiring `R`, semiring `A`, commutative monoid `M`, provided that `M` is a module over both `R` and `A`, and also `R` forms a scalar tower over `A` and `M`, then the action of scalar multiplication by `r` in `R` on `m` in `M` is the same whether we consider `r` as an element of `R` or as an element of `A` through the embedding given by the algebra structure. In other words, the scalar multiplication operation is consistent across the scalar tower.
More concisely: For any commutative semirings R and A, commutative monoid M being an R-A module with R forming a scalar tower over A, the scalar multiplication by r in R on m equals the scalar multiplication by r in A, for all r in R and m in M.
|
NoZeroSMulDivisors.algebraMap_injective
theorem NoZeroSMulDivisors.algebraMap_injective :
∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Nontrivial A] [inst_3 : Algebra R A]
[inst_4 : NoZeroSMulDivisors R A], Function.Injective ⇑(algebraMap R A)
This theorem, `NoZeroSMulDivisors.algebraMap_injective`, states that for any types `R` and `A`, where `R` is a commutative ring, `A` is a nontrivial ring and there exists an algebra structure from `R` to `A`, then the function given by the algebra structure (`algebraMap`) from `R` to `A` is injective, provided that there are no zero scalar multiplication divisors in the algebra from `R` to `A`. In other words, if you multiply by any non-zero scalar from `R` in `A`, you get a non-zero result and the mapping from `R` to `A` distinct elements in `R` are mapped to distinct elements in `A`.
More concisely: Given a commutative ring `R`, a nontrivial ring `A`, and an algebra structure from `R` to `A` with no zero scalar multiplication divisors, the algebra map from `R` to `A` is injective.
|
Module.algebraMap_end_apply
theorem Module.algebraMap_end_apply :
∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] [inst_6 : SMul R S]
[inst_7 : IsScalarTower R S M] (a : R) (m : M), ((algebraMap R (Module.End S M)) a) m = a • m
This theorem states that for any commutative semiring `R`, semiring `S`, and an additive commutative monoid `M` that is also a module over both `R` and `S`, and assuming `R` and `S` action on `M` commute (`SMulCommClass S R M`) and `S` acts on `R` (`SMul R S`), forming a scalar tower (`IsScalarTower R S M`), the application of the algebra map from `R` to the endomorphisms of the `S`-module `M` to an element `a` from `R` and `m` from `M` is equivalent to the scalar multiplication of `m` by `a`. In LaTeX notation, for any `a` in `R` and `m` in `M`, it is true that `(algebraMap R (Module.End S M)) a m = a • m`.
More concisely: Given a commutative semiring `R`, semiring `S`, and an additive commutative `R-S`-module `M` with commuting actions and scalar tower property, the application of the algebra map from `R` to the endomorphisms of `M` to an element `a` from `R` and `m` from `M` equals the scalar multiplication of `m` by `a`, i.e., `(algebraMap R (Module.End S M)) a m = a • m`.
|
NoZeroSMulDivisors.of_algebraMap_injective
theorem NoZeroSMulDivisors.of_algebraMap_injective :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : NoZeroDivisors A], Function.Injective ⇑(algebraMap R A) → NoZeroSMulDivisors R A
The theorem `NoZeroSMulDivisors.of_algebraMap_injective` states that if the function `algebraMap R A`, which embeds a commutative semiring `R` into a semiring `A` in the context of an algebra structure, is injective, and if `A` has no zero divisors (meaning that the product of two non-zero elements in `A` is always non-zero), then any product in `A` that is a multiple of an element from `R` is zero if and only if one of the factors is zero. This theorem cannot be an instance as there is no `Injective (algebraMap R A)` typeclass.
More concisely: If `algebraMap R A` embeds a commutative semiring `R` into a semiring `A` with no zero divisors and is injective, then for all `x, y in A`, `x * y = 0` implies `x = 0` or `y = 0`.
|
algebraMap_int_eq
theorem algebraMap_int_eq : ∀ (R : Type u_1) [inst : Ring R], algebraMap ℤ R = Int.castRingHom R
This theorem, `algebraMap_int_eq`, states that for any type `R` that has a ring structure, the algebra map from the integers `ℤ` to `R` is identical to the ring homomorphism that casts integers to `R`. In other words, the function embedding the integers `ℤ` into `R` via the algebra structure is the same as the function that simply casts integers to elements of `R`.
More concisely: The algebra map from the integers to a ring is equal to the ring homomorphism that casts integers to elements of that ring.
|
smul_algebra_smul_comm
theorem smul_algebra_smul_comm :
∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
[inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : IsScalarTower R A M] (r : R)
(a : A) (m : M), a • r • m = r • a • m
This theorem states that for any commutative semiring `R`, any semiring `A` that is also an `R`-algebra, and any additively commutative monoid `M` that is an `A`-module and an `R`-module (with `R`, `A` and `M` forming a scalar tower), scalar multiplication is commutative with respect to `R` and `A`. In other words, for any elements `r` in `R`, `a` in `A`, and `m` in `M`, the operations of scalar multiplication `a • r • m` and `r • a • m` are equal.
More concisely: For any commutative semiring `R`, `R-algebra `A`, `A-module and `R-module `M` forming a scalar tower, the scalar multiplication of elements in `A` by elements in `R` commutes with the scalar multiplication of `M` by both `A` and `R`.
|
Module.End_algebraMap_isUnit_inv_apply_eq_iff
theorem Module.End_algebraMap_isUnit_inv_apply_eq_iff :
∀ {R : Type u} (S : Type v) {M : Type w} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] [inst_6 : SMul R S]
[inst_7 : IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m m' : M),
↑h.unit⁻¹ m = m' ↔ m = x • m'
This theorem states that for any commutative semiring `R`, type `S`, module `M` over `R`, where `S` and `M` are also modules and there exists a commutative action and a scalar multiplication with `R` and `S` on `M`, and `R` is a scalar tower over `S` and `M`, if `x` is an element of `R` which becomes a unit when mapped to the endomorphisms of the module via the algebraic structure, then for any two elements `m` and `m'` of the module, the inverse of the unit corresponding to `x` applied to `m` equals `m'` if and only if `m` equals `x` scaled by `m'`.
More concisely: For any commutative semiring `R`, module `M` over `R` with commutative action and scalar multiplication, if `x` in `R` is a unit when mapped to endomorphisms and `m` and `m'` are elements of `M` such that `x * m = m'`, then the inverse of `x` maps `m` to `m'`.
|
IsUnit.algebraMap_of_algebraMap
theorem IsUnit.algebraMap_of_algebraMap :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B),
f 1 = 1 → ∀ {r : R}, IsUnit ((algebraMap R A) r) → IsUnit ((algebraMap R B) r)
This theorem states that for any types `R`, `A`, and `B` such that `R` is a commutative semiring, `A` and `B` are semirings, and `A` and `B` are both `R`-algebras, if there exists a linear map `f` from `A` to `B` that preserves the identity element (i.e., `f(1) = 1`), then for any element `r` of `R`, if `r` is a unit under the algebra map from `R` to `A`, then `r` is also a unit under the algebra map from `R` to `B`.
In other words, if an element is a unit in the `R`-algebra `A`, and there is a linear map from `A` to another `R`-algebra `B` preserving the identity, then this element is a unit in `B` as well.
More concisely: If `R` is a commutative semiring, `A` and `B` are `R`-algebras that are semirings, `f` is a linear map from `A` to `B` preserving the identity, and `r` is a unit in `A` under the algebra map from `R` to `A`, then `r` is a unit in `B` under the algebra map from `R` to `B`.
|
RingHom.map_rat_algebraMap
theorem RingHom.map_rat_algebraMap :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Algebra ℚ R]
[inst_3 : Algebra ℚ S] (f : R →+* S) (r : ℚ), f ((algebraMap ℚ R) r) = (algebraMap ℚ S) r
This theorem states that for any two semirings `R` and `S`, both having an algebra structure over the rational numbers (`ℚ`), and given a ring homomorphism `f` from `R` to `S`, the application of `f` after mapping a rational number `r` into `R` using the algebra map is the same as directly mapping `r` into `S` using its respective algebra map. Symbolically, for all rational numbers `r`, `f((algebraMap ℚ R) r) = (algebraMap ℚ S) r`. This theorem essentially says that the algebraic structure of the semirings preserves the action of the ring homomorphism.
More concisely: For any semirings `R` and `S` with algebra structures over the rational numbers, and for any ring homomorphism `f` from `R` to `S`, the algebra maps commute, i.e., `f(algebraMapℚ R r) = algebraMapℚ S r` for all rational numbers `r`.
|
algebra_compatible_smul
theorem algebra_compatible_smul :
∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
[inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : IsScalarTower R A M] (r : R)
(m : M), r • m = (algebraMap R A) r • m
The theorem `algebra_compatible_smul` states that for any types `R` and `A` where `R` is a commutative semiring and `A` is a semiring with an algebra structure over `R`, and for any type `M` which is an additive commutative monoid and also a module over `A` and `R` with a scalar tower structure, the action of scalar multiplication by an element `r` from `R` on an element `m` from `M` is the same as the action of scalar multiplication by the image of `r` under the algebra map from `R` to `A` on `m`. In other words, the scalar multiplication operation is compatible with the algebra map.
More concisely: For any commutative semiring `R`, semiring `A` with an algebra structure over `R`, additive commutative monoid `M` that is an `A`-module and `R`-module with scalar tower structure, the scalar multiplication of an `A`-element `r` and an `M`-element `m` equals the scalar multiplication of `m` by `r`'s image under the algebra map.
|
LinearMap.map_algebraMap_mul
theorem LinearMap.map_algebraMap_mul :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R),
f ((algebraMap R A) r * a) = (algebraMap R B) r * f a
The theorem `LinearMap.map_algebraMap_mul` states that for all types `R`, `A`, `B` with `R` being a commutative semiring, `A` and `B` being semirings, and `A` and `B` being `R`-algebras, for any linear map `f` from `A` to `B` over `R`, any element `a` from `A`, and any element `r` from `R`, the image of the product of the algebra embedding of `r` into `A` and `a` under `f` is the same as the product of the algebra embedding of `r` into `B` and the image of `a` under `f`. In terms of mathematical notation, this is saying that for all $r \in R$ and $a \in A$, we have $f((\text{algebraMap } R \rightarrow A)(r) \cdot a) = (\text{algebraMap } R \rightarrow B)(r) \cdot f(a)$. This theorem provides an alternative statement of `LinearMap.map_smul` for when `algebraMap` is more convenient to work with than scalar multiplication.
More concisely: For any commutative semiring R, semirings A and B, and R-algebras A and B, for all linear maps f from A to B, elements r in R, and a in A, we have f(r • a) = r • f(a). (Here, • denotes the algebra multiplication.)
|