Algebra.commutes
theorem Algebra.commutes :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x : A),
(algebraMap R A) r * x = x * (algebraMap R A) r
This theorem, called `Algebra.commutes`, states that for any commutative semiring `R`, semiring `A`, and `Algebra` structure between them, multiplication is commutative when one of the elements is from the base ring `R`. More specifically, for any element `r` from `R` and `x` from `A`, the product of the algebra map of `r` and `x` is the same as the product of `x` and the algebra map of `r`. In mathematical terms, this can be written as `(algebraMap R A) r * x = x * (algebraMap R A) r`.
More concisely: For any commutative semiring `R`, semiring `A` with an algebra structure over `R`, and elements `r in R` and `x in A`, the algebra product `(algebraMap R A) r * x` equals the algebra product `x * (algebraMap R A) r`.
|
Algebra.mul_smul_comm
theorem Algebra.mul_smul_comm :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : R) (x y : A),
x * s • y = s • (x * y)
This theorem, `Algebra.mul_smul_comm`, states that for any commutative semiring `R`, semiring `A`, and `R`-algebra `A`, and for any elements `s` in `R` and `x`, `y` in `A`, the operation `x * (s • y)` is equal to `s • (x * y)`. Here, `*` represents the multiplication operation in the semiring `A` and `s • y` denotes the scalar multiplication of `s` and `y`. Essentially, this theorem is saying that scalar multiplication can be "commuted" with multiplication in the algebra.
More concisely: For any commutative semiring `R`, semiring `A`, and `R`-algebra `A` with elements `s` in `R` and `x`, `y` in `A`, the scalar multiplication `s • y` commutes with the multiplication `x * y` in `A`, i.e., `x * (s • y) = s • (x * y)`.
|
Algebra.smul_mul_assoc
theorem Algebra.smul_mul_assoc :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x y : A),
r • x * y = r • (x * y)
This theorem, `Algebra.smul_mul_assoc`, states that for any commutative semiring `R`, semiring `A`, and an algebra structure over them, the scalar multiplication and multiplication operations are associative. In other words, given an element `r` from `R` and elements `x` and `y` from `A`, multiplying `r`-scaled `x` with `y` is the same as scaling the multiplication of `x` and `y` by `r`. Mathematically, this can be represented as `r*(x*y) = (r*x)*y`. This is a special case of a more general property, `smul_mul_assoc`, and requires less typeclass search.
More concisely: For any commutative semiring `R`, semiring `A`, and algebra structure over them, the scalar multiplication and multiplication operations are associative, i.e., `r*(x * y) = (r * x) * y` for all `r` in `R` and elements `x` and `y` in `A`.
|
Algebra.smul_def
theorem Algebra.smul_def :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x : A),
r • x = (algebraMap R A) r * x
The theorem `Algebra.smul_def` states that for any commutative semiring `R` and any semiring `A` with an algebra structure, the scalar multiplication of an element `r` from `R` and an element `x` from `A` is defined as the multiplication of `x` and the image of `r` under the algebra map from `R` to `A`. In mathematical terms, given `r ∈ R` and `x ∈ A`, we have `r • x = (algebraMap R A) r * x`.
More concisely: For any commutative semiring `R` and algebra `A` over it, scalar multiplication `r • x` equals the product of `x` and the algebra map image of `r`, i.e., `r • x = (algebraMap R A) r * x`.
|
Algebra.algebra_ext
theorem Algebra.algebra_ext :
∀ {R : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] (P Q : Algebra R A),
(∀ (r : R), (algebraMap R A) r = (algebraMap R A) r) → P = Q
This theorem states that to show equivalence between two algebra structures, `P` and `Q`, on a fixed pair of commutative semiring `R` and semiring `A`, it is enough to show that their corresponding `algebraMap`s, which are the embeddings from `R` to `A` defined by these algebra structures, agree for all elements `r` of `R`. In other words, if for every element `r` from `R`, the result of applying `algebraMap` under algebra structure `P` is the same as applying `algebraMap` under algebra structure `Q`, then the two algebra structures `P` and `Q` are the same.
More concisely: If for all elements \(r\) in a commutative semiring \(R\), the algebra maps \(P(r)\) and \(Q(r)\) from algebra structures \(P\) and \(Q\) over semiring \(A\) agree, then \(P\) and \(Q\) are equal algebra structures.
|
Algebra.algebraMap_eq_smul_one
theorem Algebra.algebraMap_eq_smul_one :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
(algebraMap R A) r = r • 1
This theorem 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 element `r` in `R`, the algebra map (which is the embedding of `R` into `A` defined by the algebra structure) of `r` is equal to `r` times the multiplicative identity element in `A`. In mathematical terms, this means that for any `r` in `R`, we have that `algebraMap R A r = r * 1_A`, where `1_A` denotes the multiplicative identity in `A`.
More concisely: For any commutative semiring `R` and semiring `A` with an algebra structure over `R`, the algebra map embeds each element `r` in `R` as `r * 1_A` in `A`.
|
Algebra.algebraMap_eq_smul_one'
theorem Algebra.algebraMap_eq_smul_one' :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
⇑(algebraMap R A) = fun r => r • 1
The theorem `Algebra.algebraMap_eq_smul_one'` states that for any commutative semiring `R`, semiring `A` and given an algebra structure over `R` and `A`, the function defined by the embedding `algebraMap` from `R` to `A` is equivalent to the function that takes an element `r` from `R` and returns the result of 'scalar multiplication' of `r` with the multiplicative identity `1` in `A`. This theorem formalizes the intuition that the map induced by the algebra structure 'scales' elements of `R` by the identity in `A`.
More concisely: For any commutative semiring `R`, semiring `A`, and algebra structure over `R` and `A`, the algebra map from `R` to `A` is equal to the function that scales elements of `R` by the multiplicative identity of `A`.
|
algebraMap.coe_one
theorem algebraMap.coe_one :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ↑1 = 1 := by
sorry
This theorem, `algebraMap.coe_one`, states that for any two types `R` and `A`, where `R` is a commutative semiring and `A` is a semiring with an algebra structure over `R`, the algebraic map of the number 1 from `R` to `A` equals 1 in `A`. In more mathematical terms, given any commutative semiring `R` and any semiring `A` that has `R` as an algebra, the image of 1 in `R` under the algebra map is 1 in `A`. This theorem essentially underlines one of the basic properties of algebra maps: they must preserve the multiplicative identity.
More concisely: For any commutative semiring `R` and semiring `A` with `R` being an algebra over `A`, the algebra map of `1` from `R` to `A` equals `1` in `A`.
|
Algebra.right_comm
theorem Algebra.right_comm :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (r : R)
(y : A), x * (algebraMap R A) r * y = x * y * (algebraMap R A) r
The theorem `Algebra.right_comm` states that for any commutative semiring `R`, semiring `A`, and any algebra structure from `R` to `A`, and for any elements `x` and `y` from the semiring `A`, and any element `r` from the semiring `R`, the multiplication of `x`, the image of `r` under the algebra map into `A`, and `y` is commutative. That is, `x * (algebraMap R A) r * y = x * y * (algebraMap R A) r`, where `*` denotes the multiplication operation. This theorem essentially extends the property of right commutativity from the base ring `R` to the algebra `A`.
More concisely: For any commutative semirings R and A, algebra homomorphism f : R -> A, and elements x, y in A and r in R, we have x * f(r) * y = x * y * f(r).
|
algebraMap.coe_zero
theorem algebraMap.coe_zero :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ↑0 = 0 := by
sorry
This theorem states that, for any commutative semiring `R`, any semiring `A`, and any algebra structure over `R` and `A`, the algebra map of `0` (from `R` to `A`) is equal to `0` in `A`. In other words, the image of `0` under any algebra mapping is `0`. This is a consequence of the definition of an algebra over a ring, where the algebra map must preserve addition and scalar multiplication, which in particular implies that it must send `0` to `0`.
More concisely: For any commutative semiring `R`, any semiring `A`, and any algebra structure over `R` and `A`, the algebra map of `0` from `R` to `A` equals `0` in `A`.
|
Algebra.left_comm
theorem Algebra.left_comm :
∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (r : R)
(y : A), x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)
This theorem, `Algebra.left_comm`, asserts the left-commutativity property of multiplication in an Algebra over a base ring. Specifically, given an algebra `A` over a commutative semiring `R`, an element `x` from `A`, an element `r` from `R`, and another element `y` from `A`, the multiplication of `x` with the product of `r` (mapped from `R` to `A` using the algebra structure) and `y` is the same as the multiplication of `r` (again, mapped into `A`) with the product of `x` and `y`. This is usually expressed in the following algebraic form: `x * (r * y) = r * (x * y)` for all `x ∈ A, r ∈ R, y ∈ A`.
More concisely: For all algebras A over a commutative semiring R, and all elements x in A and r in R and y in A, we have x * (r * y) = r * (x * y).
|
Algebra.id.smul_eq_mul
theorem Algebra.id.smul_eq_mul : ∀ {R : Type u} [inst : CommSemiring R] (x y : R), x • y = x * y
This theorem states that for any commutative semiring `R` and any two elements `x` and `y` of `R`, the operation of scalar multiplication of `x` and `y` is the same as their standard multiplication. In mathematical terms, for all `x` and `y` in `R`, `x` scalar multiplied by `y` is equal to `x` times `y`.
More concisely: For any commutative semiring `R`, the operation of scalar multiplication of `x` and `y` equals the standard multiplication of `x` and `y`, for all `x` and `y` in `R`.
|