English
The following four statements are equivalent: φ is nilpotent; charpoly φ = X^finrank; every vector is annihilated by some power of φ; natTrailingDegree φ.charpoly = finrank.
Русский
Следующие четыре утверждения эквивалентны: φ нильпотентно; charpoly φ = X^finrank; для каждого вектора найдётся степень φ, которая его аннигилирует; natTrailingDegree φ.charpoly = finrank.
LaTeX
$$List.TFAE [IsNilpotent φ, φ.charpoly = X ^ finrank R M, ∀ m : M, ∃ n, (φ ^ n) m = 0, natTrailingDegree φ.charpoly = finrank R M]$$
Lean4
theorem charpoly_nilpotent_tfae [IsNoetherian R M] (φ : Module.End R M) :
List.TFAE
[IsNilpotent φ, φ.charpoly = X ^ finrank R M, ∀ m : M, ∃ (n : ℕ), (φ ^ n) m = 0,
natTrailingDegree φ.charpoly = finrank R M] :=
by
tfae_have 1 → 2 := IsNilpotent.charpoly_eq_X_pow_finrank
tfae_have 2 → 3
| h, m => by
use finrank R M
suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly
tfae_have 3 → 1
| h => by
obtain ⟨n, hn⟩ := Filter.eventually_atTop.mp <| φ.eventually_iSup_ker_pow_eq
use n
ext x
rw [zero_apply, ← mem_ker, ← hn n le_rfl]
obtain ⟨k, hk⟩ := h x
rw [← mem_ker] at hk
exact Submodule.mem_iSup_of_mem _ hk
tfae_have 2 ↔ 4 := by rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
tfae_finish
