Documentation

Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

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 #

Note #

See SymAlg R instead if you are looking for the symmetrized algebra, which gives a commutative multiplication on R by ab=12(ab+ba).

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

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

@[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.

Equations
@[reducible, inline]

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

Equations

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

Equations
theorem SymmetricAlgebra.induction (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {motive : SymmetricAlgebra R MProp} (algebraMap : ∀ (r : R), motive ((algebraMap R (SymmetricAlgebra R M)) r)) (ι : ∀ (x : M), motive ((ι R M) x)) (mul : ∀ (a b : SymmetricAlgebra R M), motive amotive bmotive (a * b)) (add : ∀ (a b : SymmetricAlgebra R M), motive amotive bmotive (a + b)) (a : SymmetricAlgebra R M) :
motive a
Equations
  • One or more equations did not get rendered due to their size.
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] :

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.

Equations
@[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] :
@[simp]
theorem SymmetricAlgebra.algebraMap_inj {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (x y : R) :
@[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

A SymmetricAlgebra over a nontrivial semiring is nontrivial.