feat: refactor lemma `LieModule.dualAnnihilator_ker_traceForm_le_span…

…_weight` (#9047)

Also add some API for related results such as `LinearMap.dualCoannihilator_range_eq_ker_flip`, which is not needed here but worth having.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Algebra/Lie/Killing.lean

@@ -473,10 +473,13 @@ end LieAlgebra
 section Field
 
 open LieModule FiniteDimensional
-open Submodule (span)
+open Submodule (span subset_span)
 
-lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L]
-    [LinearWeights K L M] [IsTriangularizable K L M] (x y : L) :
+namespace LieModule
+
+variable [LieAlgebra.IsNilpotent K L] [LinearWeights K L M] [IsTriangularizable K L M]
+
+lemma traceForm_eq_sum_finrank_nsmul_mul (x y : L) :
     traceForm K L M x y = ∑ χ in weight K L M, finrank K (weightSpace M χ) • (χ x * χ y) := by
   have hxy : ∀ χ : L → K, MapsTo (toEndomorphism K L M x ∘ₗ toEndomorphism K L M y)
       (weightSpace M χ) (weightSpace M χ) :=
@@ -492,33 +495,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)
 
+lemma traceForm_eq_sum_finrank_nsmul :
+    traceForm K L M = ∑ χ : weight K L M, finrank K (weightSpace M (χ : L → K)) •
+      (weight.toLinear K L M χ).smulRight (weight.toLinear K L M χ) := by
+  ext
+  rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach]
+  simp
+
 -- 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'⟩ :=
-    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 : 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χ]
+lemma range_traceForm_le_span_weight :
+    LinearMap.range (traceForm K L M) ≤ span K (range (weight.toLinear K L M)) := by
+  rintro - ⟨x, rfl⟩
+  rw [LieModule.traceForm_eq_sum_finrank_nsmul, LinearMap.coeFn_sum, Finset.sum_apply]
+  refine Submodule.sum_mem _ fun χ _ ↦ ?_
+  simp_rw [LinearMap.smul_apply, LinearMap.coe_smulRight, weight.toLinear_apply,
+    nsmul_eq_smul_cast (R := K)]
+  exact Submodule.smul_mem _ _ <| Submodule.smul_mem _ _ <| subset_span <| mem_range_self χ
+
+end LieModule
 
 /-- 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
-  simpa using LieModule.dualAnnihilator_ker_traceForm_le_span_weight K H L
+  refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))
+  rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
+    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]
 
 end Field

Mathlib/LinearAlgebra/Dual.lean

@@ -912,6 +912,7 @@ def dualCoannihilator (Φ : Submodule R (Module.Dual R M)) : Submodule R M :=
   Φ.dualAnnihilator.comap (Module.Dual.eval R M)
 #align submodule.dual_coannihilator Submodule.dualCoannihilator
 
+@[simp]
 theorem mem_dualCoannihilator {Φ : Submodule R (Module.Dual R M)} (x : M) :
     x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, (φ x : R) = 0 := by
   simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]
@@ -1428,6 +1429,15 @@ theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M
     exact (ker_rangeRestrict f).symm
 #align linear_map.range_dual_map_eq_dual_annihilator_ker_of_subtype_range_surjective LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective
 
+theorem ker_dualMap_eq_dualCoannihilator_range (f : M →ₗ[R] M') :
+    LinearMap.ker f.dualMap = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator := by
+  ext x; simp [ext_iff (f := dualMap f x)]
+
+@[simp]
+lemma dualCoannihilator_range_eq_ker_flip (B : M →ₗ[R] M' →ₗ[R] R) :
+    (range B).dualCoannihilator = LinearMap.ker B.flip := by
+  ext x; simp [ext_iff (f := B.flip x)]
+
 end LinearMap
 
 end CommRing
@@ -1595,6 +1605,12 @@ theorem dualMap_bijective_iff {f : V₁ →ₗ[K] V₂} :
 
 variable {B : V₁ →ₗ[K] V₂ →ₗ[K] K}
 
+@[simp]
+lemma dualAnnihilator_ker_eq_range_flip [IsReflexive K V₂] :
+    (ker B).dualAnnihilator = range B.flip := by
+  change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap)
+  rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]
+
 open Function
 
 theorem flip_injective_iff₁ [FiniteDimensional K V₁] : Injective B.flip ↔ Surjective B := by