@[reducible, inline]

abbrev FormalProjectiveSum (I : Type u_1) : Type u_1

A formal real-coefficient combination of objects indexed by I, used to represent formal sums of projective covers in the Grothendieck setting.

def FormalProjectiveSum.coeff {I : Type u_1} (s : FormalProjectiveSum I) (i : I) : ℝ

The coefficient of basis element i in the formal sum s.

noncomputable def FormalProjectiveSum.basis {I : Type u_1} (i : I) : FormalProjectiveSum I

The standard basis element of FormalProjectiveSum I associated to i, namely the indicator function supported at i with value 1.

noncomputable def FormalProjectiveSum.fpdim {I : Type u_1} [Fintype I] (s : FormalProjectiveSum I) (fpDimP : I → ℝ) : ℝ

The Frobenius–Perron dimension of a formal projective sum s, given the Frobenius–Perron dimensions fpDimP of the basis projectives.

noncomputable def FormalProjectiveSum.ofFun {I : Type u_1} [Fintype I] (f : I → ℝ) : FormalProjectiveSum I

Promote a function I → ℝ on a finite type to a FormalProjectiveSum I.

structure FiniteTensorCategoryFPData : Type (u_1 + 1)

Frobenius–Perron data for a finite tensor category: a nonempty finite indexing type I of simple objects, together with the (strictly positive) Frobenius–Perron dimensions of the simples and of their projective covers.

• I : Type u_1
• I_fintype : Fintype self.I
• I_nonempty : Nonempty self.I
• fpDimSimple : self.I → ℝ
• fpDimProjCover : self.I → ℝ
• fpDimSimple_pos (i : self.I) : self.fpDimSimple i > 0
• fpDimProjCover_pos (i : self.I) : self.fpDimProjCover i > 0

noncomputable def FiniteTensorCategoryFPData.regularObject (D : FiniteTensorCategoryFPData) : FormalProjectiveSum D.I

The regular object of a finite tensor category: the formal sum of the projective covers weighted by the Frobenius–Perron dimensions of the simples.

@[simp]

theorem FiniteTensorCategoryFPData.regularObject_coeff (D : FiniteTensorCategoryFPData) (i : D.I) : D.regularObject.coeff i = D.fpDimSimple i

The coefficient of the regular object at i equals the Frobenius–Perron dimension of the simple object i.

noncomputable def FiniteTensorCategoryFPData.fpdimRegularObject (D : FiniteTensorCategoryFPData) : ℝ

The Frobenius–Perron dimension of the regular object: the formal sum of dim(simple i) · dim(projCover i).

theorem FiniteTensorCategoryFPData.fpdimRegularObject_eq (D : FiniteTensorCategoryFPData) : D.fpdimRegularObject = ∑ i : D.I, D.fpDimSimple i * D.fpDimProjCover i

The Frobenius–Perron dimension of the regular object expanded as the explicit sum ∑ dim(simple i) · dim(projCover i).

@[reducible, inline]

noncomputable abbrev Definition_1_47_4 (D : FiniteTensorCategoryFPData) : FormalProjectiveSum D.I

Reference abbreviation for Definition 1.47.4 (the regular object of a finite tensor category).