Spherical categories

A pivotal category is spherical when the left and right traces of every endomorphism agree. In a spherical category the common value trace f = leftTrace f = rightTrace f is the categorical trace, and the quantum dimension quantumDim X = trace (𝟙 X) is the common value of the left and right dimensions of X.

The trace inherits the properties of both one-sided traces: it is cyclic, additive, linear in a linear monoidal category, the identity on scalars, additive on biproducts, and invariant under the right adjoint mate, so that quantumDim Xᘁ = quantumDim X. Since the left trace lets a scalar act on the right of a loop and the right trace lets one act on the left, a scalar acting on either side factors out of the trace. Combined with the nested-loop formula for the trace of a tensor product, this makes the trace multiplicative in every spherical category: trace (f ⊗ₘ g) = trace f ≫ trace g, and so quantumDim (X ⊗ Y) = quantumDim X ≫ quantumDim Y. No braiding is needed. For the one-sided traces of a merely pivotal category, multiplicativity is only available when the relevant scalar acts on an object in the same way from both sides, for instance in a braided category.

Main declarations

• TauCeti.SphericalCategory: a pivotal category whose left and right traces agree;
• TauCeti.trace and TauCeti.quantumDim: the trace of an endomorphism and the quantum dimension of an object in a spherical category;
• TauCeti.trace_comm: cyclicity of the trace;
• TauCeti.trace_rightAdjointMate and TauCeti.quantumDim_rightDual: invariance under duality;
• TauCeti.trace_scalar_whiskerRight_comp and TauCeti.trace_comp_whiskerLeft_scalar: a scalar acting on either side factors out of the trace;
• TauCeti.trace_tensorHom and TauCeti.quantumDim_tensor: multiplicativity of the trace and of the quantum dimension;
• TauCeti.trace_biproduct and TauCeti.quantumDim_biproduct: additivity on finite biproducts.

References

• A. Henriques, D. Penneys, J. Tener, Categorified trace for module tensor categories over braided tensor categories, arXiv:1509.02937, §2.1
• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §4.7
• leanprover-community/mathlib4#42191, for the names SphericalCategory, leftTrace_eq_rightTrace, trace, trace_eq_leftTrace and trace_eq_rightTrace

class TauCeti.SphericalCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] : Prop

A pivotal category is spherical when the left and right traces of every endomorphism agree.

• leftTrace_eq_rightTrace {X : C} (f : X ⟶ X) : leftTrace f = rightTrace f

  The left and right traces of every endomorphism agree.

noncomputable def TauCeti.trace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [_hC : SphericalCategory C] {X : C} (f : X ⟶ X) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

The trace of an endomorphism in a spherical category: the common value of its left and right traces. The sphericity hypothesis is not needed to write down the formula, but it is carried so that trace is only available where it does not depend on the side.

noncomputable def TauCeti.quantumDim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

The quantum dimension of an object of a spherical category: the trace of its identity.

theorem TauCeti.trace_eq_leftTrace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X : C} (f : X ⟶ X) : trace f = leftTrace f

The trace is the left trace.

theorem TauCeti.trace_eq_rightTrace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X : C} (f : X ⟶ X) : trace f = rightTrace f

The trace is the right trace.

@[simp]

theorem TauCeti.trace_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X : C) : trace (CategoryTheory.CategoryStruct.id X) = quantumDim X

The trace of an identity is the quantum dimension.

theorem TauCeti.leftDim_eq_rightDim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X : C) : leftDim X = rightDim X

In a spherical category the left and right dimensions agree.

theorem TauCeti.quantumDim_eq_leftDim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X : C) : quantumDim X = leftDim X

The quantum dimension is the left dimension.

theorem TauCeti.quantumDim_eq_rightDim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X : C) : quantumDim X = rightDim X

The quantum dimension is the right dimension.

theorem TauCeti.trace_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : trace (CategoryTheory.CategoryStruct.comp f g) = trace (CategoryTheory.CategoryStruct.comp g f)

Cyclicity of the trace: trace (f ≫ g) = trace (g ≫ f).

theorem TauCeti.trace_conj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X Y : C} (i : X ≅ Y) (f : X ⟶ X) : trace (CategoryTheory.CategoryStruct.comp i.inv (CategoryTheory.CategoryStruct.comp f i.hom)) = trace f

The trace is invariant under conjugation by an isomorphism.

theorem TauCeti.quantumDim_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X Y : C} (i : X ≅ Y) : quantumDim X = quantumDim Y

Isomorphic objects have the same quantum dimension.

@[simp]

theorem TauCeti.trace_rightAdjointMate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X : C} (f : X ⟶ X) : trace (fᘁ) = trace f

The trace of the right adjoint mate fᘁ is the trace of f.

@[simp]

theorem TauCeti.quantumDim_rightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X : C) : quantumDim Xᘁ = quantumDim X

An object and its right dual have the same quantum dimension.

@[simp]

theorem TauCeti.trace_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : trace a = a

The trace of a scalar is itself: for a : 𝟙_ C ⟶ 𝟙_ C, trace a = a.

@[simp]

theorem TauCeti.quantumDim_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] : quantumDim (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The quantum dimension of the unit is 𝟙.

theorem TauCeti.trace_scalar_whiskerRight_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X : C} (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (f : X ⟶ X) : trace (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight a X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f))) = CategoryTheory.CategoryStruct.comp a (trace f)

A scalar acting on X from the left factors out of the trace.

theorem TauCeti.trace_comp_whiskerLeft_scalar {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X : C} (f : X ⟶ X) (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : trace (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X a) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))) = CategoryTheory.CategoryStruct.comp (trace f) a

A scalar acting on X from the right factors out of the trace.

@[simp]

theorem TauCeti.trace_tensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] {X Y : C} (f : X ⟶ X) (g : Y ⟶ Y) : trace (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = CategoryTheory.CategoryStruct.comp (trace f) (trace g)

Multiplicativity of the trace: in a spherical category, trace (f ⊗ₘ g) = trace f ≫ trace g, with no braiding required.

@[simp]

theorem TauCeti.quantumDim_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] (X Y : C) : quantumDim (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = CategoryTheory.CategoryStruct.comp (quantumDim X) (quantumDim Y)

Multiplicativity of the quantum dimension: quantumDim (X ⊗ Y) = quantumDim X ≫ quantumDim Y.

@[simp]

theorem TauCeti.trace_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X : C} (f g : X ⟶ X) : trace (f + g) = trace f + trace g

The trace is additive.

@[simp]

theorem TauCeti.trace_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (X : C) : trace 0 = 0

The trace of zero is zero.

@[simp]

theorem TauCeti.quantumDim_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasZeroObject C] : quantumDim 0 = 0

The zero object has quantum dimension zero.

@[simp]

theorem TauCeti.trace_sum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {ι : Type u_1} {X : C} (s : Finset ι) (f : ι → (X ⟶ X)) : trace (∑ i ∈ s, f i) = ∑ i ∈ s, trace (f i)

The trace commutes with finite sums.

@[simp]

theorem TauCeti.trace_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X : C} (f : X ⟶ X) : trace (-f) = -trace f

The trace commutes with negation.

@[simp]

theorem TauCeti.trace_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X : C} (f g : X ⟶ X) : trace (f - g) = trace f - trace g

The trace commutes with subtraction.

@[simp]

theorem TauCeti.trace_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalLinear R C] {X : C} (r : R) (f : X ⟶ X) : trace (r • f) = r • trace f

The trace is R-linear in an R-linear monoidal category.

theorem TauCeti.trace_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {ι : Type u_1} [Fintype ι] {X : ι → C} [CategoryTheory.Limits.HasBiproduct X] (f : ⨁ X ⟶ ⨁ X) : trace f = ∑ i : ι, trace (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π X i)))

The trace of an endomorphism of a finite biproduct is the sum of the traces of its diagonal components.

@[simp]

theorem TauCeti.trace_biproduct_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {ι : Type u_1} [Fintype ι] {X : ι → C} [CategoryTheory.Limits.HasBiproduct X] (f : (i : ι) → X i ⟶ X i) : trace (CategoryTheory.Limits.biproduct.map f) = ∑ i : ι, trace (f i)

The trace of a block-diagonal morphism is the sum of its block traces.

@[simp]

theorem TauCeti.quantumDim_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {ι : Type u_1} [Fintype ι] {X : ι → C} [CategoryTheory.Limits.HasBiproduct X] : quantumDim (⨁ X) = ∑ i : ι, quantumDim (X i)

The quantum dimension is additive on finite biproducts.

theorem TauCeti.trace_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⊞ Y ⟶ X ⊞ Y) : trace f = trace (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) + trace (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd))

The trace of an endomorphism of a binary biproduct is the sum of the traces of its two diagonal components.

@[simp]

theorem TauCeti.trace_biprod_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ X) (g : Y ⟶ Y) : trace (CategoryTheory.Limits.biprod.map f g) = trace f + trace g

The trace of a binary block-diagonal morphism is the sum of its block traces.

@[simp]

theorem TauCeti.quantumDim_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [SphericalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : quantumDim (X ⊞ Y) = quantumDim X + quantumDim Y

The quantum dimension is additive on binary biproducts.