The categorical trace

The trace of an endomorphism f : X ⟶ X in a rigid symmetric monoidal category: coevaluate at X, let f act, carry the strand across its right dual with the braiding, and evaluate. The result is a scalar, an endomorphism of the tensor unit.

The basic calculus: the trace of the identity is the categorical dimension; the trace is additive and ℂ-homogeneous; it is cyclic; and it is multiplicative over the tensor product.

def RS.catTrace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The categorical trace of an endomorphism: coevaluate, act, cross the strand over the right dual, and evaluate.

Equations

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

def RS.catDim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The categorical dimension of an object: the closed loop obtained by crossing the coevaluation strand over the dual and evaluating.

Equations

• RS.catDim X = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.CategoryStruct.comp (β_ X Xᘁ).hom (ε_ X Xᘁ))

theorem RS.catTrace_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) : catTrace (CategoryTheory.CategoryStruct.id X) = catDim X

The trace of the identity is the categorical dimension.

theorem RS.catTrace_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] {X : C} (f g : X ⟶ X) : catTrace (f + g) = catTrace f + catTrace g

The trace is additive.

theorem RS.catTrace_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] [CategoryTheory.RigidCategory C] {X : C} (a : ℂ) (f : X ⟶ X) : catTrace (a • f) = a • catTrace f

The trace is homogeneous for the ℂ-linear structure.

theorem RS.catTrace_comp_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : catTrace (CategoryTheory.CategoryStruct.comp f g) = catTrace (CategoryTheory.CategoryStruct.comp g f)

Cyclicity of the categorical trace. Both composites close to the same loop: pass the strands across the pairing with the adjoint mates and slide the braiding along.

theorem RS.catTrace_eq_loop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) : catTrace f = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.CategoryStruct.comp (β_ X Xᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ f) (ε_ X Xᘁ)))

The loop form of the trace: the braiding may be taken first and the endomorphism absorbed into the evaluation.

def RS.pairTrace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] {X D : C} (p : CategoryTheory.ExactPairing X D) (f : X ⟶ X) : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The trace computed against a chosen exact pairing.

Equations

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

theorem RS.pairTrace_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] {X D₁ D₂ : C} (p₁ : CategoryTheory.ExactPairing X D₁) (p₂ : CategoryTheory.ExactPairing X D₂) (f : X ⟶ X) : pairTrace p₂ f = pairTrace p₁ f

The trace does not depend on the choice of exact pairing: the comparison morphism between two right duals carries one pairing's coevaluation and evaluation to the other's.

theorem RS.catTrace_eq_pairTrace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) : catTrace f = pairTrace CategoryTheory.HasRightDual.exact f

The categorical trace is the pairing trace of the canonical pairing supplied by rigidity.

theorem RS.nested_cups {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.monoidalComp (η_ X Xᘁ) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (η_ Y Yᘁ)) Xᘁ) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ Xᘁ))))) (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ Xᘁ)).hom = CategoryTheory.monoidalComp (CategoryTheory.CategoryStruct.comp (η_ Y Yᘁ) (β_ Y Yᘁ).hom) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (β_ X Xᘁ).hom) Y)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))))

The block braiding carries the nested coevaluations of a tensor pairing to nested kinked cups: the strands of each loop cross the other loop twice with opposite senses, so the two crossings cancel by symmetry and the loops disentangle.

theorem RS.catTrace_tensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X Y : C} (f : X ⟶ X) (g : Y ⟶ Y) : catTrace (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = catTrace f * catTrace g

Multiplicativity of the categorical trace. The trace of a tensor product of endomorphisms is the product of the traces in the scalar monoid End (𝟙_ C). The trace of the tensor product may be computed against the tensor pairing; there the two loops disentangle by symmetry and the inner loop contracts to a scalar.

@[simp]

theorem RS.catDim_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] : catDim (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = 1

The dimension of the tensor unit is one. Computed against the unit's pairing with itself, the loop closes to the identity scalar.

def RS.catTraceLin {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.End X →ₗ[ℂ] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The trace as a ℂ-linear map into the scalar monoid.

Equations

• RS.catTraceLin X = { toFun := RS.catTrace, map_add' := ⋯, map_smul' := ⋯ }