noncomputable def TensorCategories.leftQuantumTrace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ Vᘁᘁ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Left quantum trace of an endo-like morphism a : V ⟶ (Vᘁ)ᘁ in a rigid category: the composite η_V V* ≫ (a ▷ V*) ≫ ε_{V*} (V*)*.

noncomputable def TensorCategories.rightQuantumTrace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ ᘁᘁV) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Right quantum trace of an endo-like morphism a : V ⟶ *(*V) in a rigid category, dual to leftQuantumTrace.

theorem TensorCategories.leftTrace_eq_rightTrace_dual (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ Vᘁᘁ) : leftQuantumTrace C a = CategoryTheory.CategoryStruct.comp (η_ Vᘁᘁ Vᘁᘁᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Vᘁᘁ (aᘁ)) (ε_ Vᘁ Vᘁᘁ))

The left quantum trace of a equals the right-trace expression of its dual, via the mate identity for the right adjoint.

theorem TensorCategories.leftTrace_comp_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ Vᘁᘁ) (c : V ⟶ V) : leftQuantumTrace C (CategoryTheory.CategoryStruct.comp c a) = leftQuantumTrace C (CategoryTheory.CategoryStruct.comp a (cᘁᘁ))

Cyclicity of the left quantum trace: tr(c ∘ a) = tr(a ∘ (c*)*) for any endomorphism c : V ⟶ V.

theorem TensorCategories.rightTrace_comp_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ ᘁᘁV) (c : V ⟶ V) : rightQuantumTrace C (CategoryTheory.CategoryStruct.comp c a) = rightQuantumTrace C (CategoryTheory.CategoryStruct.comp a (ᘁᘁc))

Cyclicity of the right quantum trace: tr(c ∘ a) = tr(a ∘ *(*c)) for any endomorphism c : V ⟶ V.

theorem TensorCategories.leftQuantumTrace_additive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] {V W Q : C} (i : W ⟶ V) (p : V ⟶ Q) (aV : V ⟶ Vᘁᘁ) (aW : W ⟶ Wᘁᘁ) (aQ : Q ⟶ Qᘁᘁ) (hi : CategoryTheory.Mono i) (hp : CategoryTheory.Epi p) (exact_seq : CategoryTheory.CategoryStruct.comp i p = 0) (compat_i : CategoryTheory.CategoryStruct.comp i aV = CategoryTheory.CategoryStruct.comp aW (iᘁᘁ)) (compat_p : CategoryTheory.CategoryStruct.comp p aQ = CategoryTheory.CategoryStruct.comp aV (pᘁᘁ)) : leftQuantumTrace C aV = leftQuantumTrace C aW + leftQuantumTrace C aQ

Additivity of the left quantum trace over a short exact sequence 0 → W → V → Q → 0 compatible with the chosen morphisms into the double duals.

theorem TensorCategories.rightQuantumTrace_additive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] {V W Q : C} (i : W ⟶ V) (p : V ⟶ Q) (aV : V ⟶ ᘁᘁV) (aW : W ⟶ ᘁᘁW) (aQ : Q ⟶ ᘁᘁQ) (hi : CategoryTheory.Mono i) (hp : CategoryTheory.Epi p) (exact_seq : CategoryTheory.CategoryStruct.comp i p = 0) (compat_i : CategoryTheory.CategoryStruct.comp i aV = CategoryTheory.CategoryStruct.comp aW (ᘁᘁi)) (compat_p : CategoryTheory.CategoryStruct.comp p aQ = CategoryTheory.CategoryStruct.comp aV (ᘁᘁp)) : rightQuantumTrace C aV = rightQuantumTrace C aW + rightQuantumTrace C aQ

Additivity of the right quantum trace over a short exact sequence 0 → W → V → Q → 0 compatible with the chosen morphisms into the double left duals.

structure TensorCategories.PivotalStructure (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Type (max u v)

A pivotal structure on a rigid monoidal category: a natural monoidal isomorphism V ≅ (Vᘁ)ᘁ with the unit-dimension normalisation dim(𝟙_C) = 1.

• pivotalIso (V : C) : V ≅ Vᘁᘁ
• tensorCoherenceIso (V W : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁᘁ Wᘁᘁ ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)ᘁᘁ
• naturality {V W : C} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f (self.pivotalIso W).hom = CategoryTheory.CategoryStruct.comp (self.pivotalIso V).hom (fᘁᘁ)
• monoidality (V W : C) : (self.pivotalIso (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.pivotalIso V).hom (self.pivotalIso W).hom) (self.tensorCoherenceIso V W).hom
• dimUnit : leftQuantumTrace C (self.pivotalIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[reducible, inline]

abbrev TensorCategories.def_1_38_1 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Type (max u v)

EGNO Definition 1.38.1: synonym for PivotalStructure.

class TensorCategories.PivotalCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Type (max u v)

Class form of PivotalStructure: a pivotal structure on a rigid monoidal category as a typeclass for instance inference.

• pivotalIso (V : C) : V ≅ Vᘁᘁ
• tensorCoherenceIso (V W : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁᘁ Wᘁᘁ ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)ᘁᘁ
• naturality {V W : C} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f (pivotalIso W).hom = CategoryTheory.CategoryStruct.comp (pivotalIso V).hom (fᘁᘁ)
• monoidality (V W : C) : (pivotalIso (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (pivotalIso V).hom (pivotalIso W).hom) (tensorCoherenceIso V W).hom
• dimUnit : leftQuantumTrace C (pivotalIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

noncomputable def TensorCategories.pivotalDimension (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (V : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Pivotal dimension of an object V in a pivotal category: the left quantum trace of the pivotal isomorphism V ≅ (Vᘁ)ᘁ.

@[reducible, inline]

noncomputable abbrev TensorCategories.leftQuantumDim (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (V : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Alias for pivotalDimension: the left quantum dimension of V.

@[reducible, inline]

noncomputable abbrev TensorCategories.categoricalDimension (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (V : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Alias for pivotalDimension: the categorical dimension of V.

noncomputable def TensorCategories.pivotalTrace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {V : C} (f : V ⟶ V) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Pivotal trace of an endomorphism f : V ⟶ V: the left quantum trace of f composed with the pivotal isomorphism.

noncomputable def TensorCategories.categoricalTrace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {V : C} (f : V ⟶ V) : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

Alias for pivotalTrace: the categorical trace of an endomorphism.

theorem TensorCategories.pivotalTrace_id (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (V : C) : pivotalTrace C (CategoryTheory.CategoryStruct.id V) = pivotalDimension C V

The pivotal trace of the identity endomorphism equals the pivotal dimension.

theorem TensorCategories.leftQuantumTrace_tensor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {V W : C} (a : V ⟶ Vᘁᘁ) (b : W ⟶ Wᘁᘁ) (φ : CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁᘁ Wᘁᘁ ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)ᘁᘁ) : leftQuantumTrace C (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) φ.hom) = CategoryTheory.CategoryStruct.comp (leftQuantumTrace C a) (leftQuantumTrace C b)

Multiplicativity of the left quantum trace on tensor products.

theorem TensorCategories.leftQuantumTrace_biproduct (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {V W : C} (a : V ⟶ Vᘁᘁ) (b : W ⟶ Wᘁᘁ) (ψ : Vᘁᘁ ⊞ Wᘁᘁ ≅ (V ⊞ W)ᘁᘁ) : leftQuantumTrace C (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst a) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd b)) ψ.hom) = leftQuantumTrace C a + leftQuantumTrace C b

Additivity of the left quantum trace on biproducts.

structure TensorCategories.Proposition_1_37_1 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Prop

EGNO Proposition 1.37.1: the left quantum trace satisfies left/right-dual equality, biproduct additivity, tensor multiplicativity, and cyclicity for both left and right traces.

• left_eq_right_dual {V : C} (a : V ⟶ Vᘁᘁ) : leftQuantumTrace C a = CategoryTheory.CategoryStruct.comp (η_ Vᘁᘁ Vᘁᘁᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Vᘁᘁ (aᘁ)) (ε_ Vᘁ Vᘁᘁ))
• additivity [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {V W : C} (a : V ⟶ Vᘁᘁ) (b : W ⟶ Wᘁᘁ) (ψ : Vᘁᘁ ⊞ Wᘁᘁ ≅ (V ⊞ W)ᘁᘁ) : leftQuantumTrace C (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst a) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd b)) ψ.hom) = leftQuantumTrace C a + leftQuantumTrace C b
• multiplicativity {V W : C} (a : V ⟶ Vᘁᘁ) (b : W ⟶ Wᘁᘁ) (φ : CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁᘁ Wᘁᘁ ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)ᘁᘁ) : leftQuantumTrace C (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) φ.hom) = CategoryTheory.CategoryStruct.comp (leftQuantumTrace C a) (leftQuantumTrace C b)
• cyclicity_left {V : C} (a : V ⟶ Vᘁᘁ) (c : V ⟶ V) : leftQuantumTrace C (CategoryTheory.CategoryStruct.comp c a) = leftQuantumTrace C (CategoryTheory.CategoryStruct.comp a (cᘁᘁ))
• cyclicity_right {V : C} (a : V ⟶ ᘁᘁV) (c : V ⟶ V) : rightQuantumTrace C (CategoryTheory.CategoryStruct.comp c a) = rightQuantumTrace C (CategoryTheory.CategoryStruct.comp a (ᘁᘁc))

theorem TensorCategories.proposition_1_37_1 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] : Proposition_1_37_1 C

EGNO Proposition 1.37.1 holds: bundled proof assembling the dual-equality, additivity, multiplicativity, and cyclicity statements for the quantum traces.

theorem TensorCategories.pivotalDimension_tensor_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (V W : C) : pivotalDimension C (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) = CategoryTheory.CategoryStruct.comp (pivotalDimension C V) (pivotalDimension C W)

The pivotal dimension is multiplicative on tensor products.

@[simp]

theorem TensorCategories.pivotalDimension_biproduct_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C) : pivotalDimension C (X ⊞ Y) = pivotalDimension C X + pivotalDimension C Y

The pivotal dimension is additive on binary biproducts.

@[simp]

theorem TensorCategories.pivotalDimension_unit (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] : pivotalDimension C (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The pivotal dimension of the unit object is the identity morphism (dim(𝟙_C) = 1).

structure TensorCategories.Proposition_1_38_5_IsCharacter (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : Prop

EGNO Proposition 1.38.5: the pivotal dimension is a character of the Grothendieck ring (multiplicative on tensor products, additive on biproducts, and sending the unit to 1).

• multiplicativity (V W : C) : pivotalDimension C (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) = CategoryTheory.CategoryStruct.comp (pivotalDimension C V) (pivotalDimension C W)
• additivity (X Y : C) : pivotalDimension C (X ⊞ Y) = pivotalDimension C X + pivotalDimension C Y
• unitality : pivotalDimension C (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

theorem TensorCategories.proposition_1_38_5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : Proposition_1_38_5_IsCharacter C

EGNO Proposition 1.38.5 holds: the pivotal dimension is a character of the Grothendieck ring.

theorem TensorCategories.proposition_1_38_5_conj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (∀ (V W : C), pivotalDimension C (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) = CategoryTheory.CategoryStruct.comp (pivotalDimension C V) (pivotalDimension C W)) ∧ (∀ (X Y : C), pivotalDimension C (X ⊞ Y) = pivotalDimension C X + pivotalDimension C Y) ∧ pivotalDimension C (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

Unbundled conjunction form of EGNO Proposition 1.38.5: multiplicativity, additivity, and unitality of the pivotal dimension.

theorem TensorCategories.grothendieck_ring_dim_in_fg_subalgebra (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (k : Type w) [Field k] [CategoryTheory.Preadditive C] (φ : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →+* k) (hFinSimples : ∃ (n : ℕ) (simples : Fin n → C), ∀ (V : C), ∃ (coeffs : Fin n → ℤ), φ (pivotalDimension C V) = ∑ i : Fin n, coeffs i • φ (pivotalDimension C (simples i))) : ∃ (S : Subalgebra ℤ k), (Subalgebra.toSubmodule S).FG ∧ ∀ (V : C), φ (pivotalDimension C V) ∈ S

If a pivotal category has finitely many simple objects spanning the Grothendieck ring, then the image of every pivotal dimension lies in a finitely generated ℤ-subalgebra of the base field.

theorem TensorCategories.pivotalDimension_isIntegral (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (k : Type w) [Field k] [CategoryTheory.Preadditive C] (φ : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →+* k) (hFinSimples : ∃ (n : ℕ) (simples : Fin n → C), ∀ (V : C), ∃ (coeffs : Fin n → ℤ), φ (pivotalDimension C V) = ∑ i : Fin n, coeffs i • φ (pivotalDimension C (simples i))) (V : C) : IsIntegral ℤ (φ (pivotalDimension C V))

Under the same finiteness hypothesis, the image of every pivotal dimension is integral over ℤ in the base field.

theorem TensorCategories.corollary_1_38_6 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (k : Type w) [Field k] [CategoryTheory.Preadditive C] (φ : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →+* k) (hFinSimples : ∃ (n : ℕ) (simples : Fin n → C), ∀ (V : C), ∃ (coeffs : Fin n → ℤ), φ (pivotalDimension C V) = ∑ i : Fin n, coeffs i • φ (pivotalDimension C (simples i))) (V : C) : IsIntegral ℤ (φ (pivotalDimension C V))

EGNO Corollary 1.38.6: in a pivotal category with finitely many simple objects, every pivotal dimension is an algebraic integer.

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

A spherical category is a pivotal category in which the pivotal dimension of every object equals the pivotal dimension of its dual.

• pivotalIso (V : C) : V ≅ Vᘁᘁ
• tensorCoherenceIso (V W : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁᘁ Wᘁᘁ ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)ᘁᘁ
• naturality {V W : C} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f (pivotalIso W).hom = CategoryTheory.CategoryStruct.comp (pivotalIso V).hom (fᘁᘁ)
• monoidality (V W : C) : (pivotalIso (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (pivotalIso V).hom (pivotalIso W).hom) (tensorCoherenceIso V W).hom
• dimUnit : leftQuantumTrace C (pivotalIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• spherical (V : C) : pivotalDimension C V = pivotalDimension C Vᘁ

@[reducible, inline]

abbrev TensorCategories.def_1_39_1 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Type (max u v)

EGNO Definition 1.39.1: synonym for SphericalCategory.

theorem TensorCategories.spherical_leftTrace_eq_rightTrace_aux (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [SphericalCategory C] {V : C} (x : V ⟶ V) : pivotalTrace C x = CategoryTheory.CategoryStruct.comp (η_ Vᘁ Vᘁᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Vᘁ (CategoryTheory.CategoryStruct.comp (PivotalCategory.pivotalIso V).inv x)) (ε_ V Vᘁ))

Helper for the spherical-trace equality: in a spherical category, the pivotal trace of an endomorphism can be expressed via the right-dual evaluation/coevaluation.

theorem TensorCategories.spherical_leftTrace_eq_rightTrace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [SphericalCategory C] {V : C} (x : V ⟶ V) : pivotalTrace C x = CategoryTheory.CategoryStruct.comp (η_ Vᘁ Vᘁᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Vᘁ (CategoryTheory.CategoryStruct.comp (PivotalCategory.pivotalIso V).inv x)) (ε_ V Vᘁ))

In a spherical category the left and right pivotal traces of an endomorphism agree.

structure TensorCategories.Proposition_1_37_3 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Prop

EGNO Proposition 1.37.3: both left and right quantum traces are additive on short exact sequences of objects compatible with the chosen morphisms to the double duals.

• left_additive [CategoryTheory.Preadditive C] {V W Q : C} (i : W ⟶ V) (p : V ⟶ Q) (aV : V ⟶ Vᘁᘁ) (aW : W ⟶ Wᘁᘁ) (aQ : Q ⟶ Qᘁᘁ) : CategoryTheory.Mono i → CategoryTheory.Epi p → CategoryTheory.CategoryStruct.comp i p = 0 → CategoryTheory.CategoryStruct.comp i aV = CategoryTheory.CategoryStruct.comp aW (iᘁᘁ) → CategoryTheory.CategoryStruct.comp p aQ = CategoryTheory.CategoryStruct.comp aV (pᘁᘁ) → leftQuantumTrace C aV = leftQuantumTrace C aW + leftQuantumTrace C aQ
• right_additive [CategoryTheory.Preadditive C] {V W Q : C} (i : W ⟶ V) (p : V ⟶ Q) (aV : V ⟶ ᘁᘁV) (aW : W ⟶ ᘁᘁW) (aQ : Q ⟶ ᘁᘁQ) : CategoryTheory.Mono i → CategoryTheory.Epi p → CategoryTheory.CategoryStruct.comp i p = 0 → CategoryTheory.CategoryStruct.comp i aV = CategoryTheory.CategoryStruct.comp aW (ᘁᘁi) → CategoryTheory.CategoryStruct.comp p aQ = CategoryTheory.CategoryStruct.comp aV (ᘁᘁp) → rightQuantumTrace C aV = rightQuantumTrace C aW + rightQuantumTrace C aQ

theorem TensorCategories.proposition_1_37_3_holds (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Proposition_1_37_3 C

EGNO Proposition 1.37.3 holds: bundled proof of additivity of the left and right quantum traces on short exact sequences.