noncomputable def CategoryTheory.tensorRightHomLinearEquiv (k : Type w) [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] (X Z Y : C) : (MonoidalCategoryStruct.tensorObj X Z ⟶ Y) ≃ₗ[k] X ⟶ MonoidalCategoryStruct.tensorObj Y Zᘁ

Linear equivalence (X ⊗ Z ⟶ Y) ≃ₗ[k] (X ⟶ Y ⊗ Zᘁ) upgrading the right-dual hom adjunction (tensorRightHomEquiv) in a k-linear rigid monoidal category.

theorem CategoryTheory.hom_tensor_right_finrank_eq (k : Type w) [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] (X Z Y : C) : Module.finrank k (MonoidalCategoryStruct.tensorObj X Z ⟶ Y) = Module.finrank k (X ⟶ MonoidalCategoryStruct.tensorObj Y Zᘁ)

The right-dual hom adjunction is a linear equivalence, hence the k-dimensions agree: dim (X ⊗ Z ⟶ Y) = dim (X ⟶ Y ⊗ Zᘁ).

class CategoryTheory.FiniteMultitensorDecompData (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] : Type (max u (u_1 + 1))

Bundle of combinatorial data witnessing the finiteness of a multitensor category C: indexed simples and projective covers, structure constants N_{ij}^l, Jordan–Hölder multiplicities, the dual involution, and the projective-cover multiplicity identities used to formulate the Frobenius–Perron results of EGNO §1.47.

• I : Type u_1
• instFintype : Fintype (I k C)
• instDecEq : DecidableEq (I k C)
• simpleObj : I k C → C
• simpleObj_simple (i : I k C) : Simple (simpleObj i)
• projCover : I k C → C
• projCover_projective (i : I k C) : Projective (projCover i)
• dualIndex : I k C → I k C
• structConst : I k C → I k C → I k C → ℕ
• structConst_eq (i j l : I k C) : structConst i j l = Module.finrank k (MonoidalCategoryStruct.tensorObj (simpleObj i) (simpleObj j) ⟶ simpleObj l)
• jhMult : C → I k C → ℕ
• hom_projCover_eq_mult (i : I k C) (Y : C) : Module.finrank k (projCover i ⟶ Y) = jhMult Y i
• projDecompMult : C → I k C → ℕ
• projDecompMult_eq_hom (Q : C) [Projective Q] (k' : I k C) : projDecompMult Q k' = Module.finrank k (Q ⟶ simpleObj k')
• jhMult_tensor_dual_eq (k' i : I k C) (Z : C) : jhMult (MonoidalCategoryStruct.tensorObj (simpleObj k') Zᘁ) i = ∑ l : I k C, structConst k' (dualIndex i) l * jhMult Z l
• jhMult_leftdual_tensor_eq (k' i : I k C) (Z : C) : jhMult (MonoidalCategoryStruct.tensorObj (ᘁZ) (simpleObj k')) i = ∑ l : I k C, structConst l k' i * jhMult Z l

noncomputable def CategoryTheory.tensorLeftHomLinearEquiv {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] (Z P Y : C) : (MonoidalCategoryStruct.tensorObj Z P ⟶ Y) ≃ₗ[k] P ⟶ MonoidalCategoryStruct.tensorObj (ᘁZ) Y

Linear equivalence (Z ⊗ P ⟶ Y) ≃ₗ[k] (P ⟶ (ᘁZ) ⊗ Y) upgrading the left-dual hom adjunction (tensorLeftHomEquiv) in a k-linear rigid monoidal category.

theorem CategoryTheory.hom_tensor_left_finrank_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] (Z P Y : C) : Module.finrank k (MonoidalCategoryStruct.tensorObj Z P ⟶ Y) = Module.finrank k (P ⟶ MonoidalCategoryStruct.tensorObj (ᘁZ) Y)

The left-dual hom adjunction is a linear equivalence, hence the k-dimensions agree: dim (Z ⊗ P ⟶ Y) = dim (P ⟶ (ᘁZ) ⊗ Y).

def CategoryTheory.projTensorLeftDecompFamily {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] [d : FiniteMultitensorDecompData k C] (i : FiniteMultitensorDecompData.I k C) (Z : C) : (k' : FiniteMultitensorDecompData.I k C) × Fin (∑ l : FiniteMultitensorDecompData.I k C, FiniteMultitensorDecompData.structConst k' (FiniteMultitensorDecompData.dualIndex i) l * FiniteMultitensorDecompData.jhMult Z l) → C

Indexed family of projective covers whose biproduct decomposes P_i ⊗ Z, with k'-summands repeated Σ_l N_{k', i*}^l · [Z:X_l] times (the multiplicities appearing in Proposition 1.47.2, left version).

def CategoryTheory.projTensorRightDecompFamily {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] [d : FiniteMultitensorDecompData k C] (i : FiniteMultitensorDecompData.I k C) (Z : C) : (k' : FiniteMultitensorDecompData.I k C) × Fin (∑ l : FiniteMultitensorDecompData.I k C, FiniteMultitensorDecompData.structConst l k' i * FiniteMultitensorDecompData.jhMult Z l) → C

Indexed family of projective covers whose biproduct decomposes Z ⊗ P_i, with k'-summands repeated Σ_l N_{l, k'}^i · [Z:X_l] times (the multiplicities appearing in Proposition 1.47.2, right version).

theorem CategoryTheory.prop_1_47_2_left {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] [d : FiniteMultitensorDecompData k C] (i : FiniteMultitensorDecompData.I k C) (Z : C) [Limits.HasBiproduct (projTensorLeftDecompFamily i Z)] : Nonempty (MonoidalCategoryStruct.tensorObj (FiniteMultitensorDecompData.projCover i) Z ≅ ⨁ projTensorLeftDecompFamily i Z)

EGNO Proposition 1.47.2 (left version): for any object Z of C, P_i ⊗ Z is isomorphic to a biproduct of projective covers P_k with multiplicities Σ_j N_{k, i*}^j · [Z : X_j].

structure CategoryTheory.FiniteTensorCategoryFPdimData : Type (u_1 + 1)

Numerical data of the Frobenius–Perron dimensions of simples and projective covers in a finite tensor category, together with the dual involution and the identity FPdim(P_i)·FPdim(X_{i*}) = FPdim(C) from EGNO §1.47.

• I : Type u_1
• instFintype : Fintype self.I
• instDecEq : DecidableEq self.I
• instNonempty : Nonempty self.I
• fpDimSimple : self.I → ℝ
• fpDimProjCover : self.I → ℝ
• dualIndex : self.I → self.I
• fpDimSimple_pos (i : self.I) : self.fpDimSimple i > 0
• fpDimProjCover_pos (i : self.I) : self.fpDimProjCover i > 0
• fpDim_projCover_eq (i : self.I) : self.fpDimProjCover i * self.fpDimSimple (self.dualIndex i) = ∑ j : self.I, self.fpDimSimple j * self.fpDimProjCover j

noncomputable def CategoryTheory.FiniteTensorCategoryFPdimData.catFPdim (D : FiniteTensorCategoryFPdimData) : ℝ

The Frobenius–Perron dimension of the finite tensor category, defined as FPdim(C) := Σ_i FPdim(X_i) · FPdim(P_i) (EGNO Definition 1.47.5).