[Merged by Bors] - feat: define the sl₂ Lie subalgebra associated to a root

Mathlib/Algebra/Lie/Sl2.lean

@@ -91,6 +91,46 @@ lemma HasPrimitiveVectorWith.mk' [NoZeroSMulDivisors ℤ M] (t : IsSl2Triple h e
     rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
       smul_smul, smul_smul, mul_comm ρ μ, sub_self]
 
+variable (R) in
+open Submodule in
+/-- The subalgebra associated to an `sl₂` triple. -/
+@[simps!] def toLieSubalgebra (t : IsSl2Triple h e f) :
+    LieSubalgebra R L where
+  __ := span R {h, e, f}
+  lie_mem' {x y} hx hy := by
+    simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢
+    induction hx using span_induction with
+    | zero => simp
+    | add u v hu hv hu' hv' => simpa only [add_lie] using add_mem hu' hv'
+    | smul t u hu hu' => simpa only [smul_lie] using smul_mem _ t hu'
+    | mem u hu =>
+      induction hy using span_induction with
+      | zero => simp
+      | add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
+      | smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
+      | mem v hv =>
+        simp only [mem_insert_iff, mem_singleton_iff] at hu hv
+        rcases hu with rfl | rfl | rfl <;>
+        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
+        · rw [t.lie_h_e_nsmul]
+          apply nsmul_mem <| subset_span _
+          simp
+        · rw [t.lie_h_f_nsmul, neg_mem_iff]
+          apply nsmul_mem <| subset_span _
+          simp
+        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
+          apply nsmul_mem <| subset_span _
+          simp
+        · rw [t.lie_e_f]
+          apply subset_span
+          simp
+        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
+          apply nsmul_mem <| subset_span _
+          simp
+        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
+          apply subset_span
+          simp
+
 namespace HasPrimitiveVectorWith
 
 variable {m : M} {μ : R} {t : IsSl2Triple h e f}

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -557,6 +557,12 @@ lemma finrank_rootSpace_eq_one (α : Weight K H L) (hα : α.IsNonZero) :
   replace hn : -2 = (n : ℤ) := by norm_cast at hn
   omega
 
+/-- The embedded `sl₂` associated to a root. -/
+noncomputable def sl2SubalgebraOfRoot {α : Weight K H L} (hα : α.IsNonZero) :
+    LieSubalgebra K L := by
+  choose h e f t ht using exists_isSl2Triple_of_weight_isNonZero hα
+  exact t.toLieSubalgebra K
+
 /-- The collection of roots as a `Finset`. -/
 noncomputable abbrev _root_.LieSubalgebra.root : Finset (Weight K H L) := {α | α.IsNonZero}
 

Mathlib/Algebra/Lie/Weights/RootSystem.lean

@@ -422,4 +422,9 @@ instance : (rootSystem H).IsReduced where
     · right; ext x; simpa [neg_eq_iff_eq_neg] using DFunLike.congr_fun h.symm x
     · left; ext x; simpa using DFunLike.congr_fun h.symm x
 
+/-- The Lie subalgebra assocatied to a submodule of the dual of a Cartan subalgebra. -/
+@[simps!] def lieSubalgebraOfSubmoduleRootSystem (q : Submodule K (Dual K H)) :
+    LieSubalgebra K L where
+  __ := ⨆ (α : Weight K H L) (hα : α.IsNonZero) (_ : ↑α ∈ q), sl2SubalgebraOfRoot hα
+
 end LieAlgebra.IsKilling

Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

@@ -231,6 +231,27 @@ lemma root_add_root_mem_of_pairingIn_neg (h : P.pairingIn ℤ i j < 0) (h' : α
   replace h' : i ≠ -j := by contrapose! h'; simp [h']
   simpa using P.root_sub_root_mem_of_pairingIn_pos h h'
 
+omit [Finite ι] in
+lemma root_mem_submodule_iff_of_add_mem_invtSubmodule
+    {K : Type*} [Field K] [NeZero (2 : K)] [Module K M] [Module K N] {P : RootPairing ι K M N}
+    (q : Submodule K M) (hq : ∀ i, q ∈ Module.End.invtSubmodule (P.reflection i))
+    (hij : P.root i + P.root j ∈ range P.root) :
+    P.root i ∈ q ↔ P.root j ∈ q := by
+  suffices ∀ i j, P.root i + P.root j ∈ range P.root → P.root i ∈ q → P.root j ∈ q by
+    have aux := this j i (by rwa [add_comm]); tauto
+  rintro i j ⟨k, hk⟩ hi
+  rcases eq_or_ne (P.pairing i j) 0 with hij₀ | hij₀
+  · have hik : P.pairing i k ≠ 0 := by
+      rw [ne_eq, P.pairing_eq_zero_iff, ← root_coroot_eq_pairing, hk]
+      simpa [P.pairing_eq_zero_iff.mp hij₀] using two_ne_zero
+    suffices P.root k ∈ q from (q.add_mem_iff_right hi).mp <| hk ▸ this
+    replace hq : P.root i - P.pairing i k • P.root k ∈ q := by
+      simpa [reflection_apply_root] using hq k hi
+    rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hik] at hq
+  · replace hq : P.root i - P.pairing i j • P.root j ∈ q := by
+      simpa [reflection_apply_root] using hq j hi
+    rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hij₀] at hq
+
 namespace InvariantForm
 
 variable [P.IsReduced] (B : P.InvariantForm)