Endomorphisms of a simple object are scalars #

Let k be an algebraically closed field and X a simple object of a k-linear preadditive category with kernels, whose endomorphisms form a finite-dimensional k-vector space. Schur's lemma (CategoryTheory.endomorphism_simple_eq_smul_id) says that every endomorphism of X is a scalar multiple c • 𝟙 X of the identity. We package this as a k-algebra isomorphism TauCeti.endAlgEquivOfSimple k X : End X ≃ₐ[k] k, the inverse of the structure map algebraMap k (End X), which sends c to c • 𝟙 X.

Applied to a simple monoidal unit, this identifies the scalars 𝟙_ C ⟶ 𝟙_ C of a fusion category with elements of k, which is how traces and dimensions are read as numbers.

The finite-dimensionality assumption cannot be dropped: finite-dimensional vector spaces over the rational function field k(t), viewed as a k-linear category, have a simple unit whose endomorphism algebra is k(t).

Main declarations #

TauCeti.endAlgEquivOfSimple: the isomorphism End X ≃ₐ[k] k, whose inverse is algebraMap k (End X) by TauCeti.endAlgEquivOfSimple_symm_apply;
TauCeti.endAlgEquivOfSimple_smul_id: every endomorphism f is endAlgEquivOfSimple k X f times the identity, and TauCeti.endAlgEquivOfSimple_apply_eq_iff characterizes the scalar;
CategoryTheory.End.of_id, CategoryTheory.End.of_comp, … of TauCeti.CategoryTheory.Linear.Endomorphism are simp lemmas pushing End.of inside expressions built from morphisms f : X ⟶ X, after which map_mul, map_add, … let simp compute scalars of composites, sums and multiples;
TauCeti.homPairing: the composition pairing (S ⟶ X) × (X ⟶ S) → k of a simple object S, with f ≫ g = homPairing k S X f g • 𝟙 S by TauCeti.homPairing_smul_id.

References #

[P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], for Schur's lemma

source

theorem TauCeti.bijective_algebraMap_end_of_simple (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] :

Function.Bijective ⇑(algebraMap k (CategoryTheory.End X))

The structure map k → End X of a simple object X with finite-dimensional endomorphisms over an algebraically closed field is bijective: this is Schur's lemma.

source

noncomputable def TauCeti.endAlgEquivOfSimple (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] :

CategoryTheory.End X ≃ₐ[k] k

Schur's lemma as an identification of algebras: the endomorphisms of a simple object X with finite-dimensional endomorphisms over an algebraically closed field k are the scalars k. This is the inverse of the structure map algebraMap k (End X), c ↦ c • 𝟙 X.

Instances For

source

@[simp]

theorem TauCeti.endAlgEquivOfSimple_symm_apply {k : Type w} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (c : k) :

(endAlgEquivOfSimple k X).symm c = (algebraMap k (CategoryTheory.End X)) c

The inverse of endAlgEquivOfSimple is the structure map algebraMap k (End X).

source

@[simp]

theorem TauCeti.endAlgEquivOfSimple_smul_id {k : Type w} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (f : CategoryTheory.End X) :

(endAlgEquivOfSimple k X) f • CategoryTheory.CategoryStruct.id X = f.asHom

Every endomorphism of a simple object is its scalar times the identity.

source

theorem TauCeti.endAlgEquivOfSimple_apply_eq_iff {k : Type w} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (f : CategoryTheory.End X) (c : k) :

(endAlgEquivOfSimple k X) f = c ↔ f.asHom = c • CategoryTheory.CategoryStruct.id X

The scalar of an endomorphism f is the unique c with f = c • 𝟙 X.

source

noncomputable def TauCeti.homPairing (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasKernels C] (S X : C) [CategoryTheory.Simple S] [FiniteDimensional k (S ⟶ S)] :

(S ⟶ X) →ₗ[k] (X ⟶ S) →ₗ[k] k

The composition pairing between morphisms out of and into a simple object S: the scalar homPairing k S X f g is the one with f ≫ g = homPairing k S X f g • 𝟙 S, which exists by Schur's lemma.

Instances For

source