Theorems · Theorem · category theory

CategoryTheory.finrank_endomorphism_eq_one

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] {X : C},
  (∀ (f : X ⟶ X), CategoryTheory.IsIso f ↔ f ≠ 0) → ∀ [I : FiniteDimensional 𝕜 (X ⟶ X)], Module.finrank 𝕜 (X ⟶ X) = 1

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.

Defined in

Mathlib.CategoryTheory.Preadditive.Schur

Cited by

1 results in Mathlib

Foundations

Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveFieldIsAlgClosedCategoryTheory.LinearFiniteDimensional