AddMonoidAlgebra.support_gen_of_gen'
theorem AddMonoidAlgebra.support_gen_of_gen' :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddMonoid M] {S : Set (AddMonoidAlgebra R M)},
Algebra.adjoin R S = ⊤ → Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤
The theorem `AddMonoidAlgebra.support_gen_of_gen'` states that for any commutative semiring `R` and any additive monoid `M`, if a set `S` of elements in the monoid algebra `AddMonoidAlgebra R M` generates `R[M]` as an algebra (i.e., every element of `R[M]` can be expressed as a finite `R`-linear combination of elements of `S`), then the image of the union of the supports of the elements of `S` also generates `R[M]` as an algebra.
Here, the support of an element of `AddMonoidAlgebra R M` is the set of the monoid elements that appear in the `R`-linear combination, and `AddMonoidAlgebra.of' R M` is the function embedding the monoid `M` into the monoid algebra `R[M]`.
In simpler terms, if we can build the whole algebra from `S`, then we can also build it from the individual pieces that make up the elements of `S`.
More concisely: If a set of elements in the monoid algebra of a commutative semiring generates the algebra, then the union of the supports of those elements also generates the algebra.
|
AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure
theorem AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure :
∀ {R : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : CommSemiring R] {S : Set M},
AddSubmonoid.closure S = ⊤ → Function.Surjective ⇑(MvPolynomial.aeval fun s => AddMonoidAlgebra.of' R M ↑s)
The theorem `AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure` states that for any set `S` that generates an additive monoid `M` and any commutative semiring `R`, if the closure of `S` equals the top element (i.e., it generates the entire monoid `M`), then the function induced by mapping each element of `M` to the algebra `R[M]` via `MvPolynomial.aeval` (which builds an `R`-algebra homomorphism from multivariate polynomials over `M` to `R[M]`) is surjective. In other words, every element of the `R`-algebra `R[M]` can be written as the image of some multivariate polynomial over `M` under this homomorphism.
More concisely: If `S` generates an additive monoid `M` in a set and the closure of `S` equals `M`, then the homomorphism induced by `MvPolynomial.aeval` from multivariate polynomials over `M` to the algebra `R[M]` is surjective for any commutative semiring `R`.
|
AddMonoidAlgebra.exists_finset_adjoin_eq_top
theorem AddMonoidAlgebra.exists_finset_adjoin_eq_top :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddMonoid M]
[h : Algebra.FiniteType R (AddMonoidAlgebra R M)], ∃ G, Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑G) = ⊤
The theorem `AddMonoidAlgebra.exists_finset_adjoin_eq_top` states that if the algebra `R[M]`, created from the Ring `R` and the Additive Monoid `M`, is of finite type, then there exists a finite set `G` of elements from `M` such that the algebra generated by the image of this set under the embedding of `M` into its monoid algebra completely spans `R[M]`. In other words, every element of `R[M]` can be expressed as a combination of elements from the image of `G` under the `AddMonoidAlgebra.of'` function.
More concisely: If `R[M]`, the algebra over a ring `R` with basis an additive monoid `M` of finite type, can be generated by the images of finitely many elements from `M` under the embedding into `R[M]`.
|
Algebra.FiniteType.iff_quotient_mvPolynomial
theorem Algebra.FiniteType.iff_quotient_mvPolynomial :
∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
Algebra.FiniteType R S ↔ ∃ s f, Function.Surjective ⇑f
An algebra `S` over a commutative semiring `R` is said to be finitely generated if and only if there exists a set `s` and a surjective function `f` such that `S` is a quotient of a polynomial ring whose variables are indexed by `s`. Here, the surjective function `f` maps from the polynomial ring to the algebra `S`, meaning that every element in `S` is the image of some polynomial in the polynomial ring. This theorem is stated for any types `R` and `S` with structures of commutative semirings and `S` having a structure of an `R`-algebra.
More concisely: A commutative semiring algebra S is finitely generated if and only if there exists a surjective homomorphism from a polynomial ring over S's base ring to S.
|
AddMonoidAlgebra.support_gen_of_gen
theorem AddMonoidAlgebra.support_gen_of_gen :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddMonoid M] {S : Set (AddMonoidAlgebra R M)},
Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⋃ f ∈ S, AddMonoidAlgebra.of' R M '' ↑f.support) = ⊤
The theorem `AddMonoidAlgebra.support_gen_of_gen` states that for any commutative semiring `R` and any additive monoid `M`, if a set `S` of elements in the additive monoid algebra of `R` and `M`, generates the entire algebra (i.e., `Algebra.adjoin R S = ⊤`), then the set formed by taking the union over all elements `f` in `S` of the image under the function `AddMonoidAlgebra.of' R M` of the support of `f`, also generates the entire algebra. In other words, the support set of the elements that generate an algebra also generate the same algebra.
More concisely: If a set S of an additive monoid algebra over a commutative semiring generates the entire algebra, then the union of the images under AddMonoidAlgebra.of' of the supports of elements in S also generates the entire algebra.
|
MonoidAlgebra.of_mem_span_of_iff
theorem MonoidAlgebra.of_mem_span_of_iff :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : Monoid M] [inst_2 : Nontrivial R] {m : M} {S : Set M},
(MonoidAlgebra.of R M) m ∈ Submodule.span R (⇑(MonoidAlgebra.of R M) '' S) ↔ m ∈ S
The theorem `MonoidAlgebra.of_mem_span_of_iff` states that for any given commutative ring `R`, monoid `M` with nontrivial ring structure, element `m` of monoid `M`, and a set `S` of elements of type `M`, the image of `m` in the monoid algebra `MonoidAlgebra R M` belongs to the submodule spanned by the image of set `S` under the monoid algebra map if and only if `m` is an element of `S`. In simpler terms, it explains the relationship between an element's membership in a set and its image's membership in a certain submodule of the monoid algebra.
More concisely: For any commutative ring R, monoid M with nontrivial ring structure, and set S of elements in M, an element m of M belongs to S if and only if its image in the monoid algebra MonoidAlgebra R M belongs to the submodule spanned by the images of elements in S.
|
MonoidAlgebra.support_gen_of_gen'
theorem MonoidAlgebra.support_gen_of_gen' :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] {S : Set (MonoidAlgebra R M)},
Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤
This theorem states that if a set `S` generates the monoid algebra `MonoidAlgebra R M` over the commutative semiring `R` and monoid `M`, then the image of the union of the supports of the elements of `S` also generates `MonoidAlgebra R M`. Here, the support of an element of a monoid algebra is the set of monoid elements that appear in the formal sum representing the element of the monoid algebra.
In simpler terms, if you can build every element of the monoid algebra from sums and products of elements of `S`, then you can also build every element from sums and products of monoid elements which appear in those elements of `S`.
More concisely: If a set `S` generates the monoid algebra `MonoidAlgebra R M`, then the image of the union of the supports of the elements in `S` also generates `MonoidAlgebra R M`.
|
MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure
theorem MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure :
∀ {R : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : CommSemiring R] {S : Set M},
Submonoid.closure S = ⊤ → Function.Surjective ⇑(MvPolynomial.aeval fun s => (MonoidAlgebra.of R M) ↑s)
This theorem states: Given a set `S` that generates a monoid `M`, and given that the closure of `S` is the entire set of `M` (i.e., `S` spans the monoid `M`), then the map that evaluates multivariate polynomials at the points indicated by `S` in the algebra over `M` (`MonoidAlgebra R M`) is surjective. In other words, every element of the monoid algebra can be expressed as an image of the multivariate polynomial evaluated at some elements of `S`. This underpins the ability to generate the whole algebra from the image of `M`, when the initial set `S` generates the monoid `M`.
More concisely: Given a monoid `M` generated by a set `S`, if the closure of `S` equals `M`, then the evaluation map from multivariate polynomials to the monoid algebra `MonoidAlgebra R M` is surjective.
|
AddMonoidAlgebra.mem_closure_of_mem_span_closure
theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddMonoid M] [inst_2 : Nontrivial R] {m : M}
{S : Set M},
AddMonoidAlgebra.of' R M m ∈ Submodule.span R ↑(Submonoid.closure (AddMonoidAlgebra.of' R M '' S)) →
m ∈ AddSubmonoid.closure S
This theorem states that for any commutative ring `R` and additive monoid `M`, given any element `m` in `M` and a set `S` of elements in `M`, if the image of `m` under the function `AddMonoidAlgebra.of'` belongs to the submodule generated by the closure of the set `S` (where the set is first mapped via `AddMonoidAlgebra.of'` and then the closure is taken), then `m` must belong to the additive submonoid generated by the closure of `S`. The closure of a set `S` in this context refers to the smallest additive submonoid (or submodule) that contains `S`.
More concisely: If `m` is an element of an additive monoid `M` and the image of `m` under `AddMonoidAlgebra.of'` is in the submodule generated by the closure of a set `S` in a commutative ring `R`, then `m` is in the additive submonoid generated by the closure of `S`.
|
AddMonoidAlgebra.fg_of_finiteType
theorem AddMonoidAlgebra.fg_of_finiteType :
∀ {R : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : CommRing R] [inst_2 : Nontrivial R]
[h : Algebra.FiniteType R (AddMonoidAlgebra R M)], AddMonoid.FG M
The theorem `AddMonoidAlgebra.fg_of_finiteType` states that for any types `R` and `M`, with `R` being a commutative ring and `M` an additive monoid, if the monoid algebra `R[M]` is of finite type (that is, it can be generated by a finite set), then `M` itself is also finitely generated. Here, a finitely generated additive monoid means that there exists a finite subset of `M` such that every element in `M` can be written as a finite sum of elements from this subset.
More concisely: If the monoid algebra over a commutative ring R of an additive monoid M is of finite type, then M is finitely generated.
|
MonoidAlgebra.exists_finset_adjoin_eq_top
theorem MonoidAlgebra.exists_finset_adjoin_eq_top :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : Monoid M]
[h : Algebra.FiniteType R (MonoidAlgebra R M)], ∃ G, Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ↑G) = ⊤
The theorem `MonoidAlgebra.exists_finset_adjoin_eq_top` states that for any commutative ring `R` and any monoid `M`, if the monoid algebra of `R` over `M` is of finite type, then there exists a finite set `G` of elements from `M` such that the image of `G` under the embedding of `M` into its monoid algebra generates the whole algebra. In other words, the algebra generated by this finite set `G` is the entire monoid algebra `MonoidAlgebra R M`.
More concisely: For any commutative ring R and finite type monoid algebra R⊕M, there exists a finite set G ⊆ M such that the subalgebra of R⊕M generated by G equals the entire monoid algebra.
|
Algebra.FiniteType.iff_quotient_freeAlgebra'
theorem Algebra.FiniteType.iff_quotient_freeAlgebra' :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Algebra.FiniteType R A ↔ ∃ ι x f, Function.Surjective ⇑f
This theorem states that an algebra is finitely generated if and only if it can be expressed as a quotient of a polynomial ring whose variables are indexed by a finite type. Specifically, for any commutative semiring `R` and any semiring `A` that forms an algebra over `R`, the algebra `A` is finitely generated (denoted by `Algebra.FiniteType R A`) if and only if there exist a type `ι`, a term `x`, and a function `f` such that the function `f` is surjective. The surjectivity of `f` means that for every element in the target of `f`, there is an element in the domain of `f` that is mapped to it.
More concisely: A commutative algebra `A` over a commutative semiring `R` is finitely generated if and only if it is isomorphic to a quotient of a polynomial ring over `R` with finitely many variables.
|
MonoidAlgebra.mem_adjoin_support
theorem MonoidAlgebra.mem_adjoin_support :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] (f : MonoidAlgebra R M),
f ∈ Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ↑f.support)
The theorem `MonoidAlgebra.mem_adjoin_support` states that for any commutative semiring `R` and any monoid `M`, any element `f` of the Monoid Algebra of `M` over `R` is an element of the subalgebra generated by its support. In other words, `f` belongs to the smallest subalgebra that includes the image of the support of `f` (under the map embedding `M` into its Monoid Algebra) as a subset.
More concisely: For any commutative semiring R and monoid M, every element f in the Monoid Algebra of M over R belongs to the subalgebra generated by the support of f.
|
MonoidAlgebra.mem_closure_of_mem_span_closure
theorem MonoidAlgebra.mem_closure_of_mem_span_closure :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : Monoid M] [inst_2 : Nontrivial R] {m : M} {S : Set M},
(MonoidAlgebra.of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(MonoidAlgebra.of R M) '' S)) →
m ∈ Submonoid.closure S
This theorem is stating that, for any commutative ring `R`, any monoid `M`, and any set `S` of elements of `M`, if the image of an element `m` from `M` under the embedding of `M` into its monoid algebra `MonoidAlgebra R M` belongs to the submodule generated by the closure of `S` under the action of `MonoidAlgebra.of R M`, then `m` is an element of the closure of `S` with respect to the monoid operation in `M`. In simpler terms, if an element's image in the MonoidAlgebra is in the span of the images of some set of elements, then the original element is in the submonoid generated by that set.
More concisely: If `m` is an element of a monoid `M` over a commutative ring `R` such that the image of `m` in the monoid algebra `MonoidAlgebra R M` belongs to the submodule generated by the closure of a set `S` in `M`, then `m` is in the submonoid generated by `S`.
|
MonoidAlgebra.fg_of_finiteType
theorem MonoidAlgebra.fg_of_finiteType :
∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommRing R] [inst_2 : Nontrivial R]
[h : Algebra.FiniteType R (MonoidAlgebra R M)], Monoid.FG M
The theorem `MonoidAlgebra.fg_of_finiteType` states that for any given types `R` and `M`, where `M` is a monoid, `R` is a commutative ring, and `R` is also nontrivial, if the monoid algebra `MonoidAlgebra R M` is of finite type, then the monoid `M` is finitely generated. In mathematical terms, this means that if the algebra constructed by taking the monoid `M` and considering its formal `R`-linear combinations (with the convolution product operation) has finitely many algebraically independent generators, then the monoid `M` itself has finitely many generators.
More concisely: If the monoid algebra of a finitely generated monoid over a commutative and nontrivial ring is of finite type, then the monoid is finitely generated.
|
Algebra.FiniteType.of_surjective
theorem Algebra.FiniteType.of_surjective :
∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B],
Algebra.FiniteType R A → ∀ (f : A →ₐ[R] B), Function.Surjective ⇑f → Algebra.FiniteType R B
This theorem, `Algebra.FiniteType.of_surjective`, states that for all types `R`, `A` and `B` where `R` is a commutative semiring, `A` and `B` are semirings, `R` is an algebra structure on `A` and `B`, if `A` is of finite type over `R`, then for any algebra homomorphism `f` from `A` to `B` that is surjective (every element of `B` is the image under `f` of some element in `A`), we can conclude that `B` is also of finite type over `R`. In mathematical terms, it states that the surjective image of a finitely generated algebra is also a finitely generated algebra.
More concisely: If `A` is a finite type algebra over a commutative semiring `R`, and `f : A → B` is a surjective algebra homomorphism from `A` to another algebra `B` over `R`, then `B` is also of finite type over `R`.
|
Algebra.FiniteType.iff_quotient_freeAlgebra
theorem Algebra.FiniteType.iff_quotient_freeAlgebra :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Algebra.FiniteType R A ↔ ∃ s f, Function.Surjective ⇑f
An algebra, denoted as `A`, over a commutative semiring `R` is said to be finitely generated if and only if there exists a set `s` and function `f` such that `f` is a surjective function. The surjective function means that for every element in the co-domain of `f`, there is at least one corresponding element from its domain. In this context, it is equivalent to say that `A` is a quotient of a free algebra whose variables are indexed by a finite set.
More concisely: An algebra over a commutative semiring is finitely generated if and only if it is isomorphic to a quotient of a free algebra on a finite set.
|
AddMonoidAlgebra.mem_adjoin_support
theorem AddMonoidAlgebra.mem_adjoin_support :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddMonoid M] (f : AddMonoidAlgebra R M),
f ∈ Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑f.support)
The theorem `AddMonoidAlgebra.mem_adjoin_support` states that for any commutative semiring `R` and any additive monoid `M`, any element `f` of the monoid algebra `R[M]` is contained within the subalgebra generated by its support. In other words, each element of the monoid algebra can be expressed as a linear combination of elements from the support of `f`, with coefficients in `R`. This encapsulates the idea that the support of `f` ('support' here meaning the set of elements of `M` that appear with non-zero coefficients in `f`) provides enough 'building blocks' to construct `f` itself within the algebraic structure imposed by `R` and `M`.
More concisely: For every commutative semiring R and additive monoid M, any element f in the monoid algebra R[M] is contained in the subalgebra generated by the support of f.
|
Algebra.FiniteType.iff_quotient_mvPolynomial'
theorem Algebra.FiniteType.iff_quotient_mvPolynomial' :
∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
Algebra.FiniteType R S ↔ ∃ ι x f, Function.Surjective ⇑f
This theorem states that a commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a finite type. In more detail, for any commutative semirings R and S, and any R-algebra structure on S, the algebra is of finite type over R if and only if there exists a finite type ι, a polynomial ring with variables indexed by ι, and a surjective function from the polynomial ring to S.
More concisely: A commutative algebra over a commutative semiring is finitely generated if and only if it is isomorphic to a quotient of a polynomial ring over a finite type index set.
|
RingHom.Finite.to_finiteType
theorem RingHom.Finite.to_finiteType :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B}, f.Finite → f.FiniteType
The theorem `RingHom.Finite.to_finiteType` is an alias of `RingHom.FiniteType.of_finite`. It states that for any two types `A` and `B` that are both commutative rings, and for any ring homomorphism `f` from `A` to `B`, if `f` is finite, then `f` is also of finite type.
More concisely: If `f` is a finite ring homomorphism between commutative rings `A` and `B`, then `f` is of finite type.
|
Module.Finite.injective_of_surjective_endomorphism
theorem Module.Finite.injective_of_surjective_endomorphism :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Finite R M] (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
This theorem, credited to Vasconcelos, states that for a finite module `M` over a commutative ring `R`, any surjective endomorphism of `M` is also injective. An endomorphism of `M` is a linear transformation from `M` to itself. The theorem asserts that if such a transformation is surjective, meaning every element of `M` is the image of some other element under the transformation, then it is also injective, meaning no two different elements of `M` map to the same element. The theorem does not require `M` to be a Noetherian module, but it does require the ring `R` to be commutative. This theorem is a key result in the field of module theory in abstract algebra.
More concisely: A surjective endomorphism of a finite module over a commutative ring is injective.
|
MonoidAlgebra.finiteType_iff_group_fg
theorem MonoidAlgebra.finiteType_iff_group_fg :
∀ {R : Type u_1} {G : Type u_3} [inst : Group G] [inst_1 : CommRing R] [inst_2 : Nontrivial R],
Algebra.FiniteType R (MonoidAlgebra R G) ↔ Group.FG G
This theorem establishes an equivalence between two mathematical properties: a group `G` being finitely generated, and the monoid algebra `R[G]` over a commutative ring `R` being of finite type. Specifically, it states that for any group `G` and any commutative ring `R` with a nontrivial element, `G` is finitely generated if and only if `R[G]` is an algebra of finite type. This means that we can determine whether a group is finitely generated by studying the properties of the algebra formed by its associated monoid algebra over a given commutative ring.
More concisely: A group G is finitely generated if and only if the monoid algebra R[G] over a commutative ring R with a nontrivial element is of finite type.
|
AddMonoidAlgebra.finiteType_iff_fg
theorem AddMonoidAlgebra.finiteType_iff_fg :
∀ {R : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : CommRing R] [inst_2 : Nontrivial R],
Algebra.FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M
The theorem `AddMonoidAlgebra.finiteType_iff_fg` states that for any given additive monoid `M` and commutative ring `R` with nontrivial elements, the monoid algebra `R[M]` is of finite type if and only if `M` is finitely generated. In other words, the algebra generated by `M` over `R` has finitely many basis elements if and only if `M` itself can be generated by a finite set.
More concisely: The monoid algebra of a finitely generated additive monoid over a commutative ring with nontrivial elements is of finite type if and only if the monoid is itself finite.
|
AddMonoidAlgebra.finiteType_iff_group_fg
theorem AddMonoidAlgebra.finiteType_iff_group_fg :
∀ {R : Type u_1} {G : Type u_3} [inst : AddCommGroup G] [inst_1 : CommRing R] [inst_2 : Nontrivial R],
Algebra.FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G
This theorem states that an additive group `G` is finitely generated if and only if the monoid algebra `R[G]` over a commutative ring `R` is of finite type. Here `R[G]` denotes the monoid algebra generated by `G` over `R`, which is the set of finite formal `R`-linear combinations of terms of `G`, with convolution as the product operation. The condition of `R` being nontrivial is also required.
More concisely: A commutative ring R-valued additive group G is finitely generated if and only if its monoid algebra R[G] over R is of finite type.
|
MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure
theorem MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure :
∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommSemiring R] {S : Set M},
Submonoid.closure S = ⊤ → Function.Surjective ⇑((FreeAlgebra.lift R) fun s => (MonoidAlgebra.of R M) ↑s)
Given a set `S` that generates a monoid `M`, and a commutative semiring `R`, the theorem `MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure` states that if the closure of the set `S` in the monoid `M` is the entire monoid `M` (i.e., `Submonoid.closure S = ⊤`), then the function `FreeAlgebra.lift R` applied to the function that maps each element of `S` to the algebra `R[M]` (through `MonoidAlgebra.of R M`) is surjective. In other words, every element in the algebra `R[M]` can be expressed as the image of some element of the monoid `M` under this function.
More concisely: If a set `S` generates a monoid `M` and the closure of `S` in `M` equals the entire monoid, then the function mapping each `S` element to its corresponding algebra element in `R[M]` via `MonoidAlgebra.of R M` is a surjection.
|
AddMonoidAlgebra.of'_mem_span
theorem AddMonoidAlgebra.of'_mem_span :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddMonoid M] [inst_2 : Nontrivial R] {m : M}
{S : Set M}, AddMonoidAlgebra.of' R M m ∈ Submodule.span R (AddMonoidAlgebra.of' R M '' S) ↔ m ∈ S
The theorem `AddMonoidAlgebra.of'_mem_span` states that for any commutative ring `R`, additive monoid `M`, non-trivial structure over `R`, element `m` of `M` and set `S` of `M`, the image of `m` in the monoid algebra `R[M]` belongs to the submodule generated by the set `S` if and only if `m` is an element of `S`. In other words, an element `m` of the additive monoid `M` is contained in the set `S` if and only if its embedding into the monoid algebra `R[M]` belongs to the submodule spanned by the embeddings of the elements of `S` into `R[M]`.
More concisely: For any commutative ring R, additive monoid M, and non-trivial R-module structure on M, an element m in M is contained in a subset S of M if and only if the image of m in the monoid algebra R[M] is contained in the submodule of R[M] generated by the images of elements in S.
|
MonoidAlgebra.finiteType_iff_fg
theorem MonoidAlgebra.finiteType_iff_fg :
∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommRing R] [inst_2 : Nontrivial R],
Algebra.FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M
The theorem `MonoidAlgebra.finiteType_iff_fg` states that for any monoid `M` and any commutative ring `R`, where `R` is nontrivial, the monoid algebra `MonoidAlgebra R M` is of finite type if and only if the monoid `M` is finitely generated. In other words, there is a direct correspondence between the finiteness of the generating set of the monoid and the finiteness of the type of the monoid algebra constructed from this monoid over the commutative ring.
More concisely: The monoid algebra of a finitely generated monoid over a commutative and nontrivial ring is of finite type if and only if the monoid is finite.
|
Algebra.FiniteType.iff_quotient_mvPolynomial''
theorem Algebra.FiniteType.iff_quotient_mvPolynomial'' :
∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
Algebra.FiniteType R S ↔ ∃ n f, Function.Surjective ⇑f
This theorem states that, for any types `R` and `S` that are commutative semirings, with `S` being an `R`-algebra, `S` is finitely generated as an `R`-algebra if and only if there exists an integer `n` and a function `f` such that `f` is surjective onto `S`. Here, a function being surjective means that for every element in `S`, there exists an element in the domain of `f` that maps to it. The quotient of a polynomial ring in `n` variables is a way of referring to the codomain of such a surjective function `f`.
More concisely: A commutative semiring `S` is finitely generated as an `R`-algebra if and only if there exists a surjective `R`-algebra homomorphism from a polynomial ring in `n` variables over `R` to `S` for some integer `n`.
|
MonoidAlgebra.support_gen_of_gen
theorem MonoidAlgebra.support_gen_of_gen :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] {S : Set (MonoidAlgebra R M)},
Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⋃ f ∈ S, ⇑(MonoidAlgebra.of R M) '' ↑f.support) = ⊤
This theorem states that, for any commutative semiring `R` and any monoid `M`, whenever a set `S` of elements of the monoid algebra of `R` and `M` generates the whole monoid algebra as an algebra, then the set of all supports of elements of `S`, under the standard monoid algebra embedding, also generates the whole monoid algebra. Here, the support of an element of the monoid algebra is the set of monoid elements that appear with non-zero coefficients in the linear combination defining the algebra element.
More concisely: If a set of elements in the monoid algebra of a commutative semiring and a monoid generates the algebra, then the supports of its elements under the standard embedding also generate the algebra.
|
AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure
theorem AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure :
∀ {R : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : CommSemiring R] {S : Set M},
AddSubmonoid.closure S = ⊤ → Function.Surjective ⇑((FreeAlgebra.lift R) fun s => AddMonoidAlgebra.of' R M ↑s)
This theorem states that if a set `S` generates an additive monoid `M`, then the image of `M` under a particular function generates the algebra `R[M]`. More specifically, given a type `R` that forms a commutative semiring and a type `M` that forms an additive monoid, if `S` is a subset of `M` such that the additive submonoid generated by `S` is the entire set `M` (`AddSubmonoid.closure S = ⊤`), then the function that lifts elements of `M` to the free algebra over `R` and then maps them to a monoid algebra (specifically the mapping `s => AddMonoidAlgebra.of' R M ↑s`, which is then lifted to a morphism of `R`-algebras via `FreeAlgebra.lift R`) is surjective. This implies that every element of the algebra `R[M]` can be obtained as the image of some element of `M` under this function.
More concisely: If a subset `S` of an additive monoid `M` generates `M` and forms a carrier for the free algebra over a commutative semiring `R`, then the resulting homomorphism from `R[M]` to the monoid algebra `R[M]` is surjective.
|