lift_ι — Mathlib

English

The lift of the canonical inclusion ι is the identity on the symmetric algebra.

Русский

Образ продукции lift от канонического включения ι является тождественным отображением на симметрическую алгебру.

LaTeX

$$lift (ι R M) = .id R (SymmetricAlgebra R M)$$

Lean4

@[simp]
theorem lift_ι : lift (ι R M) = .id R (SymmetricAlgebra R M) :=
  by
  apply algHom_ext
  rw [lift_comp_ι]
  ext
  simp

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