English
For a basis b with index κ and i ∈ κ, the equivFreeAlgebra b sends ι_R (b i) to FreeAlgebra.ι_R i.
Русский
Для базиса b с индексами κ и элемента i ∈ κ отображение equivFreeAlgebra b отправляет ι_R (b i) в FreeAlgebra.ι_R i.
LaTeX
$$$\\equivFreeAlgebra\\, b\\ (\\iota_R (b\\, i)) = \\mathrm{FreeAlgebra.ι}_R i$$$
Lean4
/-- A basis provides an algebra isomorphism with the free algebra, replacing each basis vector
with its index. -/
noncomputable def equivFreeAlgebra (b : Basis κ R M) : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ :=
AlgEquiv.ofAlgHom (TensorAlgebra.lift _ (Finsupp.linearCombination _ (FreeAlgebra.ι _) ∘ₗ b.repr.toLinearMap))
(FreeAlgebra.lift _ (ι R ∘ b)) (by ext; simp) (hom_ext <| b.ext fun i => by simp)