equivFreeAlgebra_ι_apply — Mathlib

English

Given a basis b of M, the tensor algebra is algebra-isomorphic to the free algebra on κ, realized by the canonical equivalence equivFreeAlgebra b.

Русский

Дана база b для M, тензорная алгебра изоморфна свободной алгебре на κ через каноническое эквивалентное отображение equivFreeAlgebra b.

LaTeX

$$$\\text{equivFreeAlgebra}\\, b: \\mathrm{TensorAlgebra}_R M \\cong_R \\mathrm{FreeAlgebra}_R \\kappa$$$

Lean4

@[simp]
theorem equivFreeAlgebra_ι_apply (b : Basis κ R M) (i : κ) : equivFreeAlgebra b (ι R (b i)) = FreeAlgebra.ι R i :=
  (TensorAlgebra.lift_ι_apply _ _).trans <| by simp

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