lieAlgebraComponent

Mathlib.Algebra.Lie.DirectSum

URI: https://scilib.ai/kg/mathlib#DirectSum.lieAlgebraComponent

Lean4

/-- The projection map onto one component, as a morphism of Lie algebras. -/
@[simps]
def lieAlgebraComponent (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j :=
  { component R ι L j with
    toFun := component R ι L j
    map_lie' := fun {x y} => by simp [component, lapply] }
    -- Note(kmill): `ext` cannot generate an iff theorem here since `x` and `y` do not determine `R`.

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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