English
The span of h' over the distinguished base generates the Cartan subalgebra inside the Geck construction and, via a suitable map, spans the whole Cartan subalgebra in the ambient Lie algebra.
Русский
Обранная Картанова подалгебра порождается линейной оболочкой по h' и через соответствующее отображение охватывает всю Картанову подалгебру во внешней Ли-алгебре.
LaTeX
$$$\operatorname{span}_R(\operatorname{range}(h')) = \langle \text{top} \rangle$ in cartanSubalgebra'(b)$$
Lean4
@[simp]
theorem span_range_h'_eq_top [Fintype ι] [DecidableEq ι] :
span R (range h') = (⊤ : Submodule R (cartanSubalgebra' b)) :=
by
rw [eq_top_iff]
rintro ⟨⟨x, -⟩, hx : x ∈ span R (range h)⟩ -
let g : cartanSubalgebra' b →ₗ[R] Matrix (b.support ⊕ ι) (b.support ⊕ ι) R :=
(lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
suffices x ∈ (span R (range h')).map g by
rwa [← SetLike.mem_coe, ← (injective_subtype _).mem_set_image, ← (injective_subtype _).mem_set_image, ← image_comp]
rwa [map_span, ← range_comp]
