ι_comp_lift

Mathlib.Algebra.Lie.UniversalEnveloping

URI: https://scilib.ai/kg/mathlib#UniversalEnvelopingAlgebra.ι_comp_lift

English

The composition of the lift with the iota map recovers the original Lie algebra homomorphism f.

Русский

Сочетание lift и отображения iota восстанавливает исходный гомоморфизм Ли f.

LaTeX

$$ι_comp_lift : lift R f ∘ ι R = f$$

Lean4

@[simp]
theorem ι_comp_lift : lift R f ∘ ι R = f :=
  funext <| LieHom.ext_iff.mp <| (lift R).symm_apply_apply f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru