Balanced categories

A balanced category is a braided monoidal category equipped with a twist: a natural automorphism θ of the identity functor whose component at a tensor product is the tensor product of the components followed by the double braiding, θ_{X ⊗ Y} = (θ_X ⊗ θ_Y) ≫ β_{X,Y} ≫ β_{Y,X}.

Balanced categories sit between braided categories and ribbon categories. A braided rigid category with a pivotal structure is balanced, and a ribbon category is a balanced rigid category whose twist is compatible with duals.

Main declarations

• TauCeti.BalancedCategory: a twist on a braided monoidal category;
• TauCeti.BalancedCategory.twist_hom_app_unit, TauCeti.BalancedCategory.twist_inv_app_unit: the twist and its inverse are trivial on the unit object;
• TauCeti.BalancedCategory.twist_inv_tensor: the balancing axiom for the inverse twist.

The class is named BalancedCategory rather than Balanced because Mathlib's CategoryTheory.Balanced is the unrelated notion of a category in which every morphism that is both a monomorphism and an epimorphism is an isomorphism.

References

• A. Henriques, D. Penneys, J. Tener, Categorified trace for module tensor categories over braided tensor categories, arXiv:1509.02937, §2.1
• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §8.10

class TauCeti.BalancedCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Type (max u v)

A balanced structure on a braided monoidal category: a twist θ : 𝟭 C ≅ 𝟭 C, a natural automorphism of the identity functor, satisfying the balancing axiom θ_{X ⊗ Y} = (θ_X ⊗ θ_Y) ≫ β_{X,Y} ≫ β_{Y,X}.

• twist : CategoryTheory.Functor.id C ≅ CategoryTheory.Functor.id C

  The twist, with components θ_X : X ≅ X.

• twist_tensor (X Y : C) : twist.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (twist.hom.app X) (twist.hom.app Y)) (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom)

  The balancing axiom: the twist of a tensor product is the tensor product of the twists, followed by the double braiding.

theorem TauCeti.BalancedCategory.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {x y : BalancedCategory C} : x = y ↔ twist = twist

theorem TauCeti.BalancedCategory.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {x y : BalancedCategory C} (twist : twist = twist) : x = y

theorem TauCeti.BalancedCategory.twist_tensor_assoc {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} [self : BalancedCategory C] (X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (twist.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (twist.hom.app X) (twist.hom.app Y)) (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (β_ Y X).hom h))

The balancing axiom: the twist of a tensor product is the tensor product of the twists, followed by the double braiding.

@[simp]

theorem TauCeti.BalancedCategory.twist_hom_app_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [BalancedCategory C] : twist.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The twist of the unit object is the identity.

@[simp]

theorem TauCeti.BalancedCategory.twist_inv_app_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [BalancedCategory C] : twist.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The inverse twist of the unit object is the identity.

theorem TauCeti.BalancedCategory.twist_inv_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [BalancedCategory C] (X Y : C) : twist.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = CategoryTheory.CategoryStruct.comp (β_ Y X).inv (CategoryTheory.CategoryStruct.comp (β_ X Y).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (twist.inv.app X) (twist.inv.app Y)))

The balancing axiom for the inverse twist: the inverse twist of a tensor product is the inverse double braiding followed by the tensor product of the inverse twists.

theorem TauCeti.BalancedCategory.twist_inv_tensor_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [BalancedCategory C] (X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (twist.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h = CategoryTheory.CategoryStruct.comp (β_ Y X).inv (CategoryTheory.CategoryStruct.comp (β_ X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (twist.inv.app X) (twist.inv.app Y)) h))

The balancing axiom for the inverse twist: the inverse twist of a tensor product is the inverse double braiding followed by the tensor product of the inverse twists.

theorem TauCeti.BalancedCategory.comp_inv_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [BalancedCategory C] {X Y : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) : CategoryTheory.CategoryStruct.comp f (β_ Y X).inv = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (twist.hom.app X) (twist.hom.app Y)) (β_ X Y).hom)

On a morphism out of the unit, balancing replaces an inverse crossing by a crossing and the twists of the two tensor factors.

theorem TauCeti.BalancedCategory.comp_inv_braiding_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [BalancedCategory C] {X Y : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (β_ Y X).inv h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (twist.hom.app X) (twist.hom.app Y)) (CategoryTheory.CategoryStruct.comp (β_ X Y).hom h))

On a morphism out of the unit, balancing replaces an inverse crossing by a crossing and the twists of the two tensor factors.