English
For any Lie submodule N, the submodule generated by the Lie brackets with the top ideal equals the join of the image of N under the endomorphism given by x and the brackets with I: ⟨(⊤, N)⟩ = (map of N by toEnd x) ⊔ ⟨I, N⟩.
Русский
Для произвольного подпредмета N справедливо: подмодуля, порожденный скобками с верхним идеалом, равен объединению образа N действием x и скобок с I и N.
LaTeX
$$$(\uparrow⁅(\top : \text{LieIdeal } R L), N⁆ : \text{Submodule } R M) = (N : \text{Submodule } R M).map (toEnd R L M x) \sqcup (\uparrow⁅I, N⁆ : \text{Submodule } R M)$$$
Lean4
theorem lie_top_eq_of_span_sup_eq_top (N : LieSubmodule R L M) :
(↑⁅(⊤ : LieIdeal R L), N⁆ : Submodule R M) = (N : Submodule R M).map (toEnd R L M x) ⊔ (↑⁅I, N⁆ : Submodule R M) :=
by
simp only [lieIdeal_oper_eq_linear_span', Submodule.sup_span, mem_top, true_and, Submodule.map_coe, toEnd_apply_apply]
refine le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)
· rintro z ⟨y, n, hn : n ∈ N, rfl⟩
obtain ⟨t, z, hz, rfl⟩ := exists_smul_add_of_span_sup_eq_top hxI y
simp only [SetLike.mem_coe, Submodule.span_union, Submodule.mem_sup]
exact
⟨t • ⁅x, n⁆, Submodule.subset_span ⟨t • n, N.smul_mem' t hn, lie_smul t x n⟩, ⁅z, n⁆,
Submodule.subset_span ⟨z, hz, n, hn, rfl⟩, by simp⟩
· rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)
exacts [⟨x, m, hm, rfl⟩, ⟨y, m, hm, rfl⟩]
