English
In a Noetherian setting, there exists k such that genWeightSpace M (0) ≤ ker (toEnd x)^k.
Русский
При условиях Ноetherian существует k, такое что genWeightSpace M (0) ⊆ ker (toEnd x)^k.
LaTeX
$$∃ k : ℕ, genWeightSpace M (0 : L → R) ≤ ker (toEnd R L M x ^ k)$$
Lean4
/-- If `M` is a representation of a nilpotent Lie algebra `L`, and `x : L`, then
`posFittingCompOf R M x` is the infimum of the decreasing system
`range φₓ ⊇ range φₓ² ⊇ range φₓ³ ⊇ ⋯` where `φₓ : End R M := toEnd R L M x`. We call this
the "positive Fitting component" because with appropriate assumptions (e.g., `R` is a field and
`M` is finite-dimensional) `φₓ` induces the so-called Fitting decomposition: `M = M₀ ⊕ M₁` where
`M₀ = genWeightSpaceOf M 0 x` and `M₁ = posFittingCompOf R M x`.
It is a Lie submodule because `L` is nilpotent. -/
def posFittingCompOf (x : L) : LieSubmodule R L M :=
{ toSubmodule := ⨅ k, LinearMap.range (toEnd R L M x ^ k)
lie_mem := by
set φ := toEnd R L M x
intro y m hm
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
Submodule.mem_iInf, LinearMap.mem_range] at hm ⊢
intro k
obtain ⟨N, hN⟩ := LieAlgebra.nilpotent_ad_of_nilpotent_algebra R L
obtain ⟨m, rfl⟩ := hm (N + k)
let f₁ : Module.End R (L ⊗[R] M) := (LieAlgebra.ad R L x).rTensor M
let f₂ : Module.End R (L ⊗[R] M) := φ.lTensor L
replace hN : f₁ ^ N = 0 := by ext; simp [f₁, hN]
have h₁ : Commute f₁ f₂ := by ext; simp [f₁, f₂]
have h₂ : φ ∘ₗ toModuleHom R L M = toModuleHom R L M ∘ₗ (f₁ + f₂) := by ext; simp [φ, f₁, f₂]
obtain ⟨q, hq⟩ := h₁.add_pow_dvd_pow_of_pow_eq_zero_right (N + k).le_succ hN
use toModuleHom R L M (q (y ⊗ₜ m))
change (φ ^ k).comp ((toModuleHom R L M : L ⊗[R] M →ₗ[R] M)) _ = _
simp [φ, f₁, f₂, Module.End.commute_pow_left_of_commute h₂, LinearMap.comp_apply (g := (f₁ + f₂) ^ k),
← LinearMap.comp_apply (g := q), ← Module.End.mul_eq_comp, ← hq] }
