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 Mis the tensor algebra itself. It is endowed with an R-algebra structure.tensor_algebra.ι R Mis the canonical R-linear mapM → tensor_algebra R M.- Given a linear map
f : M → Ato an R-algebraA,lift R M fis the lift offto anR-algebra morphismtensor_algebra R M → A.
Theorems
ι_comp_liftstates that the composition(lift R M f) ∘ (ι R M)is identical tof.lift_uniquestates that whenever an R-algebra morphismg : tensor_algebra R M → Ais given whose composition withι R Misf, then one hasg = lift R M f.hom_extis a variant oflift_uniquein the form of an extensionality theorem.lift_comp_ιis a combination ofι_comp_liftandlift_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.
This is done as a quotient of an inductive type by an inductively defined relation.
Explicltly, the construction involves three steps:
- We construct an inductive type
tensor_algebra.pre R M, the terms of which should be thought of as representatives for the elements oftensor_algebra R M. It is the free type with maps fromRandM, and with two binary operationsaddandmul. - We construct an inductive relation
tensor_algebra.rel R Montensor_algebra.pre R M. This is the smallest relation for which the quotient is anR-algebra where addition resp. multiplication are induced byaddresp.mulfrom 1, and for which the map fromRis the structure map for the algebra while the map fromMisR-linear. - The tensor algebra
tensor_algebra R Mis the quotient oftensor_algebra.pre R Mby the relationtensor_algebra.rel R M.
inductive
tensor_algebra.pre
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
Type (max u_1 u_2)
- of : Π (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M], M → tensor_algebra.pre R M
- of_scalar : Π (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M], R → tensor_algebra.pre R M
- add : Π (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M], tensor_algebra.pre R M → tensor_algebra.pre R M → tensor_algebra.pre R M
- mul : Π (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M], tensor_algebra.pre R M → tensor_algebra.pre R M → tensor_algebra.pre R M
This inductive type is used to express representatives of the tensor algebra.
@[instance]
def
tensor_algebra.pre.inhabited
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
inhabited (tensor_algebra.pre R M)
Equations
def
tensor_algebra.pre.has_coe_module
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_coe M (tensor_algebra.pre R M)
Coercion from M to pre R M. Note: Used for notation only.
Equations
- tensor_algebra.pre.has_coe_module R M = {coe := tensor_algebra.pre.of _inst_3}
def
tensor_algebra.pre.has_coe_semiring
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_coe R (tensor_algebra.pre R M)
Coercion from R to pre R M. Note: Used for notation only.
Equations
- tensor_algebra.pre.has_coe_semiring R M = {coe := tensor_algebra.pre.of_scalar _inst_3}
def
tensor_algebra.pre.has_mul
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_mul (tensor_algebra.pre R M)
Multiplication in pre R M defined as pre.mul. Note: Used for notation only.
Equations
- tensor_algebra.pre.has_mul R M = {mul := tensor_algebra.pre.mul _inst_3}
def
tensor_algebra.pre.has_add
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_add (tensor_algebra.pre R M)
Addition in pre R M defined as pre.add. Note: Used for notation only.
Equations
- tensor_algebra.pre.has_add R M = {add := tensor_algebra.pre.add _inst_3}
def
tensor_algebra.pre.has_zero
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_zero (tensor_algebra.pre R M)
Zero in pre R M defined as the image of 0 from R. Note: Used for notation only.
Equations
def
tensor_algebra.pre.has_one
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_one (tensor_algebra.pre R M)
One in pre R M defined as the image of 1 from R. Note: Used for notation only.
Equations
def
tensor_algebra.pre.has_scalar
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_scalar R (tensor_algebra.pre R M)
Scalar multiplication defined as multiplication by the image of elements from R.
Note: Used for notation only.
Equations
- tensor_algebra.pre.has_scalar R M = {smul := λ (r : R) (m : tensor_algebra.pre R M), (tensor_algebra.pre.of_scalar r).mul m}
def
tensor_algebra.lift_fun
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M]
{A : Type u_3}
[semiring A]
[algebra R A] :
(M →ₗ[R] A) → tensor_algebra.pre R M → A
Given a linear map from M to an R-algebra A, lift_fun provides a lift of f to a function
from pre R M to A. This is mainly used in the construction of tensor_algebra.lift.
Equations
- tensor_algebra.lift_fun R M f = λ (t : tensor_algebra.pre R M), t.rec_on ⇑f ⇑(algebra_map R A) (λ (_x _x : tensor_algebra.pre R M), has_add.add) (λ (_x _x : tensor_algebra.pre R M), has_mul.mul)
inductive
tensor_algebra.rel
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
tensor_algebra.pre R M → tensor_algebra.pre R M → Prop
- add_lin : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b : M}, tensor_algebra.rel R M ↑(a + b) (↑a + ↑b)
- smul_lin : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {r : R} {a : M}, tensor_algebra.rel R M ↑(r • a) (↑r * ↑a)
- add_scalar : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {r s : R}, tensor_algebra.rel R M ↑(r + s) (↑r + ↑s)
- mul_scalar : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {r s : R}, tensor_algebra.rel R M ↑(r * s) (↑r * ↑s)
- central_scalar : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {r : R} {a : tensor_algebra.pre R M}, tensor_algebra.rel R M (↑r * a) (a * ↑r)
- add_assoc : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M (a + b + c) (a + (b + c))
- add_comm : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b : tensor_algebra.pre R M}, tensor_algebra.rel R M (a + b) (b + a)
- zero_add : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a : tensor_algebra.pre R M}, tensor_algebra.rel R M (0 + a) a
- mul_assoc : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M (a * b * c) (a * (b * c))
- one_mul : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a : tensor_algebra.pre R M}, tensor_algebra.rel R M (1 * a) a
- mul_one : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a : tensor_algebra.pre R M}, tensor_algebra.rel R M (a * 1) a
- left_distrib : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M (a * (b + c)) (a * b + a * c)
- right_distrib : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M ((a + b) * c) (a * c + b * c)
- zero_mul : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a : tensor_algebra.pre R M}, tensor_algebra.rel R M (0 * a) 0
- mul_zero : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a : tensor_algebra.pre R M}, tensor_algebra.rel R M (a * 0) 0
- add_compat_left : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M a b → tensor_algebra.rel R M (a + c) (b + c)
- add_compat_right : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M a b → tensor_algebra.rel R M (c + a) (c + b)
- mul_compat_left : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M a b → tensor_algebra.rel R M (a * c) (b * c)
- mul_compat_right : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M] {a b c : tensor_algebra.pre R M}, tensor_algebra.rel R M a b → tensor_algebra.rel R M (c * a) (c * b)
An inductively defined relation on pre R M used to force the initial algebra structure on
the associated quotient.
def
tensor_algebra
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group 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 = quot (tensor_algebra.rel R M)
@[instance]
def
tensor_algebra.semiring
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
semiring (tensor_algebra R M)
Equations
- tensor_algebra.semiring R M = {add := quot.map₂ has_add.add _ _, add_assoc := _, zero := quot.mk (tensor_algebra.rel R M) 0, zero_add := _, add_zero := _, add_comm := _, mul := quot.map₂ has_mul.mul _ _, mul_assoc := _, one := quot.mk (tensor_algebra.rel R M) 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[instance]
def
tensor_algebra.inhabited
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
inhabited (tensor_algebra R M)
Equations
- tensor_algebra.inhabited R M = {default := 0}
@[instance]
def
tensor_algebra.has_scalar
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
has_scalar R (tensor_algebra R M)
Equations
- tensor_algebra.has_scalar R M = {smul := λ (r : R) (a : tensor_algebra R M), quot.lift_on a (λ (x : tensor_algebra.pre R M), quot.mk (tensor_algebra.rel R M) (↑r * x)) _}
@[instance]
def
tensor_algebra.algebra
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
algebra R (tensor_algebra R M)
Equations
- tensor_algebra.algebra R M = {to_has_scalar := tensor_algebra.has_scalar R M _inst_3, to_ring_hom := {to_fun := λ (r : R), quot.mk (tensor_algebra.rel R M) ↑r, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
def
tensor_algebra.ι
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M] :
M →ₗ[R] tensor_algebra R M
The canonical linear map M →ₗ[R] tensor_algebra R M.
Equations
- tensor_algebra.ι R M = {to_fun := λ (m : M), quot.mk (tensor_algebra.rel R M) ↑m, map_add' := _, map_smul' := _}
def
tensor_algebra.lift
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_group M]
[semimodule R M]
{A : Type u_3}
[semiring A]
[algebra R A] :
(M →ₗ[R] A) → (tensor_algebra R M →ₐ[R] A)
Given a linear map f : M → A where A is an R-algebra, lift R M f is the unique lift
of f to a morphism of R-algebras tensor_algebra R M → A.
Equations
- tensor_algebra.lift R M f = {to_fun := λ (a : tensor_algebra R M), quot.lift_on a (tensor_algebra.lift_fun R M f) _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[simp]
theorem
tensor_algebra.ι_comp_lift
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_group M]
[semimodule R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A) :
(tensor_algebra.lift R M f).to_linear_map.comp (tensor_algebra.ι R M) = f
@[simp]
theorem
tensor_algebra.lift_unique
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_group 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 M) = f ↔ g = tensor_algebra.lift R M f
@[simp]
theorem
tensor_algebra.lift_comp_ι
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_group M]
[semimodule R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(g : tensor_algebra R M →ₐ[R] A) :
tensor_algebra.lift R M (g.to_linear_map.comp (tensor_algebra.ι R M)) = g
theorem
tensor_algebra.hom_ext
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_group M]
[semimodule R M]
{A : Type u_3}
[semiring A]
[algebra R A]
{f g : tensor_algebra R M →ₐ[R] A} :
f.to_linear_map.comp (tensor_algebra.ι R M) = g.to_linear_map.comp (tensor_algebra.ι R M) → f = g