A basis for SymmetricAlgebra R M

Main definitions

• SymmetricAlgebra.equivMvPolynomial b : SymmetricAlgebra R M ≃ₐ[R] MvPolynomial I R: the isomorphism given by a basis b : Basis I R M.
• Basis.symmetricAlgebra b : Basis (I →₀ ℕ) R (SymmetricAlgebra R M): the basis on the symmetric algebra given by a basis b : Basis I R M.

Main results

• SymmetricAlgebra.instFreeModule: the symmetric algebra over M is free when M is free.
• SymmetricAlgebra.rank_eq: the rank of SymmetricAlgebra R M when M is a nontrivial free module is equal to max (Module.rank R M) Cardinal.aleph0.

Implementation notes

This file closely mirrors the corresponding file for TensorAlgebra.

noncomputable def SymmetricAlgebra.equivMvPolynomial {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) : SymmetricAlgebra R M ≃ₐ[R] MvPolynomial κ R

SymmetricAlgebra.equivMvPolynomial gives an algebra isomorphism between the symmetric algebra over a free module and multivariate polynomials over a basis. This is analogous to TensorAlgebra.equivFreeAlgebra.

Equations

• SymmetricAlgebra.equivMvPolynomial b = AlgEquiv.ofAlgHom (SymmetricAlgebra.lift ((b.constr R) MvPolynomial.X)) (MvPolynomial.aeval fun (i : κ) => (SymmetricAlgebra.ι R M) (b i)) ⋯ ⋯

@[simp]

theorem SymmetricAlgebra.equivMvPolynomial_ι_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) (i : κ) : (equivMvPolynomial b) ((ι R M) (b i)) = MvPolynomial.X i

@[simp]

theorem SymmetricAlgebra.equivMvPolynomial_symm_X {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) (i : κ) : (equivMvPolynomial b).symm (MvPolynomial.X i) = (ι R M) (b i)

theorem SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Type u_1) (b : Module.Basis I R M) : IsSymmetricAlgebra ((b.constr R) MvPolynomial.X)

noncomputable def Module.Basis.symmetricAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : Basis (κ →₀ ℕ) R (SymmetricAlgebra R M)

A basis on M can be lifted to a basis on SymmetricAlgebra R M.

Equations

• b.symmetricAlgebra = (MvPolynomial.basisMonomials κ R).map ↑(SymmetricAlgebra.equivMvPolynomial b).symm

@[simp]

theorem Module.Basis.symmetricAlgebra_repr_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (x : SymmetricAlgebra R M) : b.symmetricAlgebra.repr x = (MvPolynomial.basisMonomials κ R).repr ((SymmetricAlgebra.equivMvPolynomial b) x)

instance SymmetricAlgebra.instModuleFree {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : Module.Free R (SymmetricAlgebra R M)

SymmetricAlgebra R M is free when M is.

instance SymmetricAlgebra.instNoZeroDivisors {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] [Module.Free R M] : NoZeroDivisors (SymmetricAlgebra R M)

The SymmetricAlgebra of a free module over a commutative semiring with no zero-divisors has no zero-divisors.

instance SymmetricAlgebra.instIsDomain {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.Free R M] : IsDomain (SymmetricAlgebra R M)

The TensorAlgebra of a free module over an integral domain is a domain.

theorem SymmetricAlgebra.rank_eq {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Free R M] : Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) Cardinal.aleph0)