@[reducible, inline]

abbrev IsInvertibleObject_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u_1 u_2)

Reference abbreviation for the definition of an invertible object in a monoidal category.

noncomputable def invertibleObject_inverse_invertible {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : C) [h : CategoryTheory.IsInvertibleObject X] : CategoryTheory.IsInvertibleObject (CategoryTheory.IsInvertibleObject.tensorInverse X)

The tensor inverse of an invertible object is itself invertible.

noncomputable def invertibleObject_leftDual_iso_rightDual {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) [CategoryTheory.HasRightDual X] [CategoryTheory.IsIso (ε_ X Xᘁ)] [CategoryTheory.IsIso (η_ X Xᘁ)] : ᘁX ≅ Xᘁ

For an invertible object X in a rigid monoidal category, the canonical left and right duals are isomorphic.

noncomputable def invertibleObject_tensor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X Y : C) [hX : CategoryTheory.IsInvertibleObject X] [hY : CategoryTheory.IsInvertibleObject Y] : CategoryTheory.IsInvertibleObject (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The tensor product of two invertible objects in a rigid monoidal category is again invertible.

@[reducible, inline]

abbrev IsFiniteAbelianCategory_def (k : Type u_1) [Field k] (A : Type u_2) [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] : Prop

Reference abbreviation for the definition of a finite abelian category.

def grothendieckRing_induced_hom {ι : Type u_1} [DecidableEq ι] [Fintype ι] {κ : Type u_2} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) : R.GrRingOf →+* S.GrRingOf

The ring homomorphism between Grothendieck rings induced by a homomorphism of fusion rings.