English
A variant of corootSpace: x ∈ corootSpace α iff x ∈ span of brackets between rootSpace(H,α) and rootSpace(H(-α)) with the subalgebra H included.
Русский
Вариант corootSpace: x ∈ corootSpace α тогда и только тогда, когда x ∈ span скобок между rootSpace(H,α) и rootSpace(H(-α)) с включением H.
LaTeX
$$$x \in \operatorname{corootSpace}(\alpha) \iff x \in \operatorname{span}_R (\{ [y,z] \\mid y \in \operatorname{rootSpace}(H,\alpha), z \in \operatorname{rootSpace}(H, -\alpha)\})$$$
Lean4
theorem mem_corootSpace' {x : H} :
x ∈ corootSpace α ↔ x ∈ Submodule.span R ({⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} : Set H) :=
by
set s : Set H := ({⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} : Set H)
suffices H.subtype '' s = {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))}
by
erw [← (H : Submodule R L).injective_subtype.mem_set_image (s := Submodule.span R s)]
rw [mem_image]
simp_rw [SetLike.mem_coe]
rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
ext u
simp only [Submodule.coe_subtype, mem_image, Subtype.exists, LieSubalgebra.mem_toSubmodule, exists_and_right,
exists_eq_right, mem_setOf_eq, s]
refine ⟨fun ⟨_, y, hy, z, hz, hyz⟩ ↦ ⟨y, hy, z, hz, hyz⟩, fun ⟨y, hy, z, hz, hyz⟩ ↦ ⟨?_, y, hy, z, hz, hyz⟩⟩
convert (rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)).property using 0
simp [hyz]
