# A basis for TensorAlgebra R M#

## Main definitions #

• TensorAlgebra.equivMonoidAlgebra b : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ: the isomorphism given by a basis b : Basis κ R M.
• Basis.tensorAlgebra b : Basis (FreeMonoid κ) R (TensorAlgebra R M): the basis on the tensor algebra given by a basis b : Basis κ R M.

## Main results #

• TensorAlgebra.instFreeModule: the tensor algebra over M is free when M is
• TensorAlgebra.rank_eq
noncomputable def TensorAlgebra.equivFreeAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [] [] [Module R M] (b : Basis κ R M) :

A basis provides an algebra isomorphism with the free algebra, replacing each basis vector with its index.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TensorAlgebra.equivFreeAlgebra_ι_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [] [] [Module R M] (b : Basis κ R M) (i : κ) :
(() (b i)) =
@[simp]
theorem TensorAlgebra.equivFreeAlgebra_symm_ι {κ : Type uκ} {R : Type uR} {M : Type uM} [] [] [Module R M] (b : Basis κ R M) (i : κ) :
.symm () = () (b i)
@[simp]
theorem Basis.tensorAlgebra_repr_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [] [] [Module R M] (b : Basis κ R M) :
∀ (a : ), b.tensorAlgebra.repr a = .repr ()
noncomputable def Basis.tensorAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [] [] [Module R M] (b : Basis κ R M) :
Basis () R ()

A basis on M can be lifted to a basis on TensorAlgebra R M

Equations
• b.tensorAlgebra = .map .symm.toLinearEquiv
Instances For
instance TensorAlgebra.instModuleFree {R : Type uR} {M : Type uM} [] [] [Module R M] [] :

TensorAlgebra R M is free when M is.

Equations
• =
instance TensorAlgebra.instNoZeroDivisors {R : Type uR} {M : Type uM} [] [] [Module R M] [] [] :

The TensorAlgebra of a free module over a commutative semiring with no zero-divisors has no zero-divisors.

Equations
• =
instance TensorAlgebra.instIsDomain {R : Type uR} {M : Type uM} [] [] [Module R M] [] [] :

The TensorAlgebra of a free module over an integral domain is a domain.

Equations
• =
theorem TensorAlgebra.rank_eq {R : Type uR} {M : Type uM} [] [] [Module R M] [] [] :