Documentation

Mathlib.LinearAlgebra.TensorAlgebra.Basis

A basis for TensorAlgebra R M #

Main definitions #

Main results #

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

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

Instances For
    @[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 : κ) :
    @[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 : κ) :
    @[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) :
    noncomputable def Basis.tensorAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) :

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

    Instances For

      TensorAlgebra R M is free when M is.