English
If A is a nontrivial finite-dimensional algebra over an algebraically closed field 𝕜, then every element a ∈ A has nonempty spectrum: σ(a) ≠ ∅.
Русский
Если A — ненулёная конечномерная алгебра над алгебраически замкнутым полем 𝕜, то у каждого элемента a ∈ A спектр σ(a) непуст: σ(a) ≠ ∅.
LaTeX
$$$$ (\\sigma a) \\neq \\varnothing. $$$$
Lean4
/-- Every element `a` in a nontrivial finite-dimensional algebra `A`
over an algebraically closed field `𝕜` has non-empty spectrum. -/
theorem nonempty_of_isAlgClosed_of_finiteDimensional [IsAlgClosed 𝕜] [Nontrivial A] [I : FiniteDimensional 𝕜 A]
(a : A) : (σ a).Nonempty :=
by
obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p; rw [h_eval_p]; simp
rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu
obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu
exact ⟨k, hk⟩
