feat: add lemma `LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem…

…_rootSpaceProductNegSelf` (leanprover-community#10803)

Mathlib/Algebra/Lie/Killing.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Lie.Nilpotent
 import Mathlib.Algebra.Lie.Semisimple
 import Mathlib.Algebra.Lie.Weights.Cartan
+import Mathlib.Algebra.Lie.Weights.Chain
 import Mathlib.Algebra.Lie.Weights.Linear
 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.LinearAlgebra.PID
@@ -502,14 +503,65 @@ lemma range_traceForm_le_span_weight :
 
 end LieModule
 
+namespace LieAlgebra.IsKilling
+
+variable [FiniteDimensional K L] [IsKilling K L]
+  (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsTriangularizable K H L]
+
 /-- 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] :
+lemma span_weight_eq_top :
     span K (range (weight.toLinear K H L)) = ⊤ := by
   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]
 
+@[simp]
+lemma iInf_ker_weight_eq_bot :
+    ⨅ α : weight K H L, LinearMap.ker (weight.toLinear K H L α) = ⊥ := by
+  rw [← Subspace.dualAnnihilator_inj, Subspace.dualAnnihilator_iInf_eq,
+    Submodule.dualAnnihilator_bot]
+  simp [← LinearMap.range_dualMap_eq_dualAnnihilator_ker, ← Submodule.span_range_eq_iSup]
+
+@[simp]
+lemma rootSpaceProductNegSelf_zero_eq_bot :
+    (rootSpaceProductNegSelf (0 : H → K)).range = ⊥ := by
+  refine eq_bot_iff.mpr fun x hx ↦ ?_
+  suffices {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0} by
+    rw [LieSubmodule.mem_bot]
+    simpa [-LieModuleHom.mem_range, this, mem_range_rootSpaceProductNegSelf] using hx
+  refine eq_singleton_iff_unique_mem.mpr ⟨⟨0, H.zero_mem, 0, H.zero_mem, zero_lie 0⟩, ?_⟩
+  rintro - ⟨y, hy, z, hz, rfl⟩
+  suffices ⁅(⟨y, hy⟩ : H), (⟨z, hz⟩ : H)⁆ = 0 by
+    simpa only [Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero] using this
+  simp
+
+variable {K H L}
+
+/-- The contrapositive of this result is very useful, taking `x` to be the element of `H`
+corresponding to a root `α` under the identification between `H` and `H^*` provided by the Killing
+form. -/
+lemma eq_zero_of_apply_eq_zero_of_mem_rootSpaceProductNegSelf [CharZero K]
+    (x : H) (α : H → K) (hαx : α x = 0) (hx : x ∈ (rootSpaceProductNegSelf α).range) :
+    x = 0 := by
+  rcases eq_or_ne α 0 with rfl | hα; · simpa using hx
+  replace hx : x ∈ ⨅ β : weight K H L, LinearMap.ker (weight.toLinear K H L β) := by
+    simp only [Submodule.mem_iInf, Subtype.forall, Finite.mem_toFinset]
+    intro β hβ
+    obtain ⟨a, b, hb, hab⟩ := exists_forall_mem_rootSpaceProductNegSelf_smul_add_eq_zero L α β hα hβ
+    simpa [hαx, hb.ne'] using hab _ hx
+  simpa using hx
+
+-- When `α ≠ 0`, this can be upgraded to `IsCompl`; moreover these complements are orthogonal with
+-- respect to the Killing form. TODO prove this!
+lemma ker_weight_inf_rootSpaceProductNegSelf_eq_bot [CharZero K] (α : weight K H L) :
+    LinearMap.ker (weight.toLinear K H L α) ⊓ (rootSpaceProductNegSelf (α : H → K)).range = ⊥ := by
+  rw [LieIdeal.coe_to_lieSubalgebra_to_submodule, LieModuleHom.coeSubmodule_range]
+  refine (Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_
+  replace hαx : (α : H → K) x = 0 := by simpa using hαx
+  exact eq_zero_of_apply_eq_zero_of_mem_rootSpaceProductNegSelf x α hαx hx
+
+end LieAlgebra.IsKilling
+
 end Field

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -5,10 +5,8 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Ring.Divisibility.Lemmas
 import Mathlib.Algebra.Lie.Nilpotent
-import Mathlib.Algebra.Lie.TensorProduct
 import Mathlib.Algebra.Lie.Engel
 import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
-import Mathlib.LinearAlgebra.TensorProduct.Tower
 import Mathlib.RingTheory.Artinian
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.LinearAlgebra.FreeModule.PID

Mathlib/LinearAlgebra/Dual.lean

@@ -197,6 +197,8 @@ def LinearMap.dualMap (f : M₁ →ₗ[R] M₂) : Dual R M₂ →ₗ[R] Dual R M
   Module.Dual.transpose (R := R) f
 #align linear_map.dual_map LinearMap.dualMap
 
+lemma LinearMap.dualMap_eq_lcomp (f : M₁ →ₗ[R] M₂) : f.dualMap = f.lcomp R := rfl
+
 -- Porting note: with reducible def need to specify some parameters to transpose explicitly
 theorem LinearMap.dualMap_def (f : M₁ →ₗ[R] M₂) : f.dualMap = Module.Dual.transpose (R := R) f :=
   rfl
@@ -264,6 +266,21 @@ theorem LinearEquiv.dualMap_trans {M₃ : Type*} [AddCommGroup M₃] [Module R M
   rfl
 #align linear_equiv.dual_map_trans LinearEquiv.dualMap_trans
 
+@[simp]
+lemma Dual.apply_one_mul_eq (f : Dual R R) (r : R) :
+    f 1 * r = f r := by
+  conv_rhs => rw [← mul_one r, ← smul_eq_mul]
+  rw [map_smul, smul_eq_mul, mul_comm]
+
+@[simp]
+lemma LinearMap.range_dualMap_dual_eq_span_singleton (f : Dual R M₁) :
+    range f.dualMap = R ∙ f := by
+  ext m
+  rw [Submodule.mem_span_singleton]
+  refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
+  · ext; simp [dualMap_apply', ← hr]
+  · ext; simp [dualMap_apply', ← hr]
+
 end DualMap
 
 namespace Basis