# mathlib3documentation

linear_algebra.tensor_algebra.basic

# Tensor Algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

1. tensor_algebra R M is the tensor algebra itself. It is endowed with an R-algebra structure.
2. tensor_algebra.ι R is the canonical R-linear map M → tensor_algebra R M.
3. 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 #

1. ι_comp_lift states that the composition (lift R f) ∘ (ι R) is identical to f.
2. 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.
3. hom_ext is a variant of lift_unique in the form of an extensionality theorem.
4. 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.

inductive tensor_algebra.rel (R : Type u_1) (M : Type u_2) [ M] :
M M Prop
• add : {R : Type u_1} [_inst_1 : {M : Type u_2} [_inst_2 : [_inst_3 : M] {a b : M}, (a + b)) a + b)
• smul : {R : Type u_1} [_inst_1 : {M : Type u_2} [_inst_2 : [_inst_3 : M] {r : R} {a : M}, (r a)) ( M)) r * a)

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

@[protected, instance]
def tensor_algebra.inhabited (R : Type u_1) (M : Type u_2) [ M] :
def tensor_algebra (R : Type u_1) (M : Type u_2) [ M] :
Type (max u_1 u_2)

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

Equations
Instances for tensor_algebra
@[protected, instance]
def tensor_algebra.semiring (R : Type u_1) (M : Type u_2) [ M] :
@[protected, instance]
def tensor_algebra.algebra (R : Type u_1) (M : Type u_2) [ M] :
M)
@[protected, instance]
def tensor_algebra.ring (M : Type u_2) {S : Type u_1} [comm_ring S] [ M] :
ring M)
Equations
@[irreducible]
def tensor_algebra.ι (R : Type u_1) {M : Type u_2} [ M] :

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

Equations
theorem tensor_algebra.ring_quot_mk_alg_hom_free_algebra_ι_eq_ι (R : Type u_1) {M : Type u_2} [ M] (m : M) :
M)) m) = m
@[simp]
theorem tensor_algebra.lift_symm_apply (R : Type u_1) {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] (F : →ₐ[R] A) :
.symm) F =
@[irreducible]
def tensor_algebra.lift (R : Type u_1) {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] :
(M →ₗ[R] A) 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
@[simp]
theorem tensor_algebra.ι_comp_lift {R : Type u_1} {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] (f : M →ₗ[R] A) :
@[simp]
theorem tensor_algebra.lift_ι_apply {R : Type u_1} {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] (f : M →ₗ[R] A) (x : M) :
( f) ( x) = f x
@[simp]
theorem tensor_algebra.lift_unique {R : Type u_1} {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] (f : M →ₗ[R] A) (g : →ₐ[R] A) :
= f g = f
@[simp]
theorem tensor_algebra.lift_comp_ι {R : Type u_1} {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] (g : →ₐ[R] A) :
@[ext]
theorem tensor_algebra.hom_ext {R : Type u_1} {M : Type u_2} [ M] {A : Type u_3} [semiring A] [ A] {f g : →ₐ[R] A} (w : = ) :
f = g
theorem tensor_algebra.induction {R : Type u_1} {M : Type u_2} [ M] {C : Prop} (h_grade0 : (r : R), C ( M)) r)) (h_grade1 : (x : M), C ( x)) (h_mul : (a b : M), C a C b C (a * b)) (h_add : (a b : M), C a C b C (a + b)) (a : M) :
C a

If C holds for the algebra_map of r : R into tensor_algebra R M, the ι of x : M, and is preserved under addition and muliplication, then it holds for all of tensor_algebra R M.

def tensor_algebra.algebra_map_inv {R : Type u_1} {M : Type u_2} [ M] :

The left-inverse of algebra_map.

Equations
theorem tensor_algebra.algebra_map_left_inverse {R : Type u_1} (M : Type u_2) [ M] :
@[simp]
theorem tensor_algebra.algebra_map_inj {R : Type u_1} (M : Type u_2) [ M] (x y : R) :
M)) x = M)) y x = y
@[simp]
theorem tensor_algebra.algebra_map_eq_zero_iff {R : Type u_1} (M : Type u_2) [ M] (x : R) :
M)) x = 0 x = 0
@[simp]
theorem tensor_algebra.algebra_map_eq_one_iff {R : Type u_1} (M : Type u_2) [ M] (x : R) :
M)) x = 1 x = 1
def tensor_algebra.to_triv_sq_zero_ext {R : Type u_1} {M : Type u_2} [ M] [ M] [ M] :

The canonical map from tensor_algebra R M into triv_sq_zero_ext R M that sends tensor_algebra.ι to triv_sq_zero_ext.inr.

Equations
@[simp]
theorem tensor_algebra.to_triv_sq_zero_ext_ι {R : Type u_1} {M : Type u_2} [ M] (x : M) [ M] [ M] :
def tensor_algebra.ι_inv {R : Type u_1} {M : Type u_2} [ M] :

The left-inverse of ι.

As an implementation detail, we implement this using triv_sq_zero_ext which has a suitable algebra structure.

Equations
theorem tensor_algebra.ι_left_inverse {R : Type u_1} {M : Type u_2} [ M] :
@[simp]
theorem tensor_algebra.ι_inj (R : Type u_1) {M : Type u_2} [ M] (x y : M) :
x = y x = y
@[simp]
theorem tensor_algebra.ι_eq_zero_iff (R : Type u_1) {M : Type u_2} [ M] (x : M) :
x = 0 x = 0
@[simp]
theorem tensor_algebra.ι_eq_algebra_map_iff {R : Type u_1} {M : Type u_2} [ M] (x : M) (r : R) :
x = M)) r x = 0 r = 0
@[simp]
theorem tensor_algebra.ι_ne_one {R : Type u_1} {M : Type u_2} [ M] [nontrivial R] (x : M) :
x 1
theorem tensor_algebra.ι_range_disjoint_one {R : Type u_1} {M : Type u_2} [ M] :

The generators of the tensor algebra are disjoint from its scalars.

def tensor_algebra.tprod (R : Type u_1) (M : Type u_2) [ M] (n : ) :
(λ (i : fin n), M) M)

Construct a product of n elements of the module within the tensor algebra.

See also pi_tensor_product.tprod.

Equations
• n = (λ (_x : fin n),
@[simp]
theorem tensor_algebra.tprod_apply (R : Type u_1) (M : Type u_2) [ M] {n : } (x : fin n M) :
n) x = (list.of_fn (λ (i : fin n), (x i))).prod
def free_algebra.to_tensor {R : Type u_1} {M : Type u_2} [ M] :

The canonical image of the free_algebra in the tensor_algebra, which maps free_algebra.ι R x to tensor_algebra.ι R x.

Equations
@[simp]
theorem free_algebra.to_tensor_ι {R : Type u_1} {M : Type u_2} [ M] (m : M) :