English
The coroot space is spanned by a distinguished coroot vector corresponding to α.
Русский
Коротовное пространство порождается выделенным вектором корня α.
LaTeX
$$$\operatorname{corootSpace}(\alpha) = \operatorname{Span}_K\{ (\mathrm{cartanEquivDual} H)^{-1}(\alpha) \}$$$
Lean4
theorem coe_corootSpace_eq_span_singleton' (α : Weight K H L) :
(corootSpace α).toSubmodule = K ∙ (cartanEquivDual H).symm α :=
by
refine le_antisymm ?_ ?_
· intro ⟨x, hx⟩ hx'
have : {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} ⊆ K ∙ ((cartanEquivDual H).symm α : L) :=
by
rintro - ⟨e, heα, f, hfα, rfl⟩
rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
Submodule.mem_span_singleton]
exact ⟨killingForm K L e f, rfl⟩
simp only [LieSubmodule.mem_toSubmodule, mem_corootSpace] at hx'
replace this := Submodule.span_mono this hx'
rw [Submodule.span_span] at this
rw [Submodule.mem_span_singleton] at this ⊢
obtain ⟨t, rfl⟩ := this
solve_by_elim
· simp only [Submodule.span_singleton_le_iff_mem, LieSubmodule.mem_toSubmodule]
exact cartanEquivDual_symm_apply_mem_corootSpace α
