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.
• Given a morphism ι : M →ₗ[R] A, IsSymmetricAlgebra ι is a proposition saying that the algebra homomorphism from SymmetricAlgebra R M to A lifted from ι is bijective.
• Given a linear map f : M →ₗ[R] A' to a commutative R-algebra A', and a morphism ι : M →ₗ[R] A with p : IsSymmetricAlgebra ι, IsSymmetricAlgebra.lift p f is the lift of f to an R-algebra morphism A →ₐ[R] A'.

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.

def IsSymmetricAlgebra {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) : Prop

Given a morphism f : M →ₗ[R] A, IsSymmetricAlgebra f is a proposition saying that the algebra homomorphism from SymmetricAlgebra R M to A is bijective.

theorem SymmetricAlgebra.isSymmetricAlgebra_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : IsSymmetricAlgebra (ι R M)

noncomputable def IsSymmetricAlgebra.equiv {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} (h : IsSymmetricAlgebra f) : SymmetricAlgebra R M ≃ₐ[R] A

For f : M →ₗ[R] A, construct the algebra isomorphism SymmetricAlgebra R M ≃ₐ[R] A from IsSymmetricAlgebra f.

@[simp]

theorem IsSymmetricAlgebra.equiv_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} (h : IsSymmetricAlgebra f) (a : SymmetricAlgebra R M) : h.equiv a = (SymmetricAlgebra.lift f) a

@[simp]

theorem IsSymmetricAlgebra.equiv_toAlgHom {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} (h : IsSymmetricAlgebra f) : ↑h.equiv = SymmetricAlgebra.lift f

@[simp]

theorem IsSymmetricAlgebra.equiv_symm_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} (h : IsSymmetricAlgebra f) (a : M) : h.equiv.symm (f a) = (SymmetricAlgebra.ι R M) a

@[simp]

theorem IsSymmetricAlgebra.equiv_symm_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} (h : IsSymmetricAlgebra f) : ↑↑h.equiv.symm ∘ₗ f = SymmetricAlgebra.ι R M

theorem IsSymmetricAlgebra.of_equiv {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} (e : SymmetricAlgebra R M ≃ₐ[R] A) (he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f) : IsSymmetricAlgebra f

theorem IsSymmetricAlgebra.comp_equiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] (e : SymmetricAlgebra R M ≃ₐ[R] A) : IsSymmetricAlgebra (e.toLinearMap ∘ₗ SymmetricAlgebra.ι R M)

noncomputable def IsSymmetricAlgebra.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] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f) {A' : Type u_4} [CommSemiring A'] [Algebra R A'] (g : M →ₗ[R] A') : A →ₐ[R] A'

Given a morphism g : M →ₗ[R] A', lift this to a morphism of type A →ₐ[R] A' (where A satisfies the universal property of the symmetric algebra of M)

@[simp]

theorem IsSymmetricAlgebra.lift_eq {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} (h : IsSymmetricAlgebra f) {A' : Type u_4} [CommSemiring A'] [Algebra R A'] (g : M →ₗ[R] A') (a : M) : (h.lift g) (f a) = g a

@[simp]

theorem IsSymmetricAlgebra.lift_comp_linearMap {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} (h : IsSymmetricAlgebra f) {A' : Type u_4} [CommSemiring A'] [Algebra R A'] (g : M →ₗ[R] A') : ↑(h.lift g) ∘ₗ f = g

theorem IsSymmetricAlgebra.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 : M →ₗ[R] A} {A' : Type u_4} [CommSemiring A'] [Algebra R A'] (h : IsSymmetricAlgebra f) {F G : A →ₐ[R] A'} (hFG : ↑F ∘ₗ f = ↑G ∘ₗ f) : F = G

theorem IsSymmetricAlgebra.lift_unique {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} (h : IsSymmetricAlgebra f) {A' : Type u_4} [CommSemiring A'] [Algebra R A'] {g : M →ₗ[R] A'} {F : A →ₐ[R] A'} (hF : ↑F ∘ₗ f = g) : F = h.lift g

theorem IsSymmetricAlgebra.induction {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} (h : IsSymmetricAlgebra f) {motive : A → Prop} (algebraMap : ∀ (r : R), motive ((algebraMap R A) r)) (ι : ∀ (x : M), motive (f x)) (mul : ∀ (a b : A), motive a → motive b → motive (a * b)) (add : ∀ (a b : A), motive a → motive b → motive (a + b)) (a : A) : motive a