Pivotal traces and dimensions of biproducts

The left and right trace of an endomorphism of a finite biproduct are the sums of the traces of its diagonal components. In particular, both pivotal dimensions are additive on finite biproducts. These identities allow dimensions to descend through the direct-sum relations in a Grothendieck group.

The diagonal formulas apply to arbitrary endomorphisms, including ones with nonzero off-diagonal components. Only the particular biproduct in the statement is required to exist; neither an abelian category nor existence of all finite biproducts is assumed.

References

• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §4.7

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

Left pivotal dimension is additive on finite biproducts.

@[simp]

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

Right pivotal dimension is additive on finite biproducts.

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

Left pivotal dimension is additive on binary biproducts.

@[simp]

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

Right pivotal dimension is additive on binary biproducts.