def FusionRing.IsRegularElement {ι : Type u_1} [DecidableEq ι] [Fintype ι] (A : FusionRing ι) (fpd : A.FPdimData) (coeffs : ι → ℝ) : Prop

A family of real coefficients coeffs is a regular element of a fusion ring A with Frobenius–Perron dimension data fpd if it is a simultaneous eigenvector of left multiplication by every basis object X with eigenvalue fpd.d X.

structure FusionRing.RegularElement {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (fpd : R.FPdimData) : Type u_1

A regular element of a fusion ring R: a positive vector r that is absorbed on both sides by multiplication with eigenvalue equal to the Frobenius–Perron dimension, and whose Frobenius–Perron norm ∑ d_i · r_i is positive.

• r : ι → ℝ
• r_pos (i : ι) : 0 < self.r i
• left_absorb (X k : ι) : ∑ j : ι, ↑(R.N X j k) * self.r j = fpd.d X * self.r k
• right_absorb (Y k : ι) : ∑ j : ι, ↑(R.N j Y k) * self.r j = fpd.d Y * self.r k
• fpdim_pos : 0 < ∑ i : ι, fpd.d i * self.r i

theorem FusionRing.RegularElement.isRegularElement {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} {fpd : R.FPdimData} (reg : R.RegularElement fpd) : R.IsRegularElement fpd reg.r

The underlying coefficient vector of a RegularElement is a regular element in the sense of IsRegularElement.

theorem FusionRing.IsRegularElement.coeffs_pos_of_regularElement {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} {fpd : R.FPdimData} (reg : R.RegularElement fpd) (i : ι) : 0 < reg.r i

The coefficients of a RegularElement are strictly positive.

theorem FusionRing.proposition_1_45_8 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {A : FusionRing ι} (fpd : A.FPdimData) (star : ι → ι) (hstar : A.IsAntiAutomorphism star) (X : ι) : fpd.d (star X) = fpd.d X

Proposition 1.45.8 (Etingof–Gelaki–Nikshych–Ostrik): The Frobenius–Perron dimension is invariant under any anti-automorphism star of the fusion ring; in particular, dimensions of dual objects equal those of the originals.