lift_comp_ι — Mathlib

English

For any linear map f: M → A, lift f provides an R-algebra homomorphism from SymmetricAlgebra R M to A, and this correspondence is an equivalence between linear maps and algebra homomorphisms.

Русский

Для любого линейного отображения f: M → A функция lift f обеспечивает R-алгебра-гомоморфизм из SymmetricAlgebra R M в A; существует эквивалентность между линейными отображениями M → A и алгебра-гомоморфизмами SymmetricAlgebra R M → A.

LaTeX

$$lift : (M →ₗ[R] A) ≃ (SymmetricAlgebra R M →ₐ[R] A)$$

Lean4

@[simp]
theorem lift_comp_ι : lift f ∘ₗ ι R M = f :=
  LinearMap.ext <| lift_ι_apply f

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