Tensor Algebras

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

Notation

tensor_algebra R M is the tensor algebra itself. It is endowed with an R-algebra structure.
tensor_algebra.ι R is the canonical R-linear map M → tensor_algebra R M.
Given a linear map f : M → A to an R-algebra A, lift R f is the lift of f to an R-algebra morphism tensor_algebra R M → A.

Theorems

ι_comp_lift states that the composition (lift R f) ∘ (ι R) is identical to f.
lift_unique states that whenever an R-algebra morphism g : tensor_algebra R M → A is given whose composition with ι R is f, then one has g = lift R f.
hom_ext is a variant of lift_unique in the form of an extensionality theorem.
lift_comp_ι is a combination of ι_comp_lift and lift_unique. It states that the lift of the composition of an algebra morphism with ι is the algebra morphism itself.

Implementation details

As noted above, the tensor algebra of M is constructed as the free R-algebra generated by M, modulo the additional relations making the inclusion of M into an R-linear map.

source

inductive tensor_algebra.rel (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] (a a_1 : free_algebra R M) :

Prop

add : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_monoid M] [_inst_3 : semimodule R M] {a b : M}, tensor_algebra.rel R M (free_algebra.ι R (a + b)) (free_algebra.ι R a + free_algebra.ι R b)
smul : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_monoid M] [_inst_3 : semimodule R M] {r : R} {a : M}, tensor_algebra.rel R M (free_algebra.ι R (r • a)) ((⇑(algebra_map R (free_algebra R M)) r) * free_algebra.ι R a)

An inductively defined relation on pre R M used to force the initial algebra structure on the associated quotient.

source

@[instance]

def tensor_algebra.inhabited (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

inhabited (tensor_algebra R M)

source

def tensor_algebra (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

Type (max u_1 u_2)

The tensor algebra of the module M over the commutative semiring R.

Equations

tensor_algebra R M = ring_quot (tensor_algebra.rel R M)

source

@[instance]

def tensor_algebra.semiring (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

semiring (tensor_algebra R M)

source

@[instance]

def tensor_algebra.inst (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

algebra R (tensor_algebra R M)

source

def tensor_algebra.ι (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] :

M →ₗ[R] tensor_algebra R M

The canonical linear map M →ₗ[R] tensor_algebra R M.

Equations

tensor_algebra.ι R = {to_fun := λ (m : M), ⇑(ring_quot.mk_alg_hom R (tensor_algebra.rel R M)) (free_algebra.ι R m), map_add' := _, map_smul' := _}

source

theorem tensor_algebra.ring_quot_mk_alg_hom_free_algebra_ι_eq_ι (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] (m : M) :

⇑(ring_quot.mk_alg_hom R (tensor_algebra.rel R M)) (free_algebra.ι R m) = ⇑(tensor_algebra.ι R) m

source

def tensor_algebra.lift (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) :

tensor_algebra R M →ₐ[R] A

Given a linear map f : M → A where A is an R-algebra, lift R f is the unique lift of f to a morphism of R-algebras tensor_algebra R M → A.

Equations

tensor_algebra.lift R f = ring_quot.lift_alg_hom R (free_algebra.lift R ⇑f) _

source

@[simp]

theorem tensor_algebra.ι_comp_lift {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) :

(tensor_algebra.lift R f).to_linear_map.comp (tensor_algebra.ι R) = f

source

@[simp]

theorem tensor_algebra.lift_ι_apply {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (x : M) :

⇑(tensor_algebra.lift R f) (⇑(tensor_algebra.ι R) x) = ⇑f x

source

@[simp]

theorem tensor_algebra.lift_unique {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (g : tensor_algebra R M →ₐ[R] A) :

g.to_linear_map.comp (tensor_algebra.ι R) = f ↔ g = tensor_algebra.lift R f

source

@[simp]

theorem tensor_algebra.lift_comp_ι {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (g : tensor_algebra R M →ₐ[R] A) :

tensor_algebra.lift R (g.to_linear_map.comp (tensor_algebra.ι R)) = g

source

@[ext]

theorem tensor_algebra.hom_ext {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] {f g : tensor_algebra R M →ₐ[R] A} (w : f.to_linear_map.comp (tensor_algebra.ι R) = g.to_linear_map.comp (tensor_algebra.ι R)) :

f = g