English
The root system associated to a finite-dimensional Lie algebra with nondegenerate Killing form over a characteristic-zero field, relative to a splitting Cartan subalgebra, is built from the weight spaces of L relative to H with coroots defined via α, and reflections generated by reflectRoot.
Русский
Корневая система, связанная с конечномерной алгеброй Ли и непереходящей Killing-плотностью над полем характеристика ноль относительно разбиения по Cartan-подалгебре, строится из весовых пространств L относительно H, короты задаются через α, а отражения образуют reflectRoot.
LaTeX
$$$\text{rootSystem}(H) \text{ is the RootSystem built from weights on } L \text{ with root map } i \mapsto i \text{ and coroot map } i \mapsto \operatorname{coroot}(i)$$$
Lean4
/-- The root system of a finite-dimensional Lie algebra with non-degenerate Killing form over a
field of characteristic zero, relative to a splitting Cartan subalgebra. -/
def rootSystem : RootSystem H.root K (Dual K H) H :=
RootSystem.mk' .id
{ toFun := (↑)
inj' := by intro α β h; ext x; simpa using LinearMap.congr_fun h x }
{ toFun := coroot ∘ (↑)
inj' := by rintro ⟨α, hα⟩ ⟨β, hβ⟩ h; simpa using h }
(fun ⟨α, hα⟩ ↦ by simpa using root_apply_coroot <| by simpa using hα)
(by
rintro ⟨α, hα⟩ - ⟨⟨β, hβ⟩, rfl⟩
simpa using ⟨reflectRoot α β, by simpa using reflectRoot_isNonZero α β <| by simpa using hβ, rfl⟩)
(by convert span_weight_isNonZero_eq_top K L H; ext; simp)
(fun α β ↦ ⟨chainBotCoeff β.1 α.1 - chainTopCoeff β.1 α.1, by simp [apply_coroot_eq_cast β.1 α.1]⟩)
