equivFreeAlgebra — Mathlib

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)

Похожие утверждения