English
If X is simple and End(X) is finite-dimensional, then End(X) is a 1-dimensional algebra over 𝕜; in particular, nonzero endomorphisms are scalar multiples of the identity.
Русский
Пусть X простый, и End(X) конечномерно над 𝕜. Тогда End(X) одномерно над 𝕜; следовательно, любой небезусловно нулевой эндоморфизм является скалярным кратным единице.
LaTeX
$$$\dim_{\mathbb{k}}(\mathrm{End}(X))=1$$$
Lean4
/-- An auxiliary lemma for Schur's lemma.
If `X ⟶ X` is finite dimensional, and every nonzero endomorphism is invertible,
then `X ⟶ X` is 1-dimensional.
-/
theorem finrank_endomorphism_eq_one {X : C} (isIso_iff_nonzero : ∀ f : X ⟶ X, IsIso f ↔ f ≠ 0)
[I : FiniteDimensional 𝕜 (X ⟶ X)] : finrank 𝕜 (X ⟶ X) = 1 :=
by
have id_nonzero := (isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)
refine finrank_eq_one (𝟙 X) id_nonzero ?_
intro f
have : Nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero
have : FiniteDimensional 𝕜 (End X) := I
obtain ⟨c, nu⟩ := spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 𝕜 (End.of f)
use c
rw [spectrum.mem_iff, IsUnit.sub_iff, isUnit_iff_isIso, isIso_iff_nonzero, Ne, Classical.not_not, sub_eq_zero,
Algebra.algebraMap_eq_smul_one] at nu
exact nu.symm
