feat: add characterisation of irreducible root pairing using IsSimpleOrder (leanprover-community#24958)

Author: ocfnash

Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

@@ -32,6 +32,29 @@ variable {ι R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommG
 
 namespace RootPairing
 
+/-- The sublattice of invariant submodules of the root space. -/
+def invtRootSubmodule : Sublattice (Submodule R M) :=
+  ⨅ i, invtSubmodule (P.reflection i)
+
+lemma mem_invtRootSubmodule_iff {q : Submodule R M} :
+    q ∈ P.invtRootSubmodule ↔ ∀ i, q ∈ Module.End.invtSubmodule (P.reflection i) := by
+  simp [invtRootSubmodule]
+
+@[simp] protected lemma invtRootSubmodule.top_mem : ⊤ ∈ P.invtRootSubmodule := by
+  simp [invtRootSubmodule]
+
+@[simp] protected lemma invtRootSubmodule.bot_mem : ⊥ ∈ P.invtRootSubmodule := by
+  simp [invtRootSubmodule]
+
+instance : BoundedOrder P.invtRootSubmodule where
+  top := ⟨⊤, invtRootSubmodule.top_mem P⟩
+  bot := ⟨⊥, invtRootSubmodule.bot_mem P⟩
+  le_top := fun ⟨p, hp⟩ ↦ by simp
+  bot_le := fun ⟨p, hp⟩ ↦ by simp
+
+instance [Nontrivial M] : Nontrivial P.invtRootSubmodule where
+  exists_pair_ne := ⟨⊥, ⊤, by rw [ne_eq, Subtype.ext_iff]; exact bot_ne_top⟩
+
 lemma 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
@@ -105,6 +128,20 @@ lemma IsIrreducible.mk' {K : Type*} [Field K] [Module K M] [Module K N] [Nontriv
     replace ne_bot : q.dualAnnihilator ≠ ⊤ := by simpa
     simpa using h ne_bot
 
+lemma isIrreducible_iff_invtRootSubmodule
+    {K : Type*} [Field K] [Module K M] [Module K N] [Nontrivial M] (P : RootPairing ι K M N) :
+    P.IsIrreducible ↔ IsSimpleOrder P.invtRootSubmodule := by
+  refine ⟨fun h ↦ ⟨fun ⟨q, hq⟩ ↦ ?_⟩, fun h ↦ IsIrreducible.mk' P fun q hq hq' ↦ ?_⟩
+  · simp only [invtRootSubmodule.bot_mem,  invtRootSubmodule.top_mem, Subtype.mk_eq_bot_iff,
+      Subtype.mk_eq_top_iff]
+    rw [mem_invtRootSubmodule_iff] at hq
+    have := IsIrreducible.eq_top_of_invtSubmodule_reflection q hq
+    tauto
+  · let q' : P.invtRootSubmodule := ⟨q, P.mem_invtRootSubmodule_iff.mpr hq⟩
+    replace hq' : ⊥ < q' := by simpa [q', bot_lt_iff_ne_bot]
+    suffices q' = ⊤ by simpa [q'] using this
+    exact IsSimpleOrder.eq_top_of_lt hq'
+
 lemma exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule
     [NeZero (2 : R)] [NoZeroSMulDivisors R M] (q : Submodule R M)
     (hq : ∀ i, q ∈ invtSubmodule (P.reflection i)) :