English
Within the Geck construction, the Cartan subalgebra is a distinguished abelian Lie subalgebra of the matrix Lie algebra, and it is generated by the family h_i corresponding to the simple roots indexed by i in b.support.
Русский
В конструкции Geck Картанова подалгебра — це выделенная абелева подалгебра Ли внутри матричной алгебры, порождённая семейством h_i, соответствующим простым корням индексов i в b.support.
LaTeX
$$$\text{cartanSubalgebra}(b) \subseteq \operatorname{lieAlgebra}(b)$ and is generated by $\{h_i : i \in b.support\}$$$
Lean4
/-- A distinguished subalgebra corresponding to a Cartan subalgebra of the Geck construction.
See also `RootPairing.GeckConstruction.cartanSubalgebra'`. -/
def cartanSubalgebra [Fintype ι] [DecidableEq ι] : LieSubalgebra R (Matrix (b.support ⊕ ι) (b.support ⊕ ι) R)
where
__ := Submodule.span R (range h)
lie_mem' {x y} hx
hy :=
by
have aux : (∀ u ∈ range (h (b := b)), ∀ v ∈ range (h (b := b)), ⁅u, v⁆ = 0) := by rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩;
exact lie_h_h i j
simp only [Submodule.carrier_eq_coe, SetLike.mem_coe, LieSubalgebra.mem_toSubmodule,
← LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero (R := R) aux] at hx hy ⊢
exact LieSubalgebra.lie_mem _ hx hy
