The global dimension of a pivotal category

Let C be a pivotal category which is preadditive and has finitely many isomorphism classes of simple objects. Its global dimension is the scalar globalDim C = ∑ S, leftDim S ≫ leftDim Sᘁ : 𝟙_ C ⟶ 𝟙_ C, summed over the chosen representatives S of the simple classes TauCeti.SimpleClasses C. Since the left dimension of Sᘁ is the right dimension of S, it is also ∑ S, leftDim S ≫ rightDim S, and in a spherical category it is the sum of the squares of the quantum dimensions of the simple objects.

The global dimension is defined from a pivotal structure, but it does not depend on it, at least when the endomorphisms of each simple object are the scalars of an algebraically closed field k over which C is linear: for a simple object S, the product leftDim S ≫ rightDim S is the same for all pivotal structures (TauCeti.leftDim_comp_rightDim_eq), even though the two factors are not. So the global dimension is an invariant of the rigid category C alone, as soon as C admits a pivotal structure. This is what lets a property such as pseudo-unitarity, which compares the global dimension with the Frobenius–Perron dimension, be a property of C.

Main declarations

• TauCeti.globalDim: the global dimension of a pivotal category, with TauCeti.globalDim_def and TauCeti.globalDim_eq_sum_leftDim_comp_rightDim computing it;
• TauCeti.globalDim_eq_sum_quantumDim_comp_quantumDim: in a spherical category it is the sum of the squared quantum dimensions of the simple objects;
• TauCeti.globalDim_pivotalCategory_eq: it does not depend on the pivotal structure.

References

• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §7.21
• P. Etingof, D. Nikshych, V. Ostrik, On fusion categories, Ann. of Math. 162 (2005), §2

noncomputable def TauCeti.globalDim (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [Fintype (SimpleClasses C)] [PivotalCategory C] : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

The global dimension ∑ S, leftDim S ≫ leftDim Sᘁ of a preadditive pivotal category with finitely many simple isomorphism classes, summed over the chosen representatives S of the simple classes.

theorem TauCeti.globalDim_def (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [Fintype (SimpleClasses C)] [PivotalCategory C] : globalDim C = ∑ S : SimpleClasses C, CategoryTheory.CategoryStruct.comp (leftDim S.repr) (leftDim S.reprᘁ)

The defining formula of the global dimension.

theorem TauCeti.globalDim_eq_sum_leftDim_comp_rightDim (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [Fintype (SimpleClasses C)] [PivotalCategory C] : globalDim C = ∑ S : SimpleClasses C, CategoryTheory.CategoryStruct.comp (leftDim S.repr) (rightDim S.repr)

The global dimension is the sum, over the simple classes, of the left dimension followed by the right dimension of the chosen representative.

theorem TauCeti.globalDim_eq_sum_quantumDim_comp_quantumDim (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [Fintype (SimpleClasses C)] [PivotalCategory C] [SphericalCategory C] : globalDim C = ∑ S : SimpleClasses C, CategoryTheory.CategoryStruct.comp (quantumDim S.repr) (quantumDim S.repr)

In a spherical category the global dimension is the sum of the squared quantum dimensions of the simple objects.

theorem TauCeti.globalDim_pivotalCategory_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [Fintype (SimpleClasses C)] (k : Type w) [Field k] [IsAlgClosed k] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] [∀ (S : SimpleClasses C), FiniteDimensional k (S.repr ⟶ S.repr)] (P Q : PivotalCategory C) : globalDim C = globalDim C

The global dimension does not depend on the pivotal structure: over an algebraically closed field k, if the endomorphisms of each simple object are finite-dimensional, then any two pivotal structures P and Q on C give the same global dimension.