feat: order isomorphism between ideals and invariant root submodules (#37285)

Order isomorphism between ideals and invariant root submodules

Co-authored-by: Janos Wolosz <janos.wolosz@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

Author: jano-wol

Mathlib/Algebra/Lie/Killing.lean

@@ -98,6 +98,16 @@ instance instHasTrivialRadical
     HasTrivialRadical R L :=
   (hasTrivialRadical_iff_no_abelian_ideals R L).mpr IsKilling.ideal_eq_bot_of_isLieAbelian
 
+theorem isLieAbelian_iff_subsingleton
+    [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] :
+    IsLieAbelian L ↔ Subsingleton L := by
+  constructor
+  · intro h
+    rw [isLieAbelian_iff_center_eq_top R] at h
+    have hc : (⊤ : LieIdeal R L) = ⊥ := by rw [← center_eq_bot R L, h]
+    exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_top_eq_bot hc)
+  · exact fun _ => inferInstance
+
 end IsKilling
 
 section LieEquiv

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -108,6 +108,15 @@ instance : HasTrivialRadical R L := by
 
 end IsSimple
 
+lemma isSimple_iff_of_not_isLieAbelian (hL : ¬ IsLieAbelian L) :
+    IsSimpleOrder (LieIdeal R L) ↔ IsSimple R L :=
+  ⟨fun _ ↦ ⟨IsSimpleOrder.eq_bot_or_eq_top, hL⟩, fun _ ↦ inferInstance⟩
+
+@[nontriviality]
+lemma not_isSimple_of_subsingleton [Subsingleton L] :
+    ¬ IsSimple R L :=
+  fun contra ↦ contra.non_abelian inferInstance
+
 namespace IsSemisimple
 
 open CompleteLattice IsCompactlyGenerated

Mathlib/Algebra/Lie/Weights/IsSimple.lean

@@ -17,19 +17,20 @@ Weyl-group-invariant submodules of the corresponding root system. In this file w
 and `LieAlgebra.IsKilling.invtSubmoduleToLieIdeal`, which constructs the ideal associated to an
 invariant submodule.
 
-As of Mar 2026, the proofs that these maps are part of an order isomorphism is still pending.
-
 ## Main definitions
 * `LieIdeal.rootSet`: the set of roots whose root space is contained in a given Lie ideal.
 * `LieIdeal.rootSpan`: the submodule of `Dual K H` spanned by `LieIdeal.rootSet`.
 * `LieIdeal.toInvtRootSubmodule`: the invariant root submodule associated to an ideal.
 * `LieAlgebra.IsKilling.invtSubmoduleToLieIdeal`: constructs a Lie ideal from an invariant
-  submodule of the dual space
+  submodule of the dual space.
+* `LieAlgebra.IsKilling.lieIdealOrderIso`: the order isomorphism between Lie ideals and
+  invariant root submodules.
 
 ## Main results
 * `LieAlgebra.IsKilling.restr_inf_cartan_eq_iSup_corootSubmodule`: the intersection of a Lie ideal
   and a Cartan subalgebra is the span of the coroots whose roots have root spaces in the ideal.
-* `LieAlgebra.IsKilling.instIsIrreducible`: the root system of a simple Lie algebra is irreducible
+* `LieAlgebra.IsKilling.isSimple_iff_isIrreducible`: a Killing Lie algebra is simple if and only
+  if its root system is irreducible.
 -/
 
 @[expose] public section
@@ -500,84 +501,63 @@ lemma mem_rootSet_invtSubmoduleToLieIdeal (q : Submodule K (Dual K H))
           le_iSup_of_le ⟨↑α, hα, H.isNonZero_coe_root α⟩ le_rfl
       _ = J.restr H := (restr_invtSubmoduleToLieIdeal_eq_iSup q hq).symm
 
-open LieSubmodule in
-@[simp] lemma invtSubmoduleToLieIdeal_top :
-    invtSubmoduleToLieIdeal (⊤ : Submodule K (Module.Dual K H)) (by simp) = ⊤ := by
-  simp_rw [← toSubmodule_inj, coe_invtSubmoduleToLieIdeal_eq_iSup, iSup_toSubmodule,
-    top_toSubmodule, iSup_toSubmodule_eq_top, eq_top_iff, ← cartan_sup_iSup_rootSpace_eq_top H,
-    iSup_subtype, Submodule.mem_top, true_and, sup_le_iff, iSup_le_iff, sl2SubmoduleOfRoot_eq_sup]
-  refine ⟨?_, fun α hα ↦ le_iSup₂_of_le α hα <| le_sup_of_le_left <| le_sup_of_le_left <| le_refl _⟩
-  suffices H.toLieSubmodule ≤ ⨆ α : Weight K H L, ⨆ (_ : α.IsNonZero), corootSubmodule α from
-    this.trans <| iSup₂_mono fun α hα ↦ le_sup_right
-  simp
-
-@[simp] lemma invtSubmoduleToLieIdeal_apply_eq_top_iff (q : Submodule K (Dual K H))
-    (hq : ∀ i, q ∈ End.invtSubmodule ((rootSystem H).reflection i).toLinearMap) :
-    invtSubmoduleToLieIdeal q hq = ⊤ ↔ q = ⊤ := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-  have h : (⨆ α : {α : Weight K H L // ↑α ∈ q ∧ α.IsNonZero}, sl2SubmoduleOfRoot α.2.2) = ⊤ := by
-    rw [← LieSubmodule.toSubmodule_inj] at h
-    have := coe_invtSubmoduleToLieIdeal_eq_iSup q hq
-    exact (LieSubmodule.toSubmodule_eq_top (⨆ α, sl2SubmoduleOfRoot α.property.right)).mp h
-  by_contra hq_ne_top
-  have h_ne_bot : q.dualCoannihilator ≠ ⊥ := by
-    contrapose! hq_ne_top
-    have := Subspace.finrank_add_finrank_dualCoannihilator_eq q
-    rw [hq_ne_top, finrank_bot, add_zero] at this
-    exact Submodule.eq_top_of_finrank_eq (this.trans Subspace.dual_finrank_eq.symm)
-  obtain ⟨y, hy_mem, hy_ne_zero⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h_ne_bot
-  have hy_ortho : ∀ f ∈ q, f y = 0 := (Submodule.mem_dualCoannihilator y).mp hy_mem
-  have h_comm : ∀ α : {α : Weight K H L // ↑α ∈ q ∧ α.IsNonZero},
-      ∀ z ∈ sl2SubmoduleOfRoot α.2.2, ⁅(y : L), z⁆ = 0 := fun α z hz => by
-    have hy : (α.1 : H → K) y = 0 := hy_ortho _ α.2.1
-    rw [sl2SubmoduleOfRoot_eq_sup] at hz
-    obtain ⟨z_αneg, hz_αneg, z_cor, ⟨h_cor, _, rfl⟩, rfl⟩ := Submodule.mem_sup.mp hz
-    obtain ⟨z_α, hz_α, z_negα, hz_negα, rfl⟩ := Submodule.mem_sup.mp hz_αneg
-    simp only [lie_add, ← LieSubalgebra.coe_bracket_of_module]
-    rw [lie_eq_smul_of_mem_rootSpace hz_α, hy, zero_smul, zero_add,
-        lie_eq_smul_of_mem_rootSpace hz_negα, Pi.neg_apply, hy, neg_zero, zero_smul, zero_add]
-    have h_cor_in_zero : (h_cor : L) ∈ rootSpace H (0 : H → K) := by
-      rw [rootSpace_zero_eq]; exact h_cor.property
-    convert lie_eq_smul_of_mem_rootSpace h_cor_in_zero y using 1; simp
-  have h_comm_all : ∀ z : L, ⁅(y : L), z⁆ = 0 := fun z => by
-    have hz : z ∈ ⨆ α : {α : Weight K H L // ↑α ∈ q ∧ α.IsNonZero},
-        (sl2SubmoduleOfRoot α.2.2).toSubmodule := by
-      convert Submodule.mem_top using 1
-      rw [← LieSubmodule.iSup_toSubmodule, h]; rfl
-    rw [Submodule.mem_iSup] at hz
-    exact hz (LinearMap.ker (ad K L y)) fun α z hz => by simpa using h_comm α z hz
-  have h_y_center : (y : L) ∈ LieAlgebra.center K L := fun z => by
-    rw [← lie_skew, h_comm_all, neg_zero]
-  simp only [center_eq_bot, LieSubmodule.mem_bot, ZeroMemClass.coe_eq_zero] at h_y_center
-  exact hy_ne_zero h_y_center
-
-@[simp] lemma invtSubmoduleToLieIdeal_apply_eq_bot_iff (q : Submodule K (Module.Dual K H))
-    (hq : ∀ i, q ∈ Module.End.invtSubmodule ((rootSystem H).reflection i).toLinearMap) :
-    invtSubmoduleToLieIdeal q hq = ⊥ ↔ q = ⊥ := by
-  refine ⟨fun h => ?_, fun h => ?_⟩
-  · by_contra hq_nonzero
-    have hq_invt : q ∈ (rootSystem H).invtRootSubmodule := by
-      rw [RootPairing.mem_invtRootSubmodule_iff]; exact hq
-    have h_ne_bot : (⟨q, hq_invt⟩ : (rootSystem H).invtRootSubmodule) ≠ ⊥ :=
-      fun h_eq => hq_nonzero (Subtype.ext_iff.mp h_eq)
-    rw [Ne, RootPairing.invtRootSubmodule.eq_bot_iff, not_forall] at h_ne_bot
-    obtain ⟨i, hi⟩ := h_ne_bot
-    rw [not_not] at hi
-    have hα₀ : i.val.IsNonZero := (Finset.mem_filter.mp i.property).2
-    have h_sl2_le : (sl2SubmoduleOfRoot hα₀ : Submodule K L) ≤ invtSubmoduleToLieIdeal q hq := by
-      rw [LieIdeal.toLieSubalgebra_toSubmodule, coe_invtSubmoduleToLieIdeal_eq_iSup,
-        LieSubmodule.iSup_toSubmodule]
-      exact le_iSup_of_le ⟨i.val, hi, hα₀⟩ le_rfl
-    rw [h] at h_sl2_le
-    simp only [LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.bot_toSubmodule, le_bot_iff,
-      LieSubmodule.toSubmodule_eq_bot] at h_sl2_le
-    exact sl2SubmoduleOfRoot_ne_bot i.1 hα₀ h_sl2_le
-  · simp [h, invtSubmoduleToLieIdeal]
-
-instance [IsSimple K L] : (rootSystem H).IsIrreducible := by
-  have _i := nontrivial_of_isIrreducible K L L
-  exact RootPairing.IsIrreducible.mk' (rootSystem H) <| fun q h₀ h₁ ↦ by
-    have := IsSimple.eq_bot_or_eq_top (invtSubmoduleToLieIdeal q h₀)
-    aesop
+@[gcongr]
+lemma invtSubmoduleToLieIdeal_mono {q₁ q₂ : Submodule K (Dual K H)}
+    (hq₁ : ∀ i, q₁ ∈ End.invtSubmodule ((rootSystem H).reflection i).toLinearMap)
+    (hq₂ : ∀ i, q₂ ∈ End.invtSubmodule ((rootSystem H).reflection i).toLinearMap)
+    (h : q₁ ≤ q₂) :
+    invtSubmoduleToLieIdeal q₁ hq₁ ≤ invtSubmoduleToLieIdeal q₂ hq₂ := by
+  change (invtSubmoduleToLieIdeal q₁ hq₁).restr H ≤ (invtSubmoduleToLieIdeal q₂ hq₂).restr H
+  exact iSup_le fun ⟨α, hα_mem, hα_nz⟩ ↦ le_iSup_of_le ⟨α, h hα_mem, hα_nz⟩ le_rfl
+
+lemma lieIdealOrderIso_left_inv (I : LieIdeal K L)
+    (hI : ∀ α, I.rootSpan ∈ End.invtSubmodule ((rootSystem H).reflection α).toLinearMap :=
+      (rootSystem H).mem_invtRootSubmodule_iff.mp I.rootSpan_mem_invtRootSubmodule) :
+    invtSubmoduleToLieIdeal I.rootSpan hI = I := by
+  set J := invtSubmoduleToLieIdeal I.rootSpan
+    ((rootSystem H).mem_invtRootSubmodule_iff.mp I.rootSpan_mem_invtRootSubmodule)
+  have h_eq : ∀ α : H.root, α ∈ J.rootSet ↔ α ∈ I.rootSet := fun α ↦ by
+    rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]
+    exact ⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, rfl⟩⟩
+  have h_restr : J.restr H = I.restr H := by
+    rw [J.restr_eq_iSup_sl2SubmoduleOfRoot, I.restr_eq_iSup_sl2SubmoduleOfRoot]
+    exact le_antisymm
+      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).1 hα) le_rfl)
+      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).2 hα) le_rfl)
+  rw [← LieSubmodule.toSubmodule_inj, ← LieSubmodule.restr_toSubmodule J H,
+    ← LieSubmodule.restr_toSubmodule I H, h_restr]
+
+lemma lieIdealOrderIso_right_inv (q : (rootSystem H).invtRootSubmodule)
+    (hq : ∀ α, ↑q ∈ End.invtSubmodule ((rootSystem H).reflection α).toLinearMap :=
+      (rootSystem H).mem_invtRootSubmodule_iff.mp q.property) :
+    (invtSubmoduleToLieIdeal q.1 hq).toInvtRootSubmodule = q := by
+  simp only [Subtype.ext_iff, LieIdeal.toInvtRootSubmodule, LieIdeal.rootSpan, LieIdeal.rootSet]
+  conv_rhs => rw [RootPairing.invtRootSubmodule.eq_span_root q]
+  congr 2; ext α
+  exact mem_rootSet_invtSubmoduleToLieIdeal _ _
+
+variable (H) in
+/-- The order isomorphism between Lie ideals and invariant root submodules. -/
+noncomputable def lieIdealOrderIso :
+    LieIdeal K L ≃o (rootSystem H).invtRootSubmodule where
+  toFun := LieIdeal.toInvtRootSubmodule
+  invFun q := invtSubmoduleToLieIdeal q.1 ((rootSystem H).mem_invtRootSubmodule_iff.mp q.2)
+  left_inv := lieIdealOrderIso_left_inv
+  right_inv := lieIdealOrderIso_right_inv
+  map_rel_iff' {I J} := by
+    refine ⟨fun h ↦ ?_, LieIdeal.toInvtRootSubmodule_mono⟩
+    rw [← lieIdealOrderIso_left_inv (H := H) I, ← lieIdealOrderIso_left_inv (H := H) J]
+    exact invtSubmoduleToLieIdeal_mono _ _ h
+
+/-- A Killing Lie algebra is simple if and only if its root system is irreducible. -/
+theorem isSimple_iff_isIrreducible : (rootSystem H).IsIrreducible ↔ IsSimple K L := by
+  nontriviality L
+  have hL : ¬ IsLieAbelian L :=
+    (isLieAbelian_iff_subsingleton K (L := L)).not.mpr (not_subsingleton L)
+  rw [RootPairing.isIrreducible_iff_invtRootSubmodule, ← isSimple_iff_of_not_isLieAbelian K L hL,
+    (lieIdealOrderIso H).isSimpleOrder_iff]
+
+instance [IsSimple K L] : (rootSystem H).IsIrreducible :=
+  isSimple_iff_isIrreducible.mpr ‹_›
 
 end LieAlgebra.IsKilling

Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

@@ -166,6 +166,11 @@ lemma isSimpleModule_weylGroupRootRep [P.IsIrreducible] :
   have := IsIrreducible.nontrivial P
   P.isSimpleModule_weylGroupRootRep_iff.mpr IsIrreducible.eq_top_of_invtSubmodule_reflection
 
+@[nontriviality]
+lemma not_isIrreducible_of_subsingleton [Subsingleton M] :
+    ¬ P.IsIrreducible :=
+  fun contra ↦ not_nontrivial _ contra.nontrivial
+
 /-- A nonempty irreducible root pairing is a root system. -/
 instance [Nonempty ι] [NeZero (2 : R)] [P.IsIrreducible] : P.IsRootSystem where
   span_root_eq_top := IsIrreducible.eq_top_of_invtSubmodule_reflection