Subalgebra.mul_toSubmodule
theorem Subalgebra.mul_toSubmodule :
∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
(S T : Subalgebra R A), Subalgebra.toSubmodule S * Subalgebra.toSubmodule T = Subalgebra.toSubmodule (S ⊔ T)
The theorem `Subalgebra.mul_toSubmodule` states that for any commutative semi-ring `A` with a commutative semi-ring `R` and an algebra structure between `R` and `A`, and any two subalgebras `S` and `T` of `A` over `R`, the multiplication of the submodules corresponding to `S` and `T` (obtained via the forgetful map from `Subalgebra` to `Submodule`) is equal to the submodule corresponding to the join of `S` and `T` (`S ⊔ T`). This is a significant structural property that connects the algebraic operations in the larger algebra `A` to those in its subalgebras `S` and `T`.
More concisely: For any commutative semi-rings `A` and `R` with an algebra structure between `R` and `A`, and subalgebras `S` and `T` of `A`, the submodule of `A` generated by the products of elements from `S` and `T` is equal to the join of the submodules generated by `S` and `T`.
|
Subalgebra.mul_self
theorem Subalgebra.mul_self :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A), Subalgebra.toSubmodule S * Subalgebra.toSubmodule S = Subalgebra.toSubmodule S
The theorem `Subalgebra.mul_self` asserts that for any commutative semiring `R`, semiring `A`, and algebra `A` over `R`, and for any subalgebra `S` of `A`, the submodule corresponding to `S` (obtained by the `Subalgebra.toSubmodule` mapping) is idempotent under multiplication. In simpler terms, if you multiply the submodule corresponding to the subalgebra `S` by itself, you get the same submodule back.
More concisely: For any commutative semiring R, semiring A, algebra A over R, subalgebra S of A, the submodule of A generated by S is idempotent under multiplication.
|