equivFreeAlgebra_symm_ι — Mathlib

English

Let b be a basis of M indexed by κ. The inverse of the canonical isomorphism between the free algebra on M and the tensor algebra identifies the i-th free-algebra generator with the i-th basis vector in M under the tensor algebra embedding.

Русский

Пусть b является базисом M, индексируемым κ. Обратная к каноническому изоморфизму между свободной алгеброй на M и тензорной алгеброй переводит генератор с индексом i во второй алгебре в элемент ι_R(b(i)) тензорной алгебры.

LaTeX

$$$ (\text{equivFreeAlgebra } b).symm (FreeAlgebra.\iota R i) = ι R (b i) $$$

Lean4

@[simp]
theorem equivFreeAlgebra_symm_ι (b : Basis κ R M) (i : κ) : (equivFreeAlgebra b).symm (FreeAlgebra.ι R i) = ι R (b i) :=
  (equivFreeAlgebra b).toEquiv.symm_apply_eq.mpr <| equivFreeAlgebra_ι_apply b i |>.symm

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