Generators of symmetric algebras

The canonical map from a module over a commutative semiring into its symmetric algebra is injective, without a freeness assumption. Its main application is that an abelian Lie algebra embeds in its universal enveloping algebra, which is its symmetric algebra (TauCeti.UniversalEnvelopingAlgebra.ι_injective_of_isLieAbelian).

For the symmetric algebra of the base semiring itself, the degree-one element ι R R 1 generates the whole algebra. An algebra morphism whose range contains this element is therefore surjective, a criterion used for coordinate morphisms of additive root subgroups.

A ring homomorphism out of a symmetric algebra is determined by its values on scalars and on generators (SymmetricAlgebra.ringHom_ext).

theorem TauCeti.SymmetricAlgebra.ι_injective (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Injective ⇑(SymmetricAlgebra.ι R M)

The canonical map into the symmetric algebra is injective for every module over a commutative semiring.

theorem SymmetricAlgebra.ringHom_ext {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] {F G : SymmetricAlgebra R M →+* A} (h₁ : ∀ (r : R), F ((algebraMap R (SymmetricAlgebra R M)) r) = G ((algebraMap R (SymmetricAlgebra R M)) r)) (h₂ : ∀ (m : M), F ((ι R M) m) = G ((ι R M) m)) : F = G

A ring homomorphism out of a symmetric algebra is determined by its values on scalars and on generators.

theorem AlgHom.surjective_of_ι_one_mem_range {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (f : A →ₐ[R] SymmetricAlgebra R R) (hgen : (SymmetricAlgebra.ι R R) 1 ∈ f.range) : Function.Surjective ⇑f

An algebra morphism into the symmetric algebra of the base semiring is surjective if its range contains the degree-one generator.