feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739)

Author: ocfnash

Mathlib/Algebra/Lie/Killing.lean

@@ -242,7 +242,8 @@ lemma traceForm_eq_sum_weightSpaceOf [IsTriangularizable R L M] (z : L) :
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
   exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)
 
--- In characteristic zero a stronger result holds (no `⊓ LieAlgebra.center K L`) TODO prove this!
+-- In characteristic zero (or even just `LinearWeights R L M`) a stronger result holds (no
+-- `⊓ LieAlgebra.center R L`) TODO prove this using `LieModule.traceForm_eq_sum_finrank_nsmul_mul`.
 lemma lowerCentralSeries_one_inf_center_le_ker_traceForm :
     lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L ≤ LinearMap.ker (traceForm R L M) := by
   /- Sketch of proof (due to Zassenhaus):
@@ -490,32 +491,33 @@ lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L]
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
   exact Finset.sum_congr (by simp) (fun χ _ ↦ traceForm_weightSpace_eq K L M χ x y)
 
-@[simp]
-lemma LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot [LieAlgebra.IsNilpotent K L]
-    [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L]
-    (h : LinearMap.ker (traceForm K L M) = ⊥) :
-    span K (range (weight.toLinear K L M)) = ⊤ := by
+-- The reverse inclusion should also hold: TODO prove this!
+lemma LieModule.dualAnnihilator_ker_traceForm_le_span_weight [LieAlgebra.IsNilpotent K L]
+    [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L] :
+    (LinearMap.ker (traceForm K L M)).dualAnnihilator ≤ span K (range (weight.toLinear K L M)) := by
+  intro g hg
+  simp only [Submodule.mem_dualAnnihilator, LinearMap.mem_ker] at hg
   by_contra contra
   obtain ⟨f : Module.Dual K (Module.Dual K L), hf, hf'⟩ :=
-    Module.exists_dual_map_eq_bot_of_lt_top K (lt_top_iff_ne_top.mpr contra) inferInstance
+    Submodule.exists_dual_map_eq_bot_of_nmem contra inferInstance
   let x : L := (Module.evalEquiv K L).symm f
   replace hf' : ∀ χ ∈ weight K L M, χ x = 0 := by
     intro χ hχ
     change weight.toLinear K L M ⟨χ, hχ⟩ x = 0
     rw [Module.apply_evalEquiv_symm_apply, ← Submodule.mem_bot (R := K), ← hf', Submodule.mem_map]
     exact ⟨weight.toLinear K L M ⟨χ, hχ⟩, Submodule.subset_span (mem_range_self _), rfl⟩
-  have hx : x ≠ 0 := (LinearEquiv.map_ne_zero_iff _).mpr hf
-  apply hx
-  rw [← Submodule.mem_bot (R := K), ← h, LinearMap.mem_ker]
+  have hx : g x ≠ 0 := by simpa
+  refine hx (hg _ ?_)
   ext y
   rw [LieModule.traceForm_eq_sum_finrank_nsmul_mul, LinearMap.zero_apply]
   exact Finset.sum_eq_zero fun χ hχ ↦ by simp [hf' χ hχ]
 
 /-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular
 Killing form, the corresponding roots span the dual space of `H`. -/
+@[simp]
 lemma LieAlgebra.IsKilling.span_weight_eq_top [FiniteDimensional K L] [IsKilling K L]
     (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsTriangularizable K H L] :
     span K (range (weight.toLinear K H L)) = ⊤ := by
-  simp
+  simpa using LieModule.dualAnnihilator_ker_traceForm_le_span_weight K H L
 
 end Field

Mathlib/LinearAlgebra/Dual.lean

@@ -585,16 +585,6 @@ theorem nontrivial_dual_iff :
 instance instNontrivialDual [Nontrivial V] : Nontrivial (Dual K V) :=
   (nontrivial_dual_iff K).mpr inferInstance
 
-theorem exists_dual_map_eq_bot_of_lt_top {p : Submodule K V} (hp : p < ⊤) (hp' : Free K (V ⧸ p)) :
-    ∃ f : Dual K V, f ≠ 0 ∧ p.map f = ⊥ := by
-  obtain ⟨f, g, h⟩ : Nontrivial (Dual K <| V ⧸ p) :=
-    (nontrivial_dual_iff K).mpr <| Submodule.Quotient.nontrivial_of_lt_top p hp
-  refine ⟨(f - g).comp p.mkQ, ?_, by simp [Submodule.map_comp]⟩
-  replace h : f - g ≠ 0 := sub_ne_zero.mpr h
-  contrapose! h
-  refine Submodule.quot_hom_ext (f := f - g) (g := 0) fun v ↦ (?_ : (f - g).comp p.mkQ v = _)
-  simp [h]
-
 end
 
 theorem dual_rank_eq [Module.Finite K V] :
@@ -703,6 +693,27 @@ end IsReflexive
 
 end Module
 
+namespace Submodule
+
+open Module
+
+variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M}
+
+theorem exists_dual_map_eq_bot_of_nmem {x : M} (hx : x ∉ p) (hp' : Free R (M ⧸ p)) :
+    ∃ f : Dual R M, f x ≠ 0 ∧ p.map f = ⊥ := by
+  suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by
+    obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩
+  rwa [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply,
+    ← forall_dual_apply_eq_zero_iff (K := R), not_forall] at hx
+
+theorem exists_dual_map_eq_bot_of_lt_top (hp : p < ⊤) (hp' : Free R (M ⧸ p)) :
+    ∃ f : Dual R M, f ≠ 0 ∧ p.map f = ⊥ := by
+  obtain ⟨x, hx⟩ : ∃ x : M, x ∉ p := by rw [lt_top_iff_ne_top] at hp; contrapose! hp; ext; simp [hp]
+  obtain ⟨f, hf, hf'⟩ := p.exists_dual_map_eq_bot_of_nmem hx hp'
+  exact ⟨f, by aesop, hf'⟩
+
+end Submodule
+
 section DualBases
 
 open Module