English
Equality of the sl2-submodule with the supremum of weight spaces and coroot submodule.
Русский
Равенство sl2-подмодуля верхнему пределу весовых пространств и подмодуля корота.
LaTeX
$$sl2SubmoduleOfRoot α = genWeightSpace L α ⊔ genWeightSpace L (−α) ⊔ corootSubmodule α$$
Lean4
theorem sl2SubmoduleOfRoot_eq_sup (α : Weight K H L) (hα : α.IsNonZero) :
sl2SubmoduleOfRoot hα = genWeightSpace L α ⊔ genWeightSpace L (-α) ⊔ corootSubmodule α :=
by
ext x
obtain ⟨h', e, f, ht, heα, hfα⟩ := exists_isSl2Triple_of_weight_isNonZero hα
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
· replace hx : x ∈ sl2SubalgebraOfRoot hα := hx
obtain ⟨c₁, c₂, c₃, rfl⟩ := (mem_sl2SubalgebraOfRoot_iff hα ht heα hfα).mp hx
refine add_mem (add_mem ?_ ?_) ?_
· exact mem_sup_left <| mem_sup_left <| smul_mem _ _ heα
· exact mem_sup_left <| mem_sup_right <| smul_mem _ _ hfα
· suffices ∃ y ∈ corootSpace α, H.subtype y = c₃ • h' from mem_sup_right <| by simpa [ht.lie_e_f, -Subtype.exists]
refine ⟨c₃ • coroot α, smul_mem _ _ <| by simp, ?_⟩
rw [IsSl2Triple.h_eq_coroot hα ht heα hfα, map_smul, subtype_apply]
· have aux {β : Weight K H L} (hβ : β.IsNonZero) {y g : L} (hy : y ∈ genWeightSpace L β) (hg : g ∈ rootSpace H β)
(hg_ne_zero : g ≠ 0) : ∃ c : K, y = c • g :=
by
obtain ⟨c, hc⟩ :=
(finrank_eq_one_iff_of_nonzero' ⟨g, hg⟩ (by rwa [ne_eq, LieSubmodule.mk_eq_zero])).mp
(finrank_rootSpace_eq_one β hβ) ⟨y, hy⟩
exact ⟨c, by simpa using hc.symm⟩
obtain ⟨x_αneg, hx_αneg, x_h, ⟨y, hy_coroot, rfl⟩, rfl⟩ := mem_sup.mp hx
obtain ⟨x_pos, hx_pos, x_neg, hx_neg, rfl⟩ := mem_sup.mp hx_αneg
obtain ⟨c₁, rfl⟩ := aux hα hx_pos heα ht.e_ne_zero
obtain ⟨c₂, rfl⟩ := aux (Weight.IsNonZero.neg hα) hx_neg hfα ht.f_ne_zero
obtain ⟨c₃, rfl⟩ : ∃ c₃ : K, c₃ • coroot α = y := by
simpa [← mem_span_singleton, ← coe_corootSpace_eq_span_singleton α]
change _ ∈ sl2SubalgebraOfRoot hα
rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα]
use c₁, c₂, c₃
simp [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, -LieSubmodule.incl_coe]
