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} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ

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.

@[simp]

theorem TensorAlgebra.equivFreeAlgebra_ι_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (i : κ) : (TensorAlgebra.equivFreeAlgebra b) ((TensorAlgebra.ι R) (b i)) = FreeAlgebra.ι R i

@[simp]

theorem TensorAlgebra.equivFreeAlgebra_symm_ι {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (i : κ) : (AlgEquiv.symm (TensorAlgebra.equivFreeAlgebra b)) (FreeAlgebra.ι R i) = (TensorAlgebra.ι R) (b i)

@[simp]

theorem Basis.tensorAlgebra_repr_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : ∀ (a : TensorAlgebra R M), (Basis.tensorAlgebra b).repr a = (FreeAlgebra.basisFreeMonoid R κ).repr ((TensorAlgebra.equivFreeAlgebra b) a)

noncomputable def Basis.tensorAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : Basis (FreeMonoid κ) R (TensorAlgebra R M)

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

Equations

• Basis.tensorAlgebra b = Basis.map (FreeAlgebra.basisFreeMonoid R κ) (AlgEquiv.toLinearEquiv (AlgEquiv.symm (TensorAlgebra.equivFreeAlgebra b)))

instance TensorAlgebra.instModuleFree {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : Module.Free R (TensorAlgebra R M)

TensorAlgebra R M is free when M is.

Equations

• (_ : Module.Free R (TensorAlgebra R M)) = (_ : Module.Free R (TensorAlgebra R M))

instance TensorAlgebra.instNoZeroDivisors {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] [Module.Free R M] : NoZeroDivisors (TensorAlgebra R M)

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

Equations

• (_ : NoZeroDivisors (TensorAlgebra R M)) = (_ : NoZeroDivisors (TensorAlgebra R M))

instance TensorAlgebra.instIsDomain {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.Free R M] : IsDomain (TensorAlgebra R M)

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

Equations

• (_ : IsDomain (TensorAlgebra R M)) = (_ : IsDomain (TensorAlgebra R M))

theorem TensorAlgebra.rank_eq {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial R] [Module.Free R M] : Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun (n : ℕ) => Module.rank R M ^ n)