English
If α is nonzero, the root space is one-dimensional.
Русский
Корневое пространство ненулевого корня α одномерно.
LaTeX
$$finrank_K(rootSpace(H,α)) = 1$$
Lean4
theorem finrank_rootSpace_eq_one (α : Weight K H L) (hα : α.IsNonZero) : finrank K (rootSpace H α) = 1 :=
by
suffices ¬1 < finrank K (rootSpace H α)
by
have h₀ : finrank K (rootSpace H α) ≠ 0 :=
by
convert_to finrank K (rootSpace H α).toSubmodule ≠ 0
simpa using α.genWeightSpace_ne_bot
cutsat
intro contra
obtain ⟨h, e, f, ht, heα, hfα⟩ := exists_isSl2Triple_of_weight_isNonZero hα
let F : rootSpace H α →ₗ[K] K := killingForm K L f ∘ₗ (rootSpace H α).subtype
have hF : LinearMap.ker F ≠ ⊥ := F.ker_ne_bot_of_finrank_lt <| by rwa [finrank_self]
obtain ⟨⟨y, hyα⟩, hy, hy₀⟩ := (Submodule.ne_bot_iff _).mp hF
replace hy : ⁅y, f⁆ = 0 :=
by
have : killingForm K L y f = 0 := by simpa [F, traceForm_comm] using hy
simpa [this] using lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg hyα hfα
have P : ht.symm.HasPrimitiveVectorWith y (-2 : K) :=
{ ne_zero := by simpa [LieSubmodule.mk_eq_zero] using hy₀
lie_h := by
simp only [neg_smul, neg_lie, ht.h_eq_coroot hα heα hfα, ← H.coe_bracket_of_module,
lie_eq_smul_of_mem_rootSpace hyα (coroot α), root_apply_coroot hα]
lie_e := by rw [← lie_skew, hy, neg_zero] }
obtain ⟨n, hn⟩ := P.exists_nat
assumption_mod_cast
