feat: define the sl₂ Lie subalgebra associated to a root (#24995)

The lemma `root_mem_submodule_iff_of_add_mem_invtSubmodule` is related in the sense that it can be used to prove the subalgebra associated to the roots in an invariant submodule is an ideal.

Author: ocfnash

Mathlib/Algebra/Lie/Sl2.lean

@@ -91,6 +91,51 @@ 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. -/
+def toLieSubalgebra (t : IsSl2Triple h e f) :
+    LieSubalgebra R L where
+  __ := span R {e, f, h}
+  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_e_f]
+          apply subset_span
+          simp
+        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
+          apply nsmul_mem <| subset_span _
+          simp
+        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
+          apply subset_span
+          simp
+        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
+          apply nsmul_mem <| subset_span _
+          simp
+        · 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
+
+lemma mem_toLieSubalgebra_iff {x : L} {t : IsSl2Triple h e f} :
+    x ∈ t.toLieSubalgebra R ↔ ∃ c₁ c₂ c₃ : R, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ := by
+  simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
+    eq_comm]
+
 namespace HasPrimitiveVectorWith
 
 variable {m : M} {μ : R} {t : IsSl2Triple h e f}

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -135,8 +135,58 @@ lemma mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg
   | add => simp_all
 end
 
+end Field
+
+end LieAlgebra
+
+namespace LieModule
+
+namespace Weight
+
+open LieAlgebra IsKilling
+
+variable {K L}
+
+variable [FiniteDimensional K L] [IsKilling K L]
+  {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K H L] {α : Weight K H L}
+
+instance : InvolutiveNeg (Weight K H L) where
+  neg α := ⟨-α, by
+    by_cases hα : α.IsZero
+    · convert α.genWeightSpace_ne_bot; rw [hα, neg_zero]
+    · intro e
+      obtain ⟨x, hx, x_ne0⟩ := α.exists_ne_zero
+      have := mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H hx
+        (fun y hy ↦ by rw [rootSpace, e] at hy; rw [hy, map_zero])
+      rw [ker_killingForm_eq_bot] at this
+      exact x_ne0 this⟩
+  neg_neg α := by ext; simp
+
+@[simp] lemma coe_neg : ((-α : Weight K H L) : H → K) = -α := rfl
+
+lemma IsZero.neg (h : α.IsZero) : (-α).IsZero := by ext; rw [coe_neg, h, neg_zero]
+
+@[simp] lemma isZero_neg : (-α).IsZero ↔ α.IsZero := ⟨fun h ↦ neg_neg α ▸ h.neg, fun h ↦ h.neg⟩
+
+lemma IsNonZero.neg (h : α.IsNonZero) : (-α).IsNonZero := fun e ↦ h (by simpa using e.neg)
+
+@[simp] lemma isNonZero_neg {α : Weight K H L} : (-α).IsNonZero ↔ α.IsNonZero := isZero_neg.not
+
+@[simp] lemma toLinear_neg {α : Weight K H L} : (-α).toLinear = -α.toLinear := rfl
+
+end Weight
+
+end LieModule
+
+namespace LieAlgebra
+
+open Module LieModule Set
+open Submodule renaming span → span
+open Submodule renaming subset_span → subset_span
+
 namespace IsKilling
 
+variable [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra]
 variable [IsKilling K L]
 
 /-- If a Lie algebra `L` has non-degenerate Killing form, the only element of a Cartan subalgebra
@@ -188,6 +238,10 @@ lemma traceForm_coroot (α : Weight K H L) (x : H) :
   rw [coroot, map_nsmul, map_smul, LinearMap.smul_apply, LinearMap.smul_apply]
   congr 2
 
+@[simp] lemma coroot_neg [IsTriangularizable K H L] (α : Weight K H L) :
+    coroot (-α) = -coroot α := by
+  simp [coroot]
+
 variable [IsTriangularizable K H L]
 
 lemma lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux
@@ -557,6 +611,39 @@ 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
+
+lemma mem_sl2SubalgebraOfRoot_iff {α : Weight K H L} (hα : α.IsNonZero) {h e f : L}
+    (t : IsSl2Triple h e f) (hte : e ∈ rootSpace H α) (htf : f ∈ rootSpace H (- α)) {x : L} :
+    x ∈ sl2SubalgebraOfRoot hα ↔ ∃ c₁ c₂ c₃ : K, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ := by
+  simp only [sl2SubalgebraOfRoot, IsSl2Triple.mem_toLieSubalgebra_iff]
+  generalize_proofs _ _ _ he hf
+  obtain ⟨ce, hce⟩ : ∃ c : K, he.choose = c • e := by
+    obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨e, hte⟩ (by simpa using t.e_ne_zero)).mp
+      (finrank_rootSpace_eq_one α hα) ⟨_, he.choose_spec.choose_spec.2.1⟩
+    exact ⟨c, by simpa using hc.symm⟩
+  obtain ⟨cf, hcf⟩ : ∃ c : K, hf.choose = c • f := by
+    obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨f, htf⟩ (by simpa using t.f_ne_zero)).mp
+      (finrank_rootSpace_eq_one (-α) (by simpa)) ⟨_, hf.choose_spec.2.2⟩
+    exact ⟨c, by simpa using hc.symm⟩
+  have hce₀ : ce ≠ 0 := by
+    rintro rfl
+    simp only [zero_smul] at hce
+    exact he.choose_spec.choose_spec.1.e_ne_zero hce
+  have hcf₀ : cf ≠ 0 := by
+    rintro rfl
+    simp only [zero_smul] at hcf
+    exact he.choose_spec.choose_spec.1.f_ne_zero hcf
+  simp_rw [hcf, hce]
+  refine ⟨fun ⟨c₁, c₂, c₃, hx⟩ ↦ ⟨c₁ * ce, c₂ * cf, c₃ * cf * ce, ?_⟩,
+    fun ⟨c₁, c₂, c₃, hx⟩ ↦ ⟨c₁ * ce⁻¹, c₂ * cf⁻¹, c₃ * ce⁻¹ * cf⁻¹, ?_⟩⟩
+  · simp [hx, mul_smul]
+  · simp [hx, mul_smul, hce₀, hcf₀]
+
 /-- The collection of roots as a `Finset`. -/
 noncomputable abbrev _root_.LieSubalgebra.root : Finset (Weight K H L) := {α | α.IsNonZero}
 
@@ -571,52 +658,4 @@ end CharZero
 
 end IsKilling
 
-end Field
-
 end LieAlgebra
-
-namespace LieModule
-
-namespace Weight
-
-open LieAlgebra IsKilling
-
-variable {K L}
-
-variable [FiniteDimensional K L]
-variable [IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K H L]
-variable {α : Weight K H L}
-
-instance : InvolutiveNeg (Weight K H L) where
-  neg α := ⟨-α, by
-    by_cases hα : α.IsZero
-    · convert α.genWeightSpace_ne_bot; rw [hα, neg_zero]
-    · intro e
-      obtain ⟨x, hx, x_ne0⟩ := α.exists_ne_zero
-      have := mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H hx
-        (fun y hy ↦ by rw [rootSpace, e] at hy; rw [hy, map_zero])
-      rw [ker_killingForm_eq_bot] at this
-      exact x_ne0 this⟩
-  neg_neg α := by ext; simp
-
-@[simp] lemma coe_neg : ((-α : Weight K H L) : H → K) = -α := rfl
-
-lemma IsZero.neg (h : α.IsZero) : (-α).IsZero := by ext; rw [coe_neg, h, neg_zero]
-
-@[simp] lemma isZero_neg : (-α).IsZero ↔ α.IsZero := ⟨fun h ↦ neg_neg α ▸ h.neg, fun h ↦ h.neg⟩
-
-lemma IsNonZero.neg (h : α.IsNonZero) : (-α).IsNonZero := fun e ↦ h (by simpa using e.neg)
-
-@[simp] lemma isNonZero_neg {α : Weight K H L} : (-α).IsNonZero ↔ α.IsNonZero := isZero_neg.not
-
-@[simp] lemma toLinear_neg {α : Weight K H L} : (-α).toLinear = -α.toLinear := rfl
-
-variable [CharZero K]
-
-@[simp]
-lemma _root_.LieAlgebra.IsKilling.coroot_neg (α : Weight K H L) : coroot (-α) = -coroot α := by
-  simp [coroot]
-
-end Weight
-
-end LieModule

Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

@@ -231,6 +231,29 @@ 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 : P.invtRootSubmodule)
+    (hij : P.root i + P.root j ∈ range P.root) :
+    P.root i ∈ (q : Submodule K M) ↔ P.root j ∈ (q : Submodule K M) := by
+  obtain ⟨q, hq⟩ := q
+  rw [mem_invtRootSubmodule_iff] at hq
+  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)

Mathlib/LinearAlgebra/Span/Defs.lean

@@ -450,6 +450,16 @@ theorem mem_span_pair {x y z : M} :
     z ∈ span R ({x, y} : Set M) ↔ ∃ a b : R, a • x + b • y = z := by
   simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
 
+theorem mem_span_triple {w x y z : M} :
+    w ∈ span R ({x, y, z} : Set M) ↔ ∃ a b c : R, a • x + b • y + c • z = w := by
+  rw [mem_span_insert]
+  simp_rw [mem_span_pair]
+  refine exists_congr fun a ↦ ⟨?_, ?_⟩
+  · rintro ⟨u, ⟨b, c, rfl⟩, rfl⟩
+    exact ⟨b, c, by rw [add_assoc]⟩
+  · rintro ⟨b, c, rfl⟩
+    exact ⟨b • y + c • z, ⟨b, c, rfl⟩, by rw [add_assoc]⟩
+
 @[simp]
 theorem span_eq_bot : span R (s : Set M) = ⊥ ↔ ∀ x ∈ s, (x : M) = 0 :=
   eq_bot_iff.trans