From 57ca123151b29b04281afbcb84d51d845b62ae22 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Fri, 5 Jan 2024 11:32:30 +0000 Subject: [PATCH] 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 --- Mathlib/Algebra/Lie/Killing.lean | 49 +++++++++++++++++--------------- Mathlib/LinearAlgebra/Dual.lean | 16 +++++++++++ 2 files changed, 42 insertions(+), 23 deletions(-) diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean index b735f497dc472..e1fbb04f34613 100644 --- a/Mathlib/Algebra/Lie/Killing.lean +++ b/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,26 +495,24 @@ 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`. -/ @@ -519,6 +520,8 @@ Killing form, the corresponding roots span the dual space of `H`. -/ 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 diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 0753e9517e6c9..b83dcc91a128d 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/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