Traces of endomorphisms of simple objects #

Let C be a pivotal category which is k-linear, for an algebraically closed field k, with kernels. By Schur's lemma every endomorphism f of a simple object X with finite-dimensional endomorphisms is the scalar TauCeti.endAlgEquivOfSimple k X (End.of f) times 𝟙 X. Since the traces are k-linear, the trace of f is that scalar times the dimension of X:

leftTrace f = endAlgEquivOfSimple k X (End.of f) • leftDim X;
rightTrace f = endAlgEquivOfSimple k X (End.of f) • rightDim X;
trace f = endAlgEquivOfSimple k X (End.of f) • quantumDim X in a spherical category.

When the unit 𝟙_ C is itself simple with finite-dimensional endomorphisms, applying endAlgEquivOfSimple k (𝟙_ C) to these identities reads the traces as elements of k, by the simp lemmas for End.of of TauCeti.CategoryTheory.Linear.Endomorphism.

For an automorphism a of a simple object the scalars of a⁻¹ and a cancel, so leftTrace a⁻¹ ≫ rightTrace a = leftDim X ≫ rightDim X. Since changing the pivotal structure changes the left dimension of X into the left trace of an automorphism a⁻¹ and the right dimension into the right trace of a, the product leftDim X ≫ rightDim X of the two dimensions of a simple object does not depend on the pivotal structure, although each factor may.

When the unit is simple, every scalar 𝟙_ C ⟶ 𝟙_ C is a multiple of the identity, so it acts on every object in the same way from the left and from the right. Hence the left and right traces and dimensions are multiplicative on tensor products, as in a braided category (TauCeti.leftTrace_tensorHom_eq_comp_of_simple and its companions).

References #

[P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §§4.7, 7.21

source

theorem TauCeti.leftTrace_eq_smul_leftDim (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (f : X ⟶ X) :

leftTrace f = (endAlgEquivOfSimple k X) { asHom := f } • leftDim X

The left trace of an endomorphism of a simple object is its scalar times the left dimension.

source

theorem TauCeti.rightTrace_eq_smul_rightDim (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (f : X ⟶ X) :

rightTrace f = (endAlgEquivOfSimple k X) { asHom := f } • rightDim X

The right trace of an endomorphism of a simple object is its scalar times the right dimension.

source

theorem TauCeti.trace_eq_smul_quantumDim (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] [SphericalCategory C] (f : X ⟶ X) :

trace f = (endAlgEquivOfSimple k X) { asHom := f } • quantumDim X

In a spherical category, the trace of an endomorphism of a simple object is its scalar times the quantum dimension.

source

theorem TauCeti.leftTrace_inv_comp_rightTrace_hom (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (a : X ≅ X) :

CategoryTheory.CategoryStruct.comp (leftTrace a.inv) (rightTrace a.hom) = CategoryTheory.CategoryStruct.comp (leftDim X) (rightDim X)

For an automorphism a of a simple object, the left trace of a⁻¹ followed by the right trace of a is the left dimension followed by the right dimension: the scalars of a⁻¹ and a cancel.

source

theorem TauCeti.leftDim_comp_rightDim_eq (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (P Q : PivotalCategory C) :

CategoryTheory.CategoryStruct.comp (leftDim X) (rightDim X) = CategoryTheory.CategoryStruct.comp (leftDim X) (rightDim X)

For a simple object X, the left dimension followed by the right dimension of X is the same for any two pivotal structures P and Q on C, although each dimension separately may change.

source

theorem TauCeti.leftTrace_tensorHom_eq_comp_of_simple (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] [FiniteDimensional k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] {X Y : C} (f : X ⟶ X) (g : Y ⟶ Y) :

leftTrace (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = CategoryTheory.CategoryStruct.comp (leftTrace f) (leftTrace g)

If the tensor unit is simple with finite-dimensional endomorphisms over an algebraically closed field, the left trace is multiplicative.

source

theorem TauCeti.rightTrace_tensorHom_eq_comp_of_simple (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] [FiniteDimensional k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] {X Y : C} (f : X ⟶ X) (g : Y ⟶ Y) :

rightTrace (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = CategoryTheory.CategoryStruct.comp (rightTrace f) (rightTrace g)

If the tensor unit is simple with finite-dimensional endomorphisms over an algebraically closed field, the right trace is multiplicative.

source

If the tensor unit is simple with finite-dimensional endomorphisms over an algebraically closed field, the left dimension is multiplicative.

source

If the tensor unit is simple with finite-dimensional endomorphisms over an algebraically closed field, the right dimension is multiplicative.

Documentation

TauCeti.CategoryTheory.Monoidal.Pivotal.Simple

Traces of endomorphisms of simple objects #

References #