finrank_hom_simple_simple_eq_zero_of_not_iso

English

Under Schur-type hypotheses, the endomorphism algebra End(X) of a simple object X which is finite-dimensional over 𝕜 is a field (hence a division algebra).

Русский

При условиях Шура-подобного типа, алгебра эндоморфизмов End(X) простого объекта X является полем (то есть делением алгебры).

LaTeX

$$$End(X) \text{ is a field}$$$

Lean4

/-- Part of **Schur's lemma** for `𝕜`-linear categories:
the hom space between two non-isomorphic simple objects is 0-dimensional.
-/
theorem finrank_hom_simple_simple_eq_zero_of_not_iso [HasKernels C] [Linear 𝕜 C] {X Y : C} [Simple X] [Simple Y]
    (h : (X ≅ Y) → False) : finrank 𝕜 (X ⟶ Y) = 0 :=
  haveI :=
    subsingleton_of_forall_eq (0 : X ⟶ Y) fun f =>
      by
      have p := not_congr (isIso_iff_nonzero f)
      simp only [Classical.not_not, Ne] at p
      exact p.mp fun _ => h (asIso f)
  finrank_zero_of_subsingleton

Похожие утверждения