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

Typeclass packaging Jordan-Hölder multiplicities for a rigid linear monoidal abelian category C with categorical fusion data: each object is assigned multiplicities indexed by the simples in a way compatible with the unit, tensor product and isomorphisms.

• mult : C → CategoricalFusionData.ι κ C → ℕ
• mult_simple (i j : CategoricalFusionData.ι κ C) : mult (CategoricalFusionData.S i) j = if i = j then 1 else 0
• mult_unit (j : CategoricalFusionData.ι κ C) : mult (MonoidalCategoryStruct.tensorUnit C) j = if j = CategoricalFusionData.unitIdx then 1 else 0
• mult_tensor (X Y : C) (l : CategoricalFusionData.ι κ C) : mult (MonoidalCategoryStruct.tensorObj X Y) l = ∑ i : CategoricalFusionData.ι κ C, ∑ j : CategoricalFusionData.ι κ C, mult X i * mult Y j * CategoricalFusionData.N i j l
• mult_iso (X Y : C) : Nonempty (X ≅ Y) → ∀ (i : CategoricalFusionData.ι κ C), mult X i = mult Y i
• mult_nontrivial (X : C) : ∃ (i : CategoricalFusionData.ι κ C), 0 < mult X i

@[implicit_reducible]

instance CategoryTheory.hasJordanHolderMultiplicities_of_categoricalFusionData (κ : Type u_1) [Field κ] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] : HasJordanHolderMultiplicities κ C

Any CategoricalFusionData directly supplies Jordan-Hölder multiplicities by reading off its built-in multiplicity function and the associated axioms.

noncomputable def CategoryTheory.jhFpDim {κ : Type u_1} [Field κ] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] [jh : HasJordanHolderMultiplicities κ C] (fpd : CategoricalFusionData.toFusionRing.FPdimData) (X : C) : ℝ

Lifts a Frobenius-Perron dimension defined on simples to all objects of C by summing multiplicities weighted by fpd.d.

theorem CategoryTheory.jhFpDim_unit {κ : Type u_1} [Field κ] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] [jh : HasJordanHolderMultiplicities κ C] (fpd : CategoricalFusionData.toFusionRing.FPdimData) : jhFpDim fpd (MonoidalCategoryStruct.tensorUnit C) = 1

The lifted Frobenius-Perron dimension of the unit object equals 1.

theorem CategoryTheory.jhFpDim_pos {κ : Type u_1} [Field κ] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] [jh : HasJordanHolderMultiplicities κ C] (fpd : CategoricalFusionData.toFusionRing.FPdimData) (X : C) : jhFpDim fpd X > 0

The lifted Frobenius-Perron dimension is strictly positive on every object.

theorem CategoryTheory.jhFpDim_tensor {κ : Type u_1} [Field κ] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] [jh : HasJordanHolderMultiplicities κ C] (fpd : CategoricalFusionData.toFusionRing.FPdimData) (X Y : C) : jhFpDim fpd (MonoidalCategoryStruct.tensorObj X Y) = jhFpDim fpd X * jhFpDim fpd Y

The lifted Frobenius-Perron dimension is multiplicative on tensor products.

theorem CategoryTheory.jhFpDim_iso {κ : Type u_1} [Field κ] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] [jh : HasJordanHolderMultiplicities κ C] (fpd : CategoricalFusionData.toFusionRing.FPdimData) (X Y : C) (h : Nonempty (X ≅ Y)) : jhFpDim fpd X = jhFpDim fpd Y

The lifted Frobenius-Perron dimension is invariant under isomorphism.

noncomputable def CategoryTheory.jhLiftFPdimData {κ : Type u_1} [Field κ] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear κ C] [Abelian C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear κ C] [RigidCategory C] [cfd : CategoricalFusionData κ C] [jh : HasJordanHolderMultiplicities κ C] (fpd : CategoricalFusionData.toFusionRing.FPdimData) : FPdimFunction

Packages the lifted Jordan-Hölder Frobenius-Perron dimension as an FPdimFunction on C.

@[reducible]

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

From CategoricalFusionData together with Jordan-Hölder multiplicities and the Perron-Frobenius property, the category C carries a Grothendieck fusion ring.

def CategoryTheory.rank1FusionRing : FusionRing (Fin 1)

The trivial rank-one fusion ring with index set Fin 1 and the single basis element acting as the unit.

@[implicit_reducible]

instance CategoryTheory.instHasPerronFrobeniusPropertyFinOfNatNat : FusionRing.HasPerronFrobeniusProperty (Fin 1)

The rank-one fusion ring trivially has the Perron-Frobenius property since all matrices and eigenvectors are one-by-one.

noncomputable def CategoryTheory.rank1FPdimData : rank1FusionRing.FPdimData

Frobenius-Perron dimension data for the trivial rank-one fusion ring.