The trace as a complex number

The categorical trace lands in End (𝟙_ C), the endomorphisms of the tensor unit. When those are exactly the scalars — the hypothesis HasScalarUnit — that monoid is ℂ, and the trace becomes a complex-valued linear functional, which is what a tower's trace fields ask for.

Cyclicity carries across the identification unchanged.

noncomputable def RS.unitScalarEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalCategory C] (h : HasScalarUnit C) : ℂ ≃ₐ[ℂ] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The unit's endomorphisms are the scalars, as an algebra isomorphism. This is HasScalarUnit read as bijectivity of the structure map.

Equations

• RS.unitScalarEquiv h = AlgEquiv.ofBijective (Algebra.ofId ℂ (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) h

noncomputable def RS.unitScalar {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalCategory C] (h : HasScalarUnit C) : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →ₐ[ℂ] ℂ

The scalar named by an endomorphism of the unit.

Equations

• RS.unitScalar h = ↑(RS.unitScalarEquiv h).symm

The complex-valued trace

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

The complex-valued categorical trace.

Equations

• RS.scalarTrace h X = (RS.unitScalar h).toLinearMap ∘ₗ RS.catTraceLin X

theorem RS.scalarTrace_comp_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] [CategoryTheory.RigidCategory C] (h : HasScalarUnit C) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : (scalarTrace h X) (CategoryTheory.CategoryStruct.comp f g) = (scalarTrace h Y) (CategoryTheory.CategoryStruct.comp g f)

The complex-valued trace is cyclic.