# Documentation

Mathlib.LinearAlgebra.TensorAlgebra.Basic

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

1. TensorAlgebra R M is the tensor algebra itself. It is endowed with an R-algebra structure.
2. TensorAlgebra.ι R is the canonical R-linear map M → TensorAlgebra 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 TensorAlgebra 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 : TensorAlgebra 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 TensorAlgebra.Rel (R : Type u_1) [] (M : Type u_2) [] [Module R M] :
Prop

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

Instances For
def TensorAlgebra (R : Type u_1) [] (M : Type u_2) [] [Module R M] :
Type (max u_1 u_2)

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

Instances For
instance instInhabitedTensorAlgebra (R : Type u_1) [] (M : Type u_2) [] [Module R M] :
instance instSemiringTensorAlgebra (R : Type u_1) [] (M : Type u_2) [] [Module R M] :
instance instAlgebra {R : Type u_3} {A : Type u_4} {M : Type u_5} [] [] [] [Algebra R A] [Module R M] [Module A M] [] :
Algebra R ()
instance instSMulCommClassTensorAlgebraToSMulInstSemiringTensorAlgebraInstAlgebraToSMulInstAlgebra {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [] [] [] [] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] [] [] [] :
instance instIsScalarTowerTensorAlgebraToSMulInstSemiringTensorAlgebraInstAlgebraToSMulInstAlgebra {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [] [] [] [] [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] [] [] [] :
instance TensorAlgebra.instRingTensorAlgebraToCommSemiring (M : Type u_2) [] {S : Type u_3} [] [Module S M] :
Ring ()
theorem TensorAlgebra.ι_def (R : Type u_3) [] {M : Type u_4} [] [Module R M] :
= { toAddHom := { toFun := fun m => ↑() (), map_add' := (_ : ∀ (x y : M), (fun m => ↑() ()) (x + y) = (fun m => ↑() ()) x + (fun m => ↑() ()) y) }, map_smul' := (_ : ∀ (r : R) (x : M), AddHom.toFun { toFun := fun m => ↑() (), map_add' := (_ : ∀ (x y : M), (fun m => ↑() ()) (x + y) = (fun m => ↑() ()) x + (fun m => ↑() ()) y) } (r x) = ↑() r AddHom.toFun { toFun := fun m => ↑() (), map_add' := (_ : ∀ (x y : M), (fun m => ↑() ()) (x + y) = (fun m => ↑() ()) x + (fun m => ↑() ()) y) } x) }
@[irreducible]
def TensorAlgebra.ι (R : Type u_3) [] {M : Type u_4} [] [Module R M] :

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

Instances For
theorem TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι (R : Type u_1) [] {M : Type u_2} [] [Module R M] (m : M) :
↑() () = ↑() m
@[simp]
theorem TensorAlgebra.lift_symm_apply (R : Type u_1) [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] (F : →ₐ[R] A) :
().symm F =
def TensorAlgebra.lift (R : Type u_1) [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] :
(M →ₗ[R] A) ( →ₐ[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 TensorAlgebra R M → A.

Instances For
@[simp]
theorem TensorAlgebra.ι_comp_lift {R : Type u_1} [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) :
@[simp]
theorem TensorAlgebra.lift_ι_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) (x : M) :
↑(↑() f) (↑() x) = f x
@[simp]
theorem TensorAlgebra.lift_unique {R : Type u_1} [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) (g : →ₐ[R] A) :
g = ↑() f
@[simp]
theorem TensorAlgebra.lift_comp_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] (g : →ₐ[R] A) :
↑() () = g
theorem TensorAlgebra.hom_ext {R : Type u_1} [] {M : Type u_2} [] [Module R M] {A : Type u_3} [] [Algebra R A] {f : →ₐ[R] A} {g : →ₐ[R] A} (w : ) :
f = g

See note [partially-applied ext lemmas].

theorem TensorAlgebra.induction {R : Type u_1} [] {M : Type u_2} [] [Module R M] {C : Prop} (h_grade0 : (r : R) → C (↑(algebraMap R ()) r)) (h_grade1 : (x : M) → C (↑() x)) (h_mul : (a b : ) → C aC bC (a * b)) (h_add : (a b : ) → C aC bC (a + b)) (a : ) :
C a

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

def TensorAlgebra.algebraMapInv {R : Type u_1} [] {M : Type u_2} [] [Module R M] :

The left-inverse of algebraMap.

Instances For
theorem TensorAlgebra.algebraMap_leftInverse {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
Function.LeftInverse TensorAlgebra.algebraMapInv ↑(algebraMap R ())
@[simp]
theorem TensorAlgebra.algebraMap_inj {R : Type u_1} [] (M : Type u_2) [] [Module R M] (x : R) (y : R) :
↑(algebraMap R ()) x = ↑(algebraMap R ()) y x = y
@[simp]
theorem TensorAlgebra.algebraMap_eq_zero_iff {R : Type u_1} [] (M : Type u_2) [] [Module R M] (x : R) :
↑(algebraMap R ()) x = 0 x = 0
@[simp]
theorem TensorAlgebra.algebraMap_eq_one_iff {R : Type u_1} [] (M : Type u_2) [] [Module R M] (x : R) :
↑(algebraMap R ()) x = 1 x = 1
def TensorAlgebra.toTrivSqZeroExt {R : Type u_1} [] {M : Type u_2} [] [Module R M] [] [] :

The canonical map from TensorAlgebra R M into TrivSqZeroExt R M that sends TensorAlgebra.ι to TrivSqZeroExt.inr.

Instances For
@[simp]
theorem TensorAlgebra.toTrivSqZeroExt_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] (x : M) [] [] :
TensorAlgebra.toTrivSqZeroExt (↑() x) =
def TensorAlgebra.ιInv {R : Type u_1} [] {M : Type u_2} [] [Module R M] :

The left-inverse of ι.

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

Instances For
theorem TensorAlgebra.ι_leftInverse {R : Type u_1} [] {M : Type u_2} [] [Module R M] :
Function.LeftInverse TensorAlgebra.ιInv ↑()
@[simp]
theorem TensorAlgebra.ι_inj (R : Type u_1) [] {M : Type u_2} [] [Module R M] (x : M) (y : M) :
↑() x = ↑() y x = y
@[simp]
theorem TensorAlgebra.ι_eq_zero_iff (R : Type u_1) [] {M : Type u_2} [] [Module R M] (x : M) :
↑() x = 0 x = 0
@[simp]
theorem TensorAlgebra.ι_eq_algebraMap_iff {R : Type u_1} [] {M : Type u_2} [] [Module R M] (x : M) (r : R) :
↑() x = ↑(algebraMap R ()) r x = 0 r = 0
@[simp]
theorem TensorAlgebra.ι_ne_one {R : Type u_1} [] {M : Type u_2} [] [Module R M] [] (x : M) :
↑() x 1
theorem TensorAlgebra.ι_range_disjoint_one {R : Type u_1} [] {M : Type u_2} [] [Module R M] :

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

def TensorAlgebra.tprod (R : Type u_1) [] (M : Type u_2) [] [Module R M] (n : ) :
MultilinearMap R (fun x => M) ()

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

See also PiTensorProduct.tprod.

Instances For
@[simp]
theorem TensorAlgebra.tprod_apply (R : Type u_1) [] (M : Type u_2) [] [Module R M] {n : } (x : Fin nM) :
↑() x = List.prod (List.ofFn fun i => ↑() (x i))
def FreeAlgebra.toTensor {R : Type u_1} [] {M : Type u_2} [] [Module R M] :

The canonical image of the FreeAlgebra in the TensorAlgebra, which maps FreeAlgebra.ι R x to TensorAlgebra.ι R x.

Instances For
@[simp]
theorem FreeAlgebra.toTensor_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] (m : M) :
FreeAlgebra.toTensor () = ↑() m