English
If m lies in a generalized eigen-space of f, and f and g commute with g semisimple and f−g nilpotent, then g acts as μ on m.
Русский
Если m лежит в обобщенном собственном пространстве f, и g коммутирует с f, при этом g полная полусемисимпер, а f−g нильпотент, тогда g действует как μ на m.
LaTeX
$$$$ f.HasEigenvector(\mu) \Rightarrow g m = \mu m \quad \text{under } [f,g]=0,\ g\text{ semisimple},\ (f-g) \text{ nilpotent}. $$$$
Lean4
theorem apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil {μ : R} {k : ℕ∞} {m : M} (hm : m ∈ f.genEigenspace μ k)
(hfg : Commute f g) (hss : g.IsFinitelySemisimple) (hnil : IsNilpotent (f - g)) : g m = μ • m :=
by
rw [f.mem_genEigenspace] at hm
obtain ⟨l, -, hm⟩ := hm
rw [← f.mem_genEigenspace_nat] at hm
set p := f.genEigenspace μ l
have h₁ : MapsTo g p p := mapsTo_genEigenspace_of_comm hfg μ l
have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p :=
mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l
have h₃ : MapsTo (f - g) p p := mapsTo_genEigenspace_of_comm (Commute.sub_right rfl hfg) μ l
have h₄ : MapsTo (f - algebraMap R (End R M) μ) p p :=
mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ l
replace hfg : Commute (f - algebraMap R (End R M) μ) (f - g) :=
(Commute.sub_right rfl hfg).sub_left <| Algebra.commute_algebraMap_left μ (f - g)
suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂)
by
replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩
simpa [LinearMap.restrict_sub h₄ h₃] using
(LinearMap.restrict_commute hfg h₄ h₃).isNilpotent_sub (f.isNilpotent_restrict_sub_algebraMap μ l)
(Module.End.isNilpotent.restrict h₃ hnil)
