The partial categorical trace

Tracing out the last tensor factor: for f : P ⊗ X ⟶ P ⊗ X the partial trace ptr f : P ⟶ P closes the X strand into a loop and leaves the P strand open.

The calculus: the partial trace absorbs factors acting on P alone from either side, it commutes with whiskering by a further factor on the left, the partial trace of the braiding of the last two factors is the identity, and the full trace of a partial trace is the full trace. Those are what the cycle-trace factorisation of a permutation action needs.

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

The partial trace of an endomorphism of P ⊗ X over its last factor: coevaluate an X strand beside P, let the endomorphism act, cross the strand over its dual and evaluate.

Equations

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

theorem RS.ptr_whiskerRight_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {P X : C} (a : P ⟶ P) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj P X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj P X) : ptr (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight a X) f) = CategoryTheory.CategoryStruct.comp a (ptr f)

The partial trace absorbs a factor acting on P alone from the left.

theorem RS.ptr_comp_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {P X : C} (a : P ⟶ P) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj P X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj P X) : ptr (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.whiskerRight a X)) = CategoryTheory.CategoryStruct.comp (ptr f) a

The partial trace absorbs a factor acting on P alone from the right.

Tracing inside a further factor

Partial trace over the last factor is unaffected by a factor whiskered on the far left, so it may be computed inside the smaller tensorand. Combined with the calculus above this evaluates the partial trace of the braiding of the last two factors.

theorem RS.ptr_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (Q : C) {R X : C} (u : CategoryTheory.MonoidalCategoryStruct.tensorObj R X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R X) : ptr (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Q R X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q u) (CategoryTheory.MonoidalCategoryStruct.associator Q R X).inv)) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (ptr u)

The partial trace passes a left factor. A morphism acting on R ⊗ X inside Q ⊗ (R ⊗ X) has partial trace Q ◁ ptr u. Both sides carry the same coevaluation, morphism and evaluation in the same order, so only the bracketing differs.

theorem RS.ptr_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) : ptr (β_ X X).hom = CategoryTheory.CategoryStruct.id X

The partial trace of the braiding is the identity: the strand created by the coevaluation crosses the open strand and is capped against it, and the resulting zig-zag is the snake identity of the pairing.

theorem RS.ptr_braiding_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (Q X : C) (g : X ⟶ X) : ptr (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Q X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (β_ X X).hom) (CategoryTheory.MonoidalCategoryStruct.associator Q X X).inv)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q X) g)) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g

The partial trace of a braided last factor: braiding the last two factors and then acting by g on the last traces to g acting on the factor that remains.

The full trace of a partial trace

Closing the remaining P strand of ptr f into a loop closes both strands of f. The comparison passes through the partial trace over the first factor: against the tensor pairing the two loops of the full trace disentangle with the P loop innermost, and an exchange of disjoint cups and caps re-nests the loop closure of ptr f into exactly that shape.

theorem RS.catTrace_ptr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {P X : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj P X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj P X) : catTrace (ptr f) = catTrace f

The full trace of a partial trace is the full trace: closing the remaining strand of ptr f into a loop closes both strands of f.