English
For α : H → R and x ∈ corootSpace α, x lies in the span of brackets of root spaces: x ∈ span{ [y,z] | y ∈ rootSpace(H,α), z ∈ rootSpace(H,−α) }.
Русский
Для α : H → R и x в corootSpace α, x лежит в области порождающихся скобок: x ∈ span{ [y,z] | y ∈ rootSpace(H,α), z ∈ rootSpace(H,−α) }.
LaTeX
$$$x \in \operatorname{corootSpace}(\alpha) \iff x \in \operatorname{span}_R\{\,[y,z]\;|\; y \in \operatorname{rootSpace}(H,\alpha), z \in \operatorname{rootSpace}(H,-\alpha)\}$$$
Lean4
theorem mem_corootSpace {x : H} :
x ∈ corootSpace α ↔ (x : L) ∈ Submodule.span R ({⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))}) :=
by
have : x ∈ corootSpace α ↔ (x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α) :=
by
rw [corootSpace]
simp only [rootSpaceProduct_def, LieModuleHom.mem_range, LieSubmodule.mem_map, LieSubmodule.incl_apply,
SetLike.coe_eq_coe, exists_eq_right]
rfl
simp_rw [this, corootSpace, ← LieModuleHom.map_top, ← LieSubmodule.mem_toSubmodule, LieSubmodule.toSubmodule_map,
LieSubmodule.top_toSubmodule, ← TensorProduct.span_tmul_eq_top, LinearMap.map_span, Set.image, Set.mem_setOf_eq,
exists_exists_exists_and_eq]
change (x : L) ∈ Submodule.span R {x | ∃ (a : rootSpace H α) (b : rootSpace H (-α)), ⁅(a : L), (b : L)⁆ = x} ↔ _
simp
