English
Schur’s lemma specialized: the endomorphism algebra of a simple object X which is finite-dimensional over 𝕜 is a one-dimensional division algebra; hence End(X) is a field.
Русский
Специально сформулированная лемма Шура: эндоморфизм‑алгебра простого объекта X, конечномерная над 𝕜, образует делительную алгебру размерности 1; значит End(X) — поле.
LaTeX
$$$\mathrm{End}(X) \text{ is a field}$$$
Lean4
/-- Endomorphisms of a simple object form a field if they are finite dimensional.
This can't be an instance as `𝕜` would be undetermined.
-/
noncomputable def fieldEndOfFiniteDimensional (X : C) [Simple X] [I : FiniteDimensional 𝕜 (X ⟶ X)] : Field (End X) := by
classical
exact
{ (inferInstance : DivisionRing (End X)) with
mul_comm := fun f g => by
obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
simp [← mul_smul, mul_comm c d] }
-- There is a symmetric argument that uses `[FiniteDimensional 𝕜 (Y ⟶ Y)]` instead,
-- but we don't bother proving that here.
