English
The inclusion of a component j into the direct sum as a Lie module morphism is given by lieModuleOf j.
Русский
Включение компонента j в прямую сумму как морфизм модуля Ли задаётся через lieModuleOf j.
LaTeX
$$lieModuleOf R ι M j$$
Lean4
/-- The inclusion of each component into a direct sum as a morphism of Lie modules. -/
def lieModuleOf [DecidableEq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i :=
{ lof R ι M j with
map_lie' := fun {x m} => by
ext i
by_cases h : j = i
· rw [← h]; simp
· -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
-- old proof `simp [lof, lsingle, h]`
simp only [lof, lsingle, AddHom.toFun_eq_coe, lie_module_bracket_apply]
-- The coercion in the goal is `DFunLike.coe (β := fun x ↦ Π₀ (i : ι), M i)`
-- but the lemma is expecting `DFunLike.coe (β := fun x ↦ ⨁ (i : ι), M i)`
erw [AddHom.coe_mk]
simp [h] }
