span_orbit_eq_top — Mathlib

English

For any i ∈ ι, the span of the Weyl-group orbit of P.root i is the whole space.

Русский

Для любого i из ι линейное пространство, порождаемое орбитой корня P.root i группой Weyl, совпадает с всей пространством.

LaTeX

$$$$ \operatorname{span}_R(\operatorname{orbit}_{P.weylGroup}(P.root i)) = \top. $$$$

Lean4

theorem span_orbit_eq_top (i : ι) : span R (orbit P.weylGroup (P.root i)) = ⊤ :=
  by
  refine IsIrreducible.eq_top_of_invtSubmodule_reflection (P := P) _ (fun j ↦ ?_) ?_
  · let g : P.weylGroup := ⟨Equiv.reflection P j, P.reflection_mem_weylGroup j⟩
    exact Module.End.span_orbit_mem_invtSubmodule R (P.root i) g
  · simpa using ⟨P.root i, mem_orbit_self _, P.ne_zero i⟩

Похожие утверждения