Subalgebra.algebraMap_mem'
theorem Subalgebra.algebraMap_mem' :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(self : Subalgebra R A) (r : R), (algebraMap R A) r ∈ self.carrier
The theorem `Subalgebra.algebraMap_mem'` states that for any commutative semiring `R`, any semiring `A`, and any `R`-algebra structure on `A`, the image of any element `r` in `R` under the algebra map from `R` to `A` always lies in the underlying set of any subalgebra of `A`. In other words, the action of the algebra map on `R` is always within the specified subalgebra of `A`.
More concisely: Given a commutative semiring R, an R-algebra A, and an R-algebra structure on A, the image of any r in R under the algebra map lies in every subalgebra of A.
|
Subalgebra.smul_mem
theorem Subalgebra.smul_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) {x : A}, x ∈ S → ∀ (r : R), r • x ∈ S
This theorem, `Subalgebra.smul_mem`, states that for any given types R and A, where R is a commutative semiring and A is a semiring with an algebra structure over R, and for any subalgebra S of A, if an element x belongs to S, then the scaling of x by any scalar r from R also belongs to S. In other words, the scalar multiplication of any element in the subalgebra by any scalar in R remains within the subalgebra.
More concisely: For any commutative semiring R, semiring A with an algebra structure over R, and subalgebra S of A, if x is in S and r is in R, then r \* x is in S. (Here, \* denotes scalar multiplication.)
|
Subalgebra.mul_mem
theorem Subalgebra.mul_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) {x y : A}, x ∈ S → y ∈ S → x * y ∈ S
This theorem states that for any types `R` and `A`, given a commutative semiring structure on `R`, a semiring structure on `A`, and an algebra structure between `R` and `A`, if `S` is a subalgebra of `R` in `A`, then the product of any two elements `x` and `y` in `S` is also in `S`. In other words, the subalgebra `S` is closed under multiplication.
More concisely: For any commutative semirings `R` and `A`, and an algebra homomorphism from `R` to `A`, if `S` is a subalgebra of `R` in `A`, then `S` is closed under multiplication.
|
Mathlib.Algebra.Algebra.Subalgebra.Basic._auxLemma.11
theorem Mathlib.Algebra.Algebra.Subalgebra.Basic._auxLemma.11 :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
(x ∈ ⊤) = True
This theorem, `Mathlib.Algebra.Algebra.Subalgebra.Basic._auxLemma.11`, states that for any type `R`, any type `A`, given that `R` is a commutative semiring, `A` is a semiring, and `A` is an algebra over `R`, then for any element `x` of `A`, `x` belongs to the top element (in the sense of a topological space or the universal set in a set theory context) is always true. In simpler terms, this is saying that any element of an algebra is in the universal set.
More concisely: For any commutative semiring `R`, semiring `A`, and algebra `A` over `R`, every element `x` in `A` belongs to the universally-quantified set `A`.
|
Subalgebra.equivOfEq.proof_2
theorem Subalgebra.equivOfEq.proof_2 :
∀ {R : Type u_2} {A : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S T : Subalgebra R A), S = T → Subalgebra.toSubmodule S = Subalgebra.toSubmodule T
This theorem, `Subalgebra.equivOfEq.proof_2`, states that for any types `R` and `A`, with `R` being a commutative semiring and `A` a semiring on which `R` is an algebra, if `S` and `T` are two subalgebras of `A` over `R` that are equal, then the corresponding submodules of `S` and `T` obtained by the forgetful map from subalgebra to submodule, `Subalgebra.toSubmodule`, are also equal.
More concisely: If `R` is a commutative semiring and `A` is an `R`-algebra, then equal `R`-subalgebras `S` and `T` of `A` have equal corresponding submodules `Subalgebra.toSubmodule S` and `Subalgebra.toSubmodule T`.
|
Subalgebra.zero_mem
theorem Subalgebra.zero_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A), 0 ∈ S
This theorem states that, given any subalgebra `S` of an algebra `A` over a commutative semiring `R`, the zero element (0) of the algebra `A` is always an element of the subalgebra `S`. This is an inherent property of subalgebras, which are non-empty subsets of an algebra that are themselves algebras, and therefore must contain the zero element.
More concisely: Given any subalgebra S of an algebra A over a commutative semiring R, the zero element of A is an element of S.
|
Algebra.mem_top
theorem Algebra.mem_top :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A}, x ∈ ⊤
This theorem states that, for any given types `R` and `A`, with `R` being a commutative semiring, `A` being a semiring, and `A` being an algebra over `R`, any element `x` of type `A` is an element of the top element (denoted by `⊤`). This indicates that every element `x` in `A` is included in the biggest possible subset of `A` given the algebraic structure.
More concisely: For any commutative semiring R and semiring A being an algebra over R, every element x in A is contained in the top element ⊤ of A.
|
Algebra.gc
theorem Algebra.gc :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
GaloisConnection (Algebra.adjoin R) SetLike.coe
This theorem, `Algebra.gc`, states that for any commutative semiring `R` and any semiring `A` where `A` is an algebra over `R`, a Galois connection exists between the function `Algebra.adjoin R` and `SetLike.coe`.
In other words, for any subset `s` in `A` and any subalgebra `a` in `A`, the property that `s` is contained in the set of the subalgebra `a` is equivalent to the property that the subalgebra generated by `s` is contained or equal to `a`.
More concisely: For any commutative semiring `R` and its algebra `A`, there exists a Galois connection between the inclusion of subsets in `A` and the subalgebras of `A`, relating subset containment to subalgebra inclusion.
|
AlgHom.mem_range
theorem AlgHom.mem_range :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) {y : B}, y ∈ φ.range ↔ ∃ x, φ x = y
The theorem `AlgHom.mem_range` states that for any commutative semiring `R`, semirings `A` and `B`, and algebra structures over `A` and `B`, given an algebra homomorphism `φ` from `A` to `B` and an element `y` of `B`, `y` belongs to the range of `φ` if and only if there exists an element `x` in `A` such that `φ(x) = y`. In other words, it is checking whether a particular element of `B` can be obtained by applying the algebraic homomorphism `φ` to some element of `A`.
More concisely: For any commutative semirings R, semirings A and B, and algebra structures on A and B, an algebra homomorphism φ from A to B sends an element x in A to y in B if and only if y is in the image of φ.
|
Algebra.map_top
theorem Algebra.map_top :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Subalgebra.map f ⊤ = f.range
The theorem `Algebra.map_top` states that for any commutative semiring `R`, semirings `A` and `B`, and an algebra homomorphism `f` from `A` to `B` with both `A` and `B` being `R`-algebras, the application of the `Subalgebra.map` function on `f` and the top subalgebra of `A` results in the same subalgebra as the range of `f` when viewed as an algebra homomorphism. In other words, the image of the entire algebra `A` under the algebra homomorphism `f` is precisely the range of `f`.
More concisely: For any commutative semiring R, semirings A and B, and an algebra homomorphism f from A to B with both A and B being R-algebras, the image of the top subalgebra of A under f, through Subalgebra.map, equals the range of f as an R-algebra homomorphism.
|
AlgHom.coe_range
theorem AlgHom.coe_range :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), ↑φ.range = Set.range ⇑φ
This theorem asserts that for all commutative semirings `R`, semirings `A` and `B`, and algebras `A` and `B` over `R`, the set of elements in the range of any algebra homomorphism `φ` from `A` to `B` over `R` (denoted as `AlgHom.range φ`) is identical to the set of elements obtained by applying the function `φ` to all possible arguments (denoted as `Set.range φ`). In other words, it equates the set of outputs of `φ` considered as an algebra homomorphism, with the set of its outputs considered merely as a function.
More concisely: For any commutative semirings R, semirings A and B, and algebra homomorphisms φ from A to B over R, the image of φ as an algebra homomorphism equals the image of φ considered as a function, i.e., AlgHom.range φ = Set.range φ.
|
Subalgebra.sum_mem
theorem Subalgebra.sum_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ι → A}, (∀ x ∈ t, f x ∈ S) → (t.sum fun x => f x) ∈ S
The theorem `Subalgebra.sum_mem` states that for any given commutative semiring `R` and semiring `A` with an algebra structure over `R`, subalgebra `S` of `A`, finite set `t` and a function `f` mapping from `t` to `A`, if every element `f x` for `x` in `t` belongs to the subalgebra `S`, then the sum of `f x` over all `x` in `t`, denoted by `Finset.sum t f`, also belongs to the subalgebra `S`. In mathematical terms, this means that a subalgebra is closed under finite summation.
More concisely: If `R` is a commutative semiring, `A` is an `R`-algebra, `S` is a subalgebra of `A`, `t` is a finite set, and `f : t → A` is a function such that `f x ∈ S` for all `x ∈ t`, then `Finset.sum t f ∈ S`.
|
Subalgebra.pow_mem
theorem Subalgebra.pow_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) {x : A}, x ∈ S → ∀ (n : ℕ), x ^ n ∈ S
This theorem states that for any commutative semiring `R`, a semiring `A`, and an algebra structure on `A` over `R`, if `x` is an element of a certain subalgebra `S` of `A` over `R`, then `x` raised to any natural number power `n` is also an element of the subalgebra `S`. In other words, the subalgebra is closed under exponentiation with natural number exponents.
More concisely: If `R` is a commutative semiring, `A` is a semiring with an algebra structure over `R`, and `S` is a subalgebra of `A`, then for all `x ∈ S` and `n ∈ ℕ`, `x^n ∈ S`.
|
Subalgebra.add_mem
theorem Subalgebra.add_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) {x y : A}, x ∈ S → y ∈ S → x + y ∈ S
This theorem states that for any commutative semiring `R`, any semiring `A`, and any algebra structure over `R` and `A`, if `S` is a subalgebra of `A` over `R` and if `x` and `y` are elements of `S`, then the sum of `x` and `y` is also an element of `S`. In other words, the sum of any two elements in a subalgebra of an algebra is also in the subalgebra, showing that the subalgebra is closed under addition.
More concisely: Given a commutative semiring `R`, an algebra `A` over `R`, a subalgebra `S` of `A` over `R`, and elements `x`, `y` in `S`, the sum `x + y` is also in `S`.
|
Subalgebra.mem_toSubring
theorem Subalgebra.mem_toSubring :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A}
{x : A}, x ∈ S.toSubring ↔ x ∈ S
This theorem states that for any given types `R` and `A`, where `R` is a commutative ring, `A` is a ring, and `A` is an algebra over `R`, and given a subalgebra `S` of `A` over `R` and an element `x` of `A`, `x` is an element of the subring of `A` obtained from the subalgebra `S` if and only if `x` is an element of the subalgebra `S`. In other words, an element belongs to the subring corresponding to a subalgebra if and only if it belongs to the original subalgebra.
More concisely: For any commutative ring R, rings A over R, and subalgebras S of A over R, an element x of A belongs to the subring generated by S if and only if it belongs to S.
|
Subalgebra.one_mem
theorem Subalgebra.one_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A), 1 ∈ S
This theorem states that for any subalgebra `S` of an algebra `A` over a commutative semiring `R`, the multiplicative identity element `1` is an element of `S`. Here, `A` is a semiring and `R` is a commutative semiring, with `A` being an algebra over `R`. In the context of algebra, a subalgebra is a subset of an algebra that is closed under the operations of addition, scalar multiplication, and multiplication.
More concisely: In any subalgebra S of an algebra A over a commutative semiring R, the multiplicative identity 1 of R is an element of S.
|
algebraMap_mem
theorem algebraMap_mem :
∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : SetLike S A] [inst_4 : OneMemClass S A] [inst_5 : SMulMemClass S R A] (s : S) (r : R),
(algebraMap R A) r ∈ s
This theorem, `algebraMap_mem`, asserts that for any given types `S`, `R`, and `A`, with `R` being a commutative semiring, `A` being a semiring, and `A` having an algebraic structure over `R`, if `S` is a set-like structure in `A` that contains the multiplicative identity and respects scalar multiplication from `R` to `A`, then for any element `s` of `S` and any element `r` of `R`, the result of applying the algebra map from `R` to `A` to `r` is an element of `S`. In simpler terms, it states that the algebra map from a commutative semiring to a semiring always maps elements into a set that is compatible with the algebraic structure.
More concisely: Given a commutative semiring `R`, a semiring `A` with an algebra structure over `R`, and a set-like `S` in `A` containing the multiplicative identity and respecting scalar multiplication, for all `s in S` and `r in R`, `(algMap R A r) in S`.
|
Algebra.toSubmodule_bot
theorem Algebra.toSubmodule_bot :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Subalgebra.toSubmodule ⊥ = 1
The theorem `Algebra.toSubmodule_bot` states that for any commutative semiring `R` and any semiring `A` that is also an `R`-algebra, when the "bottom" (i.e., the smallest possible) subalgebra of `A` is mapped to a submodule of `A` using the function `Subalgebra.toSubmodule`, the result is the "unit" (or one) submodule. In other words, the smallest subalgebra corresponds to the unit submodule under the consider mapping.
More concisely: The smallest subalgebra of an `R`-algebra `A` maps to the unit submodule under the function `Subalgebra.toSubmodule` for any commutative semiring `R`.
|
Subalgebra.ext
theorem Subalgebra.ext :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
{S T : Subalgebra R A}, (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any two subalgebras 'S' and 'T' of a given algebra 'A' over a commutative semiring 'R', if every element 'x' of the algebra 'A' belongs to 'S' if and only if it belongs to 'T', then the two subalgebras 'S' and 'T' are equal. The algebra 'A' is a semiring and it becomes an algebra over 'R' with additional structure from 'R'.
More concisely: If two subalgebras S and T of a commutative semiring R-algebra A have the same elements, then they are equal.
|
Algebra.mem_bot
theorem Algebra.mem_bot :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R A)
The theorem `Algebra.mem_bot` states that for any given types `R` and `A`, where `R` is a commutative semiring, `A` is a semiring, and `A` is an `R`-algebra, any element `x` of type `A` is in the zero ideal (denoted by `⊥`) if and only if `x` is in the range of the algebra map from `R` to `A`. In other words, `x` can be expressed as the image of some element from `R` under the algebra map. The algebra map (`algebraMap`) is the ring homomorphism associated with the `Algebra` structure from `R` to `A`. The set range of a function `f` (denoted by `Set.range`) consists of all possible output values `x` for which there exists an input `y` such that `f(y) = x`.
More concisely: For any commutative semiring R, semiring A, and R-algebra A, an element x of A belongs to the zero ideal if and only if it is the image of some element in R under the algebra map.
|
Algebra.coe_sInf
theorem Algebra.coe_sInf :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Set (Subalgebra R A)), ↑(sInf S) = ⋂ s ∈ S, ↑s
This theorem, `Algebra.coe_sInf`, states that for any two types `R` and `A`, given instances of `R` being a commutative semiring, `A` being a semiring, and an algebra structure over `R` and `A`, if `S` is a set of subalgebras of `R` and `A`, then the set of elements included in the infimum (`sInf`) of `S` is equal to the intersection of the sets of elements included in each subalgebra in `S`. In mathematical terms, given a collection of subalgebras `S` of an algebra structure over a commutative semiring `R` and a semiring `A`, the underlying set of the infimum of `S` is the intersection of the underlying sets of the subalgebras in `S`.
More concisely: For any commutative semiring `R`, semiring `A`, and an algebra structure over `R` and `A`, the underlying set of the infimum of a collection `S` of subalgebras of `R` and `A` is equal to the intersection of the underlying sets of the subalgebras in `S`.
|
Algebra.eq_top_iff
theorem Algebra.eq_top_iff :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
{S : Subalgebra R A}, S = ⊤ ↔ ∀ (x : A), x ∈ S
This theorem, `Algebra.eq_top_iff`, states that for any given types `R` and `A` with `R` being a commutative semiring and `A` a semiring, and given an algebra structure between `R` and `A`; for any subalgebra `S` of `A` over `R`, `S` is equal to the top element (`⊤`) if and only if every element `x` of type `A` is contained in `S`. In other words, a subalgebra is equal to the whole algebra if and only if it contains every element of the algebra.
More concisely: A subalgebra of a commutative semiring `A` over a commutative semiring `R` is equal to the top element of `A` if and only if it contains every element of `A`.
|
Subalgebra.range_val
theorem Subalgebra.range_val :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A), S.val.range = S
The theorem `Subalgebra.range_val` states that for any subalgebra `S` of an algebra `A` over a commutative semiring `R`, the range of the algebra homomorphism that embeds the subalgebra `S` into the algebra `A` is the subalgebra `S` itself. In other words, if we consider all elements in `A` that can be obtained by applying this homomorphism to elements of `S`, we get exactly the set of elements in `S`.
More concisely: The range of the algebra homomorphism embedding a subalgebra into an algebra over a commutative semiring is equal to the subalgebra itself.
|
Subalgebra.algebraMap_mem
theorem Subalgebra.algebraMap_mem :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) (r : R), (algebraMap R A) r ∈ S
This theorem states that for any commutative semiring `R`, semiring `A`, and algebra structure of `R` on `A`, if we have a subalgebra `S` of `A` over `R` and any element `r` of `R`, then the algebra map (which is a ring homomorphism) of `r` from `R` to `A` is in `S`. Essentially, this means that the image of any element from the base ring `R` under the algebra map is always in the subalgebra `S`. This is a fundamental property of subalgebras.
More concisely: For any commutative semiring `R`, semiring `A`, algebra structure of `R` on `A`, subalgebra `S` of `A` over `R`, and element `r` in `R`, the algebra map of `r` from `R` to `A` belongs to `S`.
|
Subalgebra.copy_eq
theorem Subalgebra.copy_eq :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A) (s : Set A) (hs : s = ↑S), S.copy s hs = S
This theorem states that for any commutative semiring `R`, any semiring `A`, and any algebra structure on `A` over `R`, for any subalgebra `S` of `A` over `R` and a set `s` of `A`, if `s` is equal to the carrier of `S`, then the subalgebra obtained by copying `S` with carrier `s` is equal to `S` itself. In other words, creating a copy of a subalgebra with a carrier identical to the original does not change the subalgebra.
More concisely: For any commutative semiring `R`, semiring `A`, algebra structure on `A` over `R`, subalgebra `S` of `A` over `R`, and set `s` equal to the carrier of `S`, the subalgebra of `A` with carrier `s` equal to `S` holds. (i.e., the subalgebra obtained by copying `S` with carrier `s` is equal to `S` itself.)
|
Subalgebra.range_subset
theorem Subalgebra.range_subset :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
(S : Subalgebra R A), Set.range ⇑(algebraMap R A) ⊆ ↑S
The theorem `Subalgebra.range_subset` states that for any commutative semiring `R`, any semiring `A` and any algebra structure over `R` and `A`, and for any subalgebra `S` of `A` over `R`, the range of the algebra map from `R` to `A` is a subset of `S`. The algebra map refers to the embedding given by the algebra structure. This theorem is essentially stating that all the elements in `R` that are mapped to `A` via the algebra structure are included in the given subalgebra `S` of `A`.
More concisely: For any commutative semiring R, semiring A, algebra structure over R and A, and subalgebra S of A, the image of R under the algebra map is contained in S.
|
Subalgebra.sub_mem
theorem Subalgebra.sub_mem :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
{x y : A}, x ∈ S → y ∈ S → x - y ∈ S
This theorem states that for any commutative ring `R` and any ring `A`, where `A` is an algebra over `R`, and `S` is a subalgebra of `A`, if `x` and `y` are elements of `S`, then the difference of `x` and `y` (denoted as `x - y`) is also an element of `S`. In other words, the difference of any two elements in a subalgebra of an algebra remains within that subalgebra.
More concisely: If `R` is a commutative ring, `A` is an algebra over `R`, and `S` is a subalgebra of `A`, then for all `x, y ∈ S`, `x - y ∈ S`.
|
Algebra.top_toSubmodule
theorem Algebra.top_toSubmodule :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Subalgebra.toSubmodule ⊤ = ⊤
This theorem states that, for any commutative semiring `R` and any semiring `A` with a given algebra structure, the top `Subalgebra` of `A` over `R`, when mapped through the forgetful function `Subalgebra.toSubmodule`, gives the top `Submodule` of `A` over `R`. In other words, the largest subalgebra (the whole algebra) corresponds to the largest submodule under the forgetful map from `Subalgebra` to `Submodule`.
More concisely: The top subalgebra of an algebra over a commutative semiring, when mapped through the forgetful function to submodules, equals the top submodule.
|