lift_symm_apply — Mathlib

English

For any algebra hom F from the universal enveloping algebra to A, the symmetric lift map sends F to the composition F ∘ ι.

Русский

Для любого гомома A, поднимаемого через универсальную окружную алгебру, симметричное отображение lift_send отправляет F на композицию F ∘ ι.

LaTeX

$$lift_symm_apply : (lift R).symm F = (F : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)$$

Lean4

@[simp]
theorem lift_symm_apply (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) :
    (lift R).symm F = (F : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R) :=
  rfl

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