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)$.

source

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)

Instances For

source

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

Instances For

source

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

Equations

Instances For

source

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

Function.Surjective ⇑(algHom R M)

source

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.

Equations

Instances For

source

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

source

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

CommSemiring (SymmetricAlgebra R M)

Equations

source

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

CommRing (SymmetricAlgebra R M)

Equations

source

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.

Equations

Instances For

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

Instances For

source

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))

source

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

source

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

source

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

source

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.

source

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.

Equations

Instances For

source

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

IsSymmetricAlgebra (ι R M)

source

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.

Equations

Instances For

source

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

source

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

source

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

source

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

source

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

source

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)

source

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)

Equations

Instances For

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Symmetric Algebras #

Notation #

Note #