Schur's lemma

We first prove the part of Schur's Lemma that holds in any preadditive category with kernels, that any nonzero morphism between simple objects is an isomorphism.

Second, we prove Schur's lemma for 𝕜-linear categories with finite dimensional hom spaces, over an algebraically closed field 𝕜: the hom space X ⟶ Y between simple objects X and Y is at most one dimensional, and is 1-dimensional iff X and Y are isomorphic.

theorem CategoryTheory.mono_of_nonzero_from_simple {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X : C} {Y : C} [CategoryTheory.Simple X] {f : X ⟶ Y} (w : f ≠ 0) : CategoryTheory.Mono f

theorem CategoryTheory.isIso_of_hom_simple {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X : C} {Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : CategoryTheory.IsIso f

The part of Schur's lemma that holds in any preadditive category with kernels: that a nonzero morphism between simple objects is an isomorphism.

theorem CategoryTheory.isIso_iff_nonzero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X : C} {Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ f ≠ 0

As a corollary of Schur's lemma for preadditive categories, any morphism between simple objects is (exclusively) either an isomorphism or zero.

noncomputable instance CategoryTheory.instDivisionRingEndOfHasKernelsOfSimple {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] : DivisionRing (CategoryTheory.End X)

In any preadditive category with kernels, the endomorphisms of a simple object form a division ring.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [DivisionRing 𝕜] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Linear 𝕜 C] {X : C} {Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (h : (X ≅ Y) → False) : FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 0

Part of Schur's lemma for 𝕜-linear categories: the hom space between two non-isomorphic simple objects is 0-dimensional.

theorem CategoryTheory.finrank_endomorphism_eq_one {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] {X : C} (isIso_iff_nonzero : ∀ (f : X ⟶ X), CategoryTheory.IsIso f ↔ f ≠ 0) [I : FiniteDimensional 𝕜 (X ⟶ X)] : FiniteDimensional.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.

theorem CategoryTheory.finrank_endomorphism_simple_eq_one {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] : FiniteDimensional.finrank 𝕜 (X ⟶ X) = 1

Schur's lemma for endomorphisms in 𝕜-linear categories.

theorem CategoryTheory.endomorphism_simple_eq_smul_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] (f : X ⟶ X) : ∃ (c : 𝕜), c • CategoryTheory.CategoryStruct.id X = f

noncomputable def CategoryTheory.fieldEndOfFiniteDimensional {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [I : FiniteDimensional 𝕜 (X ⟶ X)] : Field (CategoryTheory.End X)

Endomorphisms of a simple object form a field if they are finite dimensional. This can't be an instance as 𝕜 would be undetermined.

Equations

• CategoryTheory.fieldEndOfFiniteDimensional 𝕜 X = let __src := inferInstance; Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯

theorem CategoryTheory.finrank_hom_simple_simple_le_one {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) (Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : FiniteDimensional.finrank 𝕜 (X ⟶ Y) ≤ 1

Schur's lemma for 𝕜-linear categories: if hom spaces are finite dimensional, then the hom space between simples is at most 1-dimensional.

See finrank_hom_simple_simple_eq_one_iff and finrank_hom_simple_simple_eq_zero_iff below for the refinements when we know whether or not the simples are isomorphic.

theorem CategoryTheory.finrank_hom_simple_simple_eq_one_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) (Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)

theorem CategoryTheory.finrank_hom_simple_simple_eq_zero_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) (Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)

theorem CategoryTheory.finrank_hom_simple_simple {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) (Y : C) [∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : FiniteDimensional.finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0