English
If f is nilpotent and IsFinitelySemisimple, then f = 0.
Русский
Если f нильпотентен и является конечносемпсимым, то f = 0.
LaTeX
$$$ IsNilpotent(f) \land IsFinitelySemisimple(f) \Rightarrow f = 0$$$
Lean4
theorem eq_zero_of_isNilpotent_of_isFinitelySemisimple (hn : IsNilpotent f) (hs : IsFinitelySemisimple f) : f = 0 :=
by
have (p) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite R p) : f.restrict hp₁ = 0 :=
by
specialize hs p hp₁ hp₂
replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
exact eq_zero_of_isNilpotent_isSemisimple hn hs
ext x
obtain ⟨k : ℕ, hk : f ^ k = 0⟩ := hn
let p := Submodule.span R {(f ^ i) x | (i : ℕ) (_ : i ≤ k)}
have hp₁ : p ∈ f.invtSubmodule :=
by
simp only [mem_invtSubmodule, p, Submodule.span_le]
rintro - ⟨i, hi, rfl⟩
apply Submodule.subset_span
rcases lt_or_eq_of_le hi with hik | rfl
· exact ⟨i + 1, hik, by simpa [Module.End.pow_apply] using iterate_succ_apply' f i x⟩
· exact ⟨i, by simp [hk]⟩
have hp₂ : Module.Finite R p := by
let g : ℕ → M := fun i ↦ (f ^ i) x
have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)
simpa [LinearMap.restrict_apply, Subtype.ext_iff] using
LinearMap.congr_fun (this p hp₁ hp₂) ⟨x, Submodule.subset_span ⟨0, k.zero_le, rfl⟩⟩
