Symmetric Algebras

Given a commutative semiring R, and an R-module M, we construct the symmetric algebra of M. This is the free commutative R-algebra generated (R-linearly) by the module M.

Notation

• SymmetricAlgebra R M: a concrete construction of the symmetric algebra defined as a quotient of the tensor algebra. It is endowed with an R-algebra structure and a commutative ring structure.
• SymmetricAlgebra.ι R: the canonical R-linear map M →ₗ[R] SymmetricAlgebra R M.

Note

See SymAlg R instead if you are looking for the symmetrized algebra, which gives a commutative multiplication on R by $a \circ b = \frac{1}{2}(ab + ba)$.

inductive TensorAlgebra.SymRel (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorAlgebra R M → TensorAlgebra R M → Prop

Relation on the tensor algebra which will yield the symmetric algebra when quotiented out by.

• mul_comm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x y : M) : SymRel R M ((ι R) x * (ι R) y) ((ι R) y * (ι R) x)

@[reducible, inline]

abbrev SymmetricAlgebra (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)

Concrete construction of the symmetric algebra of M by quotienting out the tensor algebra by the commutativity relation.

@[reducible, inline]

abbrev SymmetricAlgebra.algHom (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorAlgebra R M →ₐ[R] SymmetricAlgebra R M

Algebra homomorphism from the tensor algebra over M to the symmetric algebra over M.

theorem SymmetricAlgebra.algHom_surjective (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Surjective ⇑(algHom R M)

def SymmetricAlgebra.ι (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] SymmetricAlgebra R M

Canonical inclusion of M into the symmetric algebra SymmetricAlgebra R M.

theorem SymmetricAlgebra.induction (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {motive : SymmetricAlgebra R M → Prop} (algebraMap : ∀ (r : R), motive ((algebraMap R (SymmetricAlgebra R M)) r)) (ι : ∀ (x : M), motive ((ι R M) x)) (mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)) (add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)) (a : SymmetricAlgebra R M) : motive a

instance SymmetricAlgebra.instCommSemiring (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : CommSemiring (SymmetricAlgebra R M)

instance SymmetricAlgebra.instCommRing (R : Type u_3) (M : Type u_4) [CommRing R] [AddCommMonoid M] [Module R M] : CommRing (SymmetricAlgebra R M)

def SymmetricAlgebra.lift {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] : (M →ₗ[R] A) ≃ (SymmetricAlgebra R M →ₐ[R] A)

For any linear map f : M →ₗ[R] A, SymmetricAlgebra.lift f lifts the linear map to an R-algebra homomorphism from SymmetricAlgebra R M to A.

@[simp]

theorem SymmetricAlgebra.lift_ι_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] (f : M →ₗ[R] A) (a : M) : (lift f) ((ι R M) a) = f a

@[simp]

theorem SymmetricAlgebra.lift_comp_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] (f : M →ₗ[R] A) : ↑(lift f) ∘ₗ ι R M = f

theorem SymmetricAlgebra.algHom_ext {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {F G : SymmetricAlgebra R M →ₐ[R] A} (h : ↑F ∘ₗ ι R M = ↑G ∘ₗ ι R M) : F = G

theorem SymmetricAlgebra.algHom_ext_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {F G : SymmetricAlgebra R M →ₐ[R] A} : F = G ↔ ↑F ∘ₗ ι R M = ↑G ∘ₗ ι R M

@[simp]

theorem SymmetricAlgebra.lift_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : lift (ι R M) = AlgHom.id R (SymmetricAlgebra R M)

def SymmetricAlgebra.algebraMapInv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : SymmetricAlgebra R M →ₐ[R] R

The left-inverse of algebraMap.

theorem SymmetricAlgebra.algebraMap_leftInverse {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.LeftInverse ⇑algebraMapInv ⇑(algebraMap R (SymmetricAlgebra R M))

@[simp]

theorem SymmetricAlgebra.algebraMap_inj {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (x y : R) : (algebraMap R (SymmetricAlgebra R M)) x = (algebraMap R (SymmetricAlgebra R M)) y ↔ x = y

@[simp]

theorem SymmetricAlgebra.algebraMap_eq_zero_iff {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : R) : (algebraMap R (SymmetricAlgebra R M)) x = 0 ↔ x = 0

@[simp]

theorem SymmetricAlgebra.algebraMap_eq_one_iff {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : R) : (algebraMap R (SymmetricAlgebra R M)) x = 1 ↔ x = 1

instance SymmetricAlgebra.instNontrivial {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] : Nontrivial (SymmetricAlgebra R M)

A SymmetricAlgebra over a nontrivial semiring is nontrivial.