lieModuleComponent — Mathlib

English

The projection onto component j is a Lie module homomorphism.

Русский

Проекция на компонент j является гомоморфизмом модуля Ли.

LaTeX

$$lieModuleComponent (j) : (⨁ i, M i) →ₗ⁅R,L⁆ M_j$$

Lean4

/-- The projection map onto one component, as a morphism of Lie modules. -/
def lieModuleComponent (j : ι) : (⨁ i, M i) →ₗ⁅R,L⁆ M j :=
  { component R ι M j with map_lie' := fun {x m} => by simp [component, lapply] }

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