class CategoricalFusionData (κ : Type u_1) [Field κ] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] : Type (max 1 u)

Categorical fusion data for a κ-linear abelian rigid monoidal category C: a finite indexing of representatives S i of simples, fusion coefficients N, duality involution, and Jordan-Hölder multiplicities mult compatible with the unit, tensor product and isomorphisms.

• ι : Type
• ι_fintype : Fintype (ι κ C)
• ι_deceq : DecidableEq (ι κ C)
• S : ι κ C → C
• S_simple (i : ι κ C) : CategoryTheory.Simple (S i)
• S_complete (X : C) : CategoryTheory.Simple X → ∃ (i : ι κ C), Nonempty (X ≅ S i)
• S_distinct (i j : ι κ C) : Nonempty (S i ≅ S j) → i = j
• unitIdx : ι κ C
• unitIso : Nonempty (S unitIdx ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• N : ι κ C → ι κ C → ι κ C → ℕ
• star : ι κ C → ι κ C
• star_star (i : ι κ C) : star (star i) = i
• N_unit_mul (j k : ι κ C) : N unitIdx j k = if j = k then 1 else 0
• N_mul_unit (i k : ι κ C) : N i unitIdx k = if i = k then 1 else 0
• N_duality (i j : ι κ C) : N i j unitIdx = if j = star i then 1 else 0
• N_assoc (i j m l : ι κ C) : ∑ p : ι κ C, N i j p * N p m l = ∑ p : ι κ C, N j m p * N i p l
• N_star_transpose (i j k : ι κ C) : N i j k = N (star i) k j
• N_eq_finrank (i j k : ι κ C) : N i j k = Module.finrank κ (S k ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S i) (S j))
• mult : C → ι κ C → ℕ
• mult_simple (i j : ι κ C) : mult (S i) j = if i = j then 1 else 0
• mult_unit (j : ι κ C) : mult (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) j = if j = unitIdx then 1 else 0
• mult_tensor (X Y : C) (l : ι κ C) : mult (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) l = ∑ i : ι κ C, ∑ j : ι κ C, mult X i * mult Y j * N i j l
• mult_iso (X Y : C) : Nonempty (X ≅ Y) → ∀ (i : ι κ C), mult X i = mult Y i
• mult_nontrivial (X : C) : ∃ (i : ι κ C), 0 < mult X i

def CategoricalFusionData.toFusionRing {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] : FusionRing (ι κ C)

The combinatorial FusionRing (Definition 1.42.2 / Proposition 1.42.4) extracted from the categorical fusion data on C.

@[reducible, inline]

abbrev CategoricalFusionData.GrothendieckRingK0 {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] : Type

Abbreviation for the underlying additive group K₀ of the Grothendieck ring obtained from the categorical fusion data on C.

@[implicit_reducible]

instance CategoricalFusionData.grothendieckRingK0_ring {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] : Ring GrothendieckRingK0

Ring structure on GrothendieckRingK0, inherited from the fusion ring construction.

def CategoricalFusionData.basisClass {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] (i : ι κ C) : GrothendieckRingK0

The basis class in the Grothendieck ring corresponding to the simple object S i.

theorem CategoricalFusionData.basisClass_mul_coeff {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] (i j l : ι κ C) : (basisClass i * basisClass j).coeff l = ↑(N i j l)

The coefficient at l of the product of two basis classes equals the fusion coefficient N i j l.

def RepZ2Categorical.N_categorical (i j k : Fin 2) : ℕ

Fusion coefficients for Rep(ℤ/2): a one-dimensional Hom space iff i + j ≡ k (mod 2).

def FusionCategoryBridge.simpleClass {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] (i : CategoricalFusionData.ι κ C) : CategoricalFusionData.toFusionRing.GrRingOf

Alternative name for the basis class of the simple S i in the Grothendieck ring, used by the fusion-category bridge.

theorem FusionCategoryBridge.simpleClass_mul_coeff {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear κ C] [CategoryTheory.RigidCategory C] [cfd : CategoricalFusionData κ C] (i j l : CategoricalFusionData.ι κ C) : (simpleClass i * simpleClass j).coeff l = ↑(CategoricalFusionData.N i j l)

Coefficient formula for products of simple classes via the fusion-category bridge.

structure BasedRing (ι : Type u_1) [DecidableEq ι] [Fintype ι] : Type u_1

Definition 1.42.2(1): A based ring on the basis ι: fusion coefficients, a unit subset I₀, an involution star, associativity, and the duality / antiautomorphism axioms.

• N : ι → ι → ι → ℕ
• I₀ : Finset ι
• star : ι → ι
• star_star (i : ι) : self.star (self.star i) = i
• assoc (i j k l : ι) : ∑ m : ι, self.N i j m * self.N m k l = ∑ m : ι, self.N j k m * self.N i m l
• sum_I₀_mul_left (j k : ι) : ∑ s ∈ self.I₀, self.N s j k = if j = k then 1 else 0
• sum_I₀_mul_right (i k : ι) : ∑ s ∈ self.I₀, self.N i s k = if i = k then 1 else 0
• duality_trace (i j : ι) : ∑ k ∈ self.I₀, self.N i j k = if i = self.star j then 1 else 0
• star_anti (i j k : ι) : self.N i j k = self.N (self.star j) (self.star i) (self.star k)

def BasedRing.IsUnital {ι : Type u_1} [DecidableEq ι] [Fintype ι] (B : BasedRing ι) : Prop

A based ring is unital (Definition 1.42.2(2)) if 1 itself belongs to the basis, i.e. I₀ is a singleton.

structure UnitalBasedRing (ι : Type u_1) [DecidableEq ι] [Fintype ι] extends BasedRing ι : Type u_1

A UnitalBasedRing is a based ring together with a distinguished basis element unitElem which is the unique element of I₀.

• N : ι → ι → ι → ℕ
• I₀ : Finset ι
• star : ι → ι
• star_star (i : ι) : self.star (self.star i) = i
• assoc (i j k l : ι) : ∑ m : ι, self.N i j m * self.N m k l = ∑ m : ι, self.N j k m * self.N i m l
• sum_I₀_mul_left (j k : ι) : ∑ s ∈ self.I₀, self.N s j k = if j = k then 1 else 0
• sum_I₀_mul_right (i k : ι) : ∑ s ∈ self.I₀, self.N i s k = if i = k then 1 else 0
• duality_trace (i j : ι) : ∑ k ∈ self.I₀, self.N i j k = if i = self.star j then 1 else 0
• star_anti (i j k : ι) : self.N i j k = self.N (self.star j) (self.star i) (self.star k)
• unitElem : ι
• I₀_eq_singleton : self.I₀ = {self.unitElem}

class CategoricalMultitensorData (κ : Type u_1) [Field κ] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : Type (max 1 u)

Categorical multitensor data for a κ-linear monoidal preadditive category C: a finite set of representatives S i of simples together with fusion coefficients N, a unit set I₀, involution and the based-ring axioms. Used to model multitensor (not necessarily tensor) categories.

• ι : Type
• ι_fintype : Fintype (ι κ C)
• ι_deceq : DecidableEq (ι κ C)
• S : ι κ C → C
• S_simple (i : ι κ C) : CategoryTheory.Simple (S i)
• N : ι κ C → ι κ C → ι κ C → ℕ
• N_eq_finrank (i j k : ι κ C) : N i j k = Module.finrank κ (S k ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S i) (S j))
• I₀ : Finset (ι κ C)
• star : ι κ C → ι κ C
• star_star (i : ι κ C) : star (star i) = i
• N_assoc (i j m l : ι κ C) : ∑ p : ι κ C, N i j p * N p m l = ∑ p : ι κ C, N j m p * N i p l
• N_sum_I₀_mul_left (j k : ι κ C) : ∑ p ∈ I₀, N p j k = if j = k then 1 else 0
• N_sum_I₀_mul_right (i k : ι κ C) : ∑ p ∈ I₀, N i p k = if i = k then 1 else 0
• N_duality_trace (i j : ι κ C) : ∑ k ∈ I₀, N i j k = if i = star j then 1 else 0
• N_star_anti (i j k : ι κ C) : N i j k = N (star j) (star i) (star k)

def CategoricalMultitensorData.toBasedRing {κ : Type u_1} [Field κ] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear κ C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [cmd : CategoricalMultitensorData κ C] : BasedRing (ι κ C)

Extract a BasedRing from CategoricalMultitensorData, realising the Grothendieck based ring of a multitensor category.