chore(Algebra/Lie): rename weightSpace to genWeightspace (#15911)

There are two variants of the concept of weight space,
similar to the two concepts of eigenspace and generalized eigenspace.
This PR renames `weightSpace` to `genWeightSpace`
so that the name `weightSpace` can be reused for the
version of weight spaces using non-generalized eigenspaces.

Moves:
- coe_lie_shiftedWeightSpace_apply -> coe_lie_shiftedgenWeightSpace_apply
- coe_weightSpaceOf_zero -> coe_genWeightSpaceOf_zero
- coe_weightSpace_of_top -> coe_genWeightSpace_of_top
- comap_weightSpace_eq_of_injective -> comap_genWeightSpace_eq_of_injective
- disjoint_weightSpace -> disjoint_genWeightSpace
- disjoint_weightSpaceOf -> disjoint_genWeightSpaceOf
- eq_zero_of_mem_weightSpace_mem_posFitting -> eq_zero_of_mem_genWeightSpace_mem_posFitting
- eventually_weightSpace_smul_add_eq_bot -> eventually_genWeightSpace_smul_add_eq_bot
- exists_weightSpace_le_ker_of_isNoetherian -> exists_genWeightSpace_le_ker_of_isNoetherian
- exists_weightSpace_smul_add_eq_bot -> exists_genWeightSpace_smul_add_eq_bot
- exists_weightSpace_zero_le_ker_of_isNoetherian -> exists_genWeightSpace_zero_le_ker_of_isNoetherian
- exists₂_weightSpace_smul_add_eq_bot -> exists₂_genWeightSpace_smul_add_eq_bot
- finite_weightSpaceOf_ne_bot -> finite_genWeightSpaceOf_ne_bot
- finite_weightSpace_ne_bot -> finite_genWeightSpace_ne_bot
- iSup_ucs_eq_weightSpace_zero -> iSup_ucs_eq_genWeightSpace_zero
- iSup_ucs_le_weightSpace_zero -> iSup_ucs_le_genWeightSpace_zero
- iSup_weightSpaceOf_eq_top -> iSup_genWeightSpaceOf_eq_top
- iSup_weightSpace_eq_top -> iSup_genWeightSpace_eq_top
- iSup_weightSpace_eq_top' -> iSup_genWeightSpace_eq_top'
- independent_weightSpace -> independent_genWeightSpace
- independent_weightSpace' -> independent_genWeightSpace'
- independent_weightSpaceOf -> independent_genWeightSpaceOf
- injOn_weightSpace -> injOn_genWeightSpace
- isCompl_weightSpaceOf_zero_posFittingCompOf -> isCompl_genWeightSpaceOf_zero_posFittingCompOf
- isCompl_weightSpace_zero_posFittingComp -> isCompl_genWeightSpace_zero_posFittingComp
- isNilpotent_toEnd_weightSpace_zero -> isNilpotent_toEnd_genWeightSpace_zero
- lie_mem_weightSpaceChain_of_weightSpace_eq_bot_left -> lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left
- lie_mem_weightSpaceChain_of_weightSpace_eq_bot_right -> lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right
- lie_mem_weightSpace_of_mem_weightSpace -> lie_mem_genWeightSpace_of_mem_genWeightSpace
- map_weightSpace_eq -> map_genWeightSpace_eq
- map_weightSpace_eq_of_injective -> map_genWeightSpace_eq_of_injective
- map_weightSpace_le -> map_genWeightSpace_le
- mapsTo_toEnd_weightSpace_add_of_mem_rootSpace -> mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace
- mem_weightSpace -> mem_genWeightSpace
- mem_weightSpaceOf -> mem_genWeightSpaceOf
- rootSpace_comap_eq_weightSpace -> rootSpace_comap_eq_genWeightSpace
- shiftedWeightSpace -> shiftedgenWeightSpace
- traceForm_eq_sum_weightSpaceOf -> traceForm_eq_sum_genWeightSpaceOf
- traceForm_weightSpace_eq -> traceForm_genWeightSpace_eq
- trace_comp_toEnd_weightSpace_eq -> trace_comp_toEnd_genWeightSpace_eq
- trace_toEnd_weightSpace -> trace_toEnd_genWeightSpace
- trace_toEnd_weightSpaceChain_eq_zero -> trace_toEnd_genWeightSpaceChain_eq_zero
- weightSpace -> genWeightSpace
- weightSpaceChain -> genWeightSpaceChain
- weightSpaceChain_def -> genWeightSpaceChain_def
- weightSpaceChain_def' -> genWeightSpaceChain_def'
- weightSpaceChain_neg -> genWeightSpaceChain_neg
- weightSpaceOf -> genWeightSpaceOf
- weightSpaceOf_ne_bot -> genWeightSpaceOf_ne_bot
- weightSpace_add_chainTop -> genWeightSpace_add_chainTop
- weightSpace_chainBotCoeff_sub_one_zsmul_sub -> genWeightSpace_chainBotCoeff_sub_one_zsmul_sub
- weightSpace_chainTopCoeff_add_one_nsmul_add -> genWeightSpace_chainTopCoeff_add_one_nsmul_add
- weightSpace_chainTopCoeff_add_one_zsmul_add -> genWeightSpace_chainTopCoeff_add_one_zsmul_add
- weightSpace_le_weightSpaceChain -> genWeightSpace_le_genWeightSpaceChain
- weightSpace_le_weightSpaceOf -> genWeightSpace_le_genWeightSpaceOf
- weightSpace_ne_bot -> genWeightSpace_ne_bot
- weightSpace_neg_add_chainBot -> genWeightSpace_neg_add_chainBot
- weightSpace_neg_zsmul_add_ne_bot -> genWeightSpace_neg_zsmul_add_ne_bot
- weightSpace_nsmul_add_ne_bot_of_le -> genWeightSpace_nsmul_add_ne_bot_of_le
- weightSpace_weightSpaceOf_map_incl -> genWeightSpace_genWeightSpaceOf_map_incl
- weightSpace_zero_normalizer_eq_self -> genWeightSpace_zero_normalizer_eq_self
- weightSpace_zsmul_add_ne_bot -> genWeightSpace_zsmul_add_ne_bot
- zero_lt_finrank_weightSpace -> zero_lt_finrank_genWeightSpace
- zero_weightSpace_eq_top_of_nilpotent -> zero_genWeightSpace_eq_top_of_nilpotent
- zero_weightSpace_eq_top_of_nilpotent' -> zero_genWeightSpace_eq_top_of_nilpotent'

Mathlib/Algebra/Lie/TraceForm.lean

@@ -103,22 +103,22 @@ lemma traceForm_lieInvariant : (traceForm R L M).lieInvariant L := by
   exact isNilpotent_toEnd_of_isNilpotent₂ R L M x y
 
 @[simp]
-lemma traceForm_weightSpace_eq [Module.Free R M]
+lemma traceForm_genWeightSpace_eq [Module.Free R M]
     [IsDomain R] [IsPrincipalIdealRing R]
     [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] [LinearWeights R L M] (χ : L → R) (x y : L) :
-    traceForm R L (weightSpace M χ) x y = finrank R (weightSpace M χ) • (χ x * χ y) := by
-  set d := finrank R (weightSpace M χ)
+    traceForm R L (genWeightSpace M χ) x y = finrank R (genWeightSpace M χ) • (χ x * χ y) := by
+  set d := finrank R (genWeightSpace M χ)
   have h₁ : χ y • d • χ x - χ y • χ x • (d : R) = 0 := by simp [mul_comm (χ x)]
   have h₂ : χ x • d • χ y = d • (χ x * χ y) := by
     simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)
-  have := traceForm_eq_zero_of_isNilpotent R L (shiftedWeightSpace R L M χ)
+  have := traceForm_eq_zero_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)
   replace this := LinearMap.congr_fun (LinearMap.congr_fun this x) y
   rwa [LinearMap.zero_apply, LinearMap.zero_apply, traceForm_apply_apply,
-    shiftedWeightSpace.toEnd_eq, shiftedWeightSpace.toEnd_eq,
+    shiftedGenWeightSpace.toEnd_eq, shiftedGenWeightSpace.toEnd_eq,
     ← LinearEquiv.conj_comp, LinearMap.trace_conj', LinearMap.comp_sub, LinearMap.sub_comp,
     LinearMap.sub_comp, map_sub, map_sub, map_sub, LinearMap.comp_smul, LinearMap.smul_comp,
     LinearMap.comp_id, LinearMap.id_comp, LinearMap.map_smul, LinearMap.map_smul,
-    trace_toEnd_weightSpace, trace_toEnd_weightSpace,
+    trace_toEnd_genWeightSpace, trace_toEnd_genWeightSpace,
     LinearMap.comp_smul, LinearMap.smul_comp, LinearMap.id_comp, map_smul, map_smul,
     LinearMap.trace_id, ← traceForm_apply_apply, h₁, h₂, sub_zero, sub_eq_zero] at this
 
@@ -159,9 +159,9 @@ lemma traceForm_apply_eq_zero_of_mem_lcs_of_mem_center {x y : L}
 /-- Given a bilinear form `B` on a representation `M` of a nilpotent Lie algebra `L`, if `B` is
 invariant (in the sense that the action of `L` is skew-adjoint wrt `B`) then components of the
 Fitting decomposition of `M` are orthogonal wrt `B`. -/
-lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
+lemma eq_zero_of_mem_genWeightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
     {B : LinearMap.BilinForm R M} (hB : ∀ (x : L) (m n : M), B ⁅x, m⁆ n = - B m ⁅x, n⁆)
-    {m₀ m₁ : M} (hm₀ : m₀ ∈ weightSpace M (0 : L → R)) (hm₁ : m₁ ∈ posFittingComp R L M) :
+    {m₀ m₁ : M} (hm₀ : m₀ ∈ genWeightSpace M (0 : L → R)) (hm₁ : m₁ ∈ posFittingComp R L M) :
     B m₀ m₁ = 0 := by
   replace hB : ∀ x (k : ℕ) m n, B m ((φ x ^ k) n) = (- 1 : R) ^ k • B ((φ x ^ k) m) n := by
     intro x k
@@ -177,7 +177,7 @@ lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
     apply LieSubmodule.iSup_induction _ hm₁ this (map_zero _)
     aesop
   clear hm₁ m₁; intro x m₁ hm₁
-  simp only [mem_weightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm₀
+  simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm₀
   obtain ⟨k, hk⟩ := hm₀ x
   obtain ⟨m, rfl⟩ := (mem_posFittingCompOf R x m₁).mp hm₁ k
   simp [hB, hk]
@@ -211,20 +211,21 @@ open TensorProduct
 
 variable [LieAlgebra.IsNilpotent R L] [IsDomain R] [IsPrincipalIdealRing R]
 
-lemma traceForm_eq_sum_weightSpaceOf
+lemma traceForm_eq_sum_genWeightSpaceOf
     [NoZeroSMulDivisors R M] [IsNoetherian R M] [IsTriangularizable R L M] (z : L) :
     traceForm R L M =
-    ∑ χ ∈ (finite_weightSpaceOf_ne_bot R L M z).toFinset, traceForm R L (weightSpaceOf M χ z) := by
+    ∑ χ ∈ (finite_genWeightSpaceOf_ne_bot R L M z).toFinset,
+      traceForm R L (genWeightSpaceOf M χ z) := by
   ext x y
   have hxy : ∀ χ : R, MapsTo ((toEnd R L M x).comp (toEnd R L M y))
-      (weightSpaceOf M χ z) (weightSpaceOf M χ z) :=
+      (genWeightSpaceOf M χ z) (genWeightSpaceOf M χ z) :=
     fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
-  have hfin : {χ : R | (weightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite := by
-    convert finite_weightSpaceOf_ne_bot R L M z
-    exact LieSubmodule.coeSubmodule_eq_bot_iff (weightSpaceOf M _ _)
+  have hfin : {χ : R | (genWeightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite := by
+    convert finite_genWeightSpaceOf_ne_bot R L M z
+    exact LieSubmodule.coeSubmodule_eq_bot_iff (genWeightSpaceOf M _ _)
   classical
   have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
-    (LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_weightSpaceOf R L M z)
+    (LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_genWeightSpaceOf R L M z)
     (IsTriangularizable.iSup_eq_top z)
   simp only [LinearMap.coeFn_sum, Finset.sum_apply, traceForm_apply_apply,
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
@@ -275,7 +276,7 @@ lemma lowerCentralSeries_one_inf_center_le_ker_traceForm [Module.Free R M] [Modu
   apply LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
   · exact IsTriangularizable.iSup_eq_top (1 ⊗ₜ[R] x)
   · exact fun μ ↦ trace_toEnd_eq_zero_of_mem_lcs A (A ⊗[R] L)
-      (weightSpaceOf (A ⊗[R] M) μ (1 ⊗ₜ x)) (le_refl 1) hz
+      (genWeightSpaceOf (A ⊗[R] M) μ (1 ⊗ₜ x)) (le_refl 1) hz
   · exact commute_toEnd_of_mem_center_right (A ⊗[R] M) hzc (1 ⊗ₜ x)
 
 /-- A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian. -/
@@ -342,7 +343,7 @@ lemma killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting
     (hx₀ : x₀ ∈ LieAlgebra.zeroRootSubalgebra R L H)
     (hx₁ : x₁ ∈ LieModule.posFittingComp R H L) :
     killingForm R L x₀ x₁ = 0 :=
-  LieModule.eq_zero_of_mem_weightSpace_mem_posFitting R H L
+  LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting R H L
     (fun x y z ↦ LieModule.traceForm_apply_lie_apply' R L L x y z) hx₀ hx₁
 
 namespace LieIdeal
@@ -395,20 +396,20 @@ variable [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimens
 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 = ∑ χ : Weight K L M, finrank K (weightSpace M χ) • (χ x * χ y) := by
+    traceForm K L M x y = ∑ χ : Weight K L M, finrank K (genWeightSpace M χ) • (χ x * χ y) := by
   have hxy : ∀ χ : Weight K L M, MapsTo (toEnd K L M x ∘ₗ toEnd K L M y)
-      (weightSpace M χ) (weightSpace M χ) :=
+      (genWeightSpace M χ) (genWeightSpace M χ) :=
     fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
   classical
   have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
-    (LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_weightSpace' K L M)
-    (LieSubmodule.iSup_eq_top_iff_coe_toSubmodule.mp <| iSup_weightSpace_eq_top' K L M)
+    (LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_genWeightSpace' K L M)
+    (LieSubmodule.iSup_eq_top_iff_coe_toSubmodule.mp <| iSup_genWeightSpace_eq_top' K L M)
   simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
-    ← traceForm_weightSpace_eq K L M _ x y]
+    ← traceForm_genWeightSpace_eq K L M _ x y]
   rfl
 
 lemma traceForm_eq_sum_finrank_nsmul :
-    traceForm K L M = ∑ χ : Weight K L M, finrank K (weightSpace M χ) •
+    traceForm K L M = ∑ χ : Weight K L M, finrank K (genWeightSpace M χ) •
       (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) := by
   ext
   rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach]