def
FusionRing.FPdimData.IsIntegral
{ι : Type u_1}
[DecidableEq ι]
[Fintype ι]
{R : FusionRing ι}
(fpd : R.FPdimData)
:
A Frobenius-Perron dimension datum on a fusion ring is integral if every basis element has integer Frobenius-Perron dimension.
Instances For
def
IsIntegralTensorCategory
{κ : 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]
(fpd : CategoricalFusionData.toFusionRing.FPdimData)
:
A tensor category (equipped with CategoricalFusionData) is called integral if its
associated Frobenius-Perron dimension datum on the Grothendieck fusion ring is integral.