English
Over a field K, the Weyl-group root representation is simple if and only if every nonzero invariant submodule under all reflections is the whole space.
Русский
Над полем K представление корневой группы Вейля простое тогда и только тогда, когда каждое ненулевое инвариантное подпространство относительно всех отражений есть всё пространство.
LaTeX
$$$$ \IsSimpleModule\left( \mathrm{MonoidAlgebra}_R(P.weylGroup) , P.weylGroupRootRep.asModule \right) \\Longleftrightarrow \\ \forall q \subset M,\; (\forall i, q \in invtSubmodule(P.reflection i)) \rightarrow q \neq \{0\} \rightarrow q = \top. $$$$
Lean4
theorem isSimpleModule_weylGroupRootRep_iff [Nontrivial M] :
IsSimpleModule (MonoidAlgebra R P.weylGroup) P.weylGroupRootRep.asModule ↔
∀ (q : Submodule R M), (∀ i, q ∈ invtSubmodule (P.reflection i)) → q ≠ ⊥ → q = ⊤ :=
by
rw [isSimpleModule_iff, ← P.weylGroupRootRep.mapSubmodule.isSimpleOrder_iff]
refine ⟨fun h q hq₁ hq₂ ↦ ?_, fun h ↦ ⟨fun q ↦ ?_⟩⟩
· suffices ∀ g : P.weylGroup, q ∈ invtSubmodule (P.weylGroupRootRep g)
by
let q' : P.weylGroupRootRep.invtSubmodule := ⟨q, (Representation.mem_invtSubmodule P.weylGroupRootRep).mpr this⟩
suffices q' = ⊤ by simpa [q']
apply (IsSimpleOrder.eq_bot_or_eq_top _).resolve_left
simpa [q']
rintro ⟨g, hg⟩
induction hg using weylGroup.induction with
| mem i => exact hq₁ i
| one => simp [← Submonoid.one_def]
| mul x y hx hy hx' hy' => apply invtSubmodule.comp <;> assumption
· rcases eq_or_ne q ⊥ with rfl | hq; · tauto
suffices (q : Submodule R M) = ⊤ by right; simpa using this
refine h q (fun i ↦ ?_) (by simpa using hq)
exact P.weylGroupRootRep.mem_invtSubmodule.mp q.property ⟨_, P.reflection_mem_weylGroup i⟩
