Pivotal and spherical categories

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe global dimension of a pivotal fusion category over a field of characteristic zero is nonzero (Etingof–Nikshych–Ostrik)#

Here C is pivotal, k-linear abelian and finite semisimple over an algebraically closed field k of characteristic zero, with finite-dimensional morphism spaces, simple tensor unit, and finitely many simple classes.

TauCeti.globalDim_ne_zero.{w', v, u} (k : Type w') [Field k] [IsAlgClosed k] [CharZero k]
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.RigidCategory C] [TauCeti.PivotalCategory C] [CategoryTheory.Linear k C]
  [CategoryTheory.MonoidalLinear k C] [TauCeti.IsFiniteSemisimpleCategory C]
  [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)]
  [Fintype (TauCeti.SimpleClasses C)] : TauCeti.globalDim C ≠ 0
Lean

Formalized in Tau Ceti as TauCeti.globalDim_ne_zero.

Sources
LeanTauCeti.globalDim_ne_zero
Uses 4
Proof usesCharacters of the Grothendieck ring are ⋆-characters · The Freyd–Yetter identity · Schur's lemma as an identification of algebras · TauCeti.SplitK0.simpleBasis

TheoremCharacters of the Grothendieck ring are ⋆-characters#

A ring homomorphism ψ from the Grothendieck ring of a fusion category to ℝ or ℂ intertwines the duality [X] ↦ [Xᘁ] with complex conjugation.

TauCeti.SplitK0.ringHom_apply_dual.{w, w', v, u, u_1} (k : Type w') [Field k] [IsAlgClosed k]
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.RigidCategory C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] [Finite (TauCeti.SimpleClasses C)] {𝕜 : Type u_1}
  [RCLike 𝕜] (ψ : TauCeti.SplitK0 C →+* 𝕜) (x : TauCeti.SplitK0 C) :
  ψ (TauCeti.SplitK0.dual x) = (starRingEnd 𝕜) (ψ x)
Lean

Formalized in Tau Ceti as TauCeti.SplitK0.ringHom_apply_dual.

Sources
LeanTauCeti.SplitK0.ringHom_apply_dual
Uses 3 · Used by 1
Proof usesFrobenius reciprocity in multiplicity form · TauCeti.fusionCoeff · TauCeti.SplitK0.simpleBasis
Used byThe global dimension of a pivotal fusion category over a field of characteristic zero is nonzero (Etingof–Nikshych–Ostrik)

TheoremThe Frobenius–Perron character#

A ring with a finite nonempty ℤ-basis with nonnegative structure constants, such that every basis element occurs in b j * ∑ i, b i for every j, has exactly one character to ℝ which is nonnegative on the basis.

Module.Basis.existsUnique_ringHom_nonneg.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Fintype ι]
  [Ring R] (b : Module.Basis ι ℤ R) (hb : ∀ (i j l : ι), 0 ≤ (b.repr (b i * b j)) l)
  (ht : ∀ (j l : ι), 0 < ∑ i, (b.repr (b j * b i)) l) [Nonempty ι] : ∃! χ, ∀ (i : ι), 0 ≤ χ (b i)
Lean

Formalized in Tau Ceti as Module.Basis.existsUnique_ringHom_nonneg.

Sources
LeanModule.Basis.existsUnique_ringHom_nonneg
Uses 2 · Used by 2
Proof usesCollatz–Wielandt bound · Perron–Frobenius theorem for nonnegative matrices
Used byTauCeti.frobeniusPerronDim · TauCeti.SplitK0.spectralRadius_fusionMatrix

TheoremTauCeti.SplitK0.spectralRadius_fusionMatrix#

The value of the Frobenius–Perron character on a simple class S is the spectral radius of the fusion matrix of S.

TauCeti.SplitK0.spectralRadius_fusionMatrix.{w, w', v, u} (k : Type w') [Field k] [IsAlgClosed k]
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.RigidCategory C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] [Fintype (TauCeti.SimpleClasses C)]
  (S : TauCeti.SimpleClasses C) :
  spectralRadius ℂ ((TauCeti.fusionMatrix k S).map Nat.cast) =
    ENNReal.ofReal ((TauCeti.SplitK0.frobeniusPerronChar k C) ((TauCeti.SplitK0.simpleBasis C) S))
Lean

Formalized in Tau Ceti as TauCeti.SplitK0.spectralRadius_fusionMatrix.

Sources
LeanTauCeti.SplitK0.spectralRadius_fusionMatrix
Uses 5
Statement usesTauCeti.fusionCoeff · TauCeti.SplitK0.simpleBasis
Proof usesFrobenius reciprocity in multiplicity form · The Frobenius–Perron character · Perron–Frobenius theorem for nonnegative matrices

TheoremThe global dimension does not depend on the pivotal structure#

over an algebraically closed field k, if the endomorphisms of each simple object are finite-dimensional, then any two pivotal structures P and Q on C give the same global dimension.

TauCeti.globalDim_pivotalCategory_eq.{w, v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C]
  [CategoryTheory.Preadditive C] [Fintype (TauCeti.SimpleClasses C)] (k : Type w) [Field k]
  [IsAlgClosed k] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C]
  [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C]
  [∀ (S : TauCeti.SimpleClasses C), FiniteDimensional k (S.repr ⟶ S.repr)]
  (P Q : TauCeti.PivotalCategory C) : TauCeti.globalDim C = TauCeti.globalDim C
Lean

Formalized in Tau Ceti as TauCeti.globalDim_pivotalCategory_eq.

Sources
LeanTauCeti.globalDim_pivotalCategory_eq
Uses 2
Proof usesThe Freyd–Yetter identity · Schur's lemma as an identification of algebras

TheoremTauCeti.symmetricSphericalCategory#

The canonical pivotal structure on a symmetric rigid category is spherical.

TauCeti.symmetricSphericalCategory.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C]
  [CategoryTheory.RigidCategory C] : TauCeti.SphericalCategory C
Lean

Formalized in Tau Ceti as TauCeti.symmetricSphericalCategory.

Sources
LeanTauCeti.symmetricSphericalCategory
Used by 1
Used byFDRep.trace_eq_smul

TheoremFDRep.trace_eq_smul#

The categorical trace of an equivariant endomorphism of a finite-dimensional representation is its linear trace, acting on the trivial representation by scalar multiplication.

FDRep.trace_eq_smul.{u, v} {k : Type u} {G : Type v} [Field k] [Group G] {V : FDRep k G}
  (f : V ⟶ V) :
  TauCeti.trace f =
    (LinearMap.trace k ↑V.V) (ModuleCat.Hom.hom f.hom.hom) •
      CategoryTheory.CategoryStruct.id
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FDRep k G))
Lean

Formalized in Tau Ceti as FDRep.trace_eq_smul.

Sources
LeanFDRep.trace_eq_smul
Uses 1
Statement usesTauCeti.symmetricSphericalCategory

DefinitionTauCeti.SplitK0.simpleBasis#

The classes of the simple representatives form a ℤ-basis of split K₀.

TauCeti.SplitK0.simpleBasis.{w, v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Abelian C] [TauCeti.IsFiniteSemisimpleCategory C]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] :
  Module.Basis (TauCeti.SimpleClasses C) ℤ (TauCeti.SplitK0 C)
Lean

Formalized in Tau Ceti as TauCeti.SplitK0.simpleBasis.

Sources
LeanTauCeti.SplitK0.simpleBasis
Used by 4
Used byCharacters of the Grothendieck ring are ⋆-characters · TauCeti.frobeniusPerronDim · TauCeti.SplitK0.spectralRadius_fusionMatrix · The global dimension of a pivotal fusion category over a field of characteristic zero is nonzero (Etingof–Nikshych–Ostrik)

DefinitionTauCeti.fusionCoeff#

The fusion coefficient N_{ST}^U of three simple classes: the dimension over k of the morphisms from the tensor product of the representatives of S and T to the representative of U. Over an algebraically closed field, with finite-dimensional morphism spaces, it is the multiplicity of U in S ⊗ T (TauCeti.fusionCoeff_eq_simpleMultiplicities).

TauCeti.fusionCoeff.{w', v, u} (k : Type w') [Field k] {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C]
  [CategoryTheory.MonoidalCategory C] (S T U : TauCeti.SimpleClasses C) : ℕ
Lean

Formalized in Tau Ceti as TauCeti.fusionCoeff.

Sources
LeanTauCeti.fusionCoeff
Used by 4
Used byFrobenius reciprocity in multiplicity form · Characters of the Grothendieck ring are ⋆-characters · TauCeti.frobeniusPerronDim · TauCeti.SplitK0.spectralRadius_fusionMatrix

DefinitionTauCeti.frobeniusPerronDim#

The Frobenius–Perron dimension of an object of a fusion category: the value of the Frobenius–Perron character TauCeti.SplitK0.frobeniusPerronChar at the class of the object.

TauCeti.frobeniusPerronDim.{w, w', v, u} (k : Type w') [Field k] [IsAlgClosed k] {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C]
  [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] [Finite (TauCeti.SimpleClasses C)] (X : C) : ℝ
Lean

Formalized in Tau Ceti as TauCeti.frobeniusPerronDim.

Sources
LeanTauCeti.frobeniusPerronDim
Uses 4
Statement usesTauCeti.SplitK0.simpleBasis
Proof usesFrobenius reciprocity in multiplicity form · The Frobenius–Perron character · TauCeti.fusionCoeff

ClassTauCeti.BalancedCategory#

A balanced structure on a braided monoidal category: a twist θ : 𝟭 C ≅ 𝟭 C, a natural automorphism of the identity functor, satisfying the balancing axiom θ_{X ⊗ Y} = (θ_X ⊗ θ_Y) ≫ β_{X,Y} ≫ β_{Y,X}.

TauCeti.BalancedCategory.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Type (max u v)
Lean

Formalized in Tau Ceti as TauCeti.BalancedCategory.

Sources
LeanTauCeti.BalancedCategory
Used by 1
Used byTauCeti.pivotalBalancedEquiv

DefinitionTauCeti.pivotalBalancedEquiv#

Pivotal structures on a braided rigid category correspond to balanced structures via θ_X = φ_X ≫ u_X⁻¹, with inverse φ_X = θ_X ≫ u_X.

TauCeti.pivotalBalancedEquiv.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C]
  [CategoryTheory.RigidCategory C] : TauCeti.PivotalCategory C ≃ TauCeti.BalancedCategory C
Lean

Formalized in Tau Ceti as TauCeti.pivotalBalancedEquiv.

Sources
LeanTauCeti.pivotalBalancedEquiv
Uses 1
Statement usesTauCeti.BalancedCategory

TheoremThe Freyd–Yetter identity#

the component of the pivotal isomorphism at Xᘁ is the mate of the inverse of its component at X.

TauCeti.pivotalIsoApp_rightDual.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [TauCeti.PivotalCategory C]
  (X : C) : (TauCeti.pivotalIsoApp Xᘁ).hom = (TauCeti.pivotalIsoApp X).invᘁ
Lean

Formalized in Tau Ceti as TauCeti.pivotalIsoApp_rightDual.

Sources
LeanTauCeti.pivotalIsoApp_rightDual
Used by 2
Used byThe global dimension does not depend on the pivotal structure · The global dimension of a pivotal fusion category over a field of characteristic zero is nonzero (Etingof–Nikshych–Ostrik)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.