The Grothendieck ring of a finite semisimple category #
In a finite semisimple abelian category every object is a finite biproduct of simple objects, with
multiplicities that do not depend on the decomposition (TauCeti.simpleMultiplicities). This file
reads that fact in the split Grothendieck group TauCeti.SplitK0 C: the classes of the chosen
simple representatives form a ℤ-basis, TauCeti.SplitK0.simpleBasis, and the coordinates of the
class of an object in that basis are its simple multiplicities. In particular two objects have the
same class exactly when they are isomorphic, and split K₀ is a free abelian group of rank the
number of simple classes.
When the category is moreover monoidal with additive tensor product, TauCeti.SplitK0 C is a ring
(TauCeti/CategoryTheory/GrothendieckGroup/Monoidal/Basic.lean), and the basis turns it into a
ring with a distinguished basis whose structure constants are the multiplicities of the simple
objects in tensor products of simple objects. Over an algebraically closed field k, with
finite-dimensional morphism spaces, these are the fusion coefficients
N_{ST}^U = finrank k (S ⊗ T ⟶ U) (TauCeti.fusionCoeff), which can equally be computed from
U ⟶ S ⊗ T. If the tensor unit is simple, the unit of the ring is a basis element. This is the
based ring of a fusion category in the sense of Etingof–Gelaki–Nikshych–Ostrik; its duality
involution is in TauCeti/CategoryTheory/Semisimple/Rigid.lean.
⚠ The fusion coefficients are computed by a k-dimension, so their identification with
multiplicities needs the endomorphisms of each simple object to be k. Over a field that is not
algebraically closed this fails: for the real representations of a cyclic group of order three, the
two-dimensional rotation representation V has End V ≅ ℂ, so finrank ℝ (𝟙 ⊗ V ⟶ V) = 2 while
V occurs once in 𝟙 ⊗ V. The multiplicity form of the structure constants
(TauCeti.SplitK0.simpleBasis_mul_simpleBasis) needs no field at all.
Main definitions #
TauCeti.SplitK0.simpleBasis C: theℤ-basis of splitK₀given by the classes of the simple representatives.TauCeti.fusionCoeff k S T U: the fusion coefficientfinrank k (S ⊗ T ⟶ U)of three simple classes.TauCeti.fusionMatrix k S: the fusion matrix ofS, with entryN_{ST}^Uin rowTand columnU.
Main results #
TauCeti.SplitK0.simpleBasis_repr_of: the coordinates of the class of an object are its simple multiplicities.TauCeti.SplitK0.of_eq_of_iff_nonempty_iso: objects with equal classes are isomorphic.TauCeti.SplitK0.finrank_eq_card: the rank of splitK₀is the number of simple classes.TauCeti.SplitK0.one_eq_simpleBasis: the unit is the basis element of the tensor unit, when the tensor unit is simple.TauCeti.fusionCoeff_eq_simpleMultiplicitiesandTauCeti.fusionCoeff_eq_finrank_hom: the fusion coefficient is the multiplicity ofUinS ⊗ T, and the dimension ofU ⟶ S ⊗ T.TauCeti.SplitK0.simpleBasis_mul_simpleBasis: the product of two basis elements is the sum of the basis elements weighted by the multiplicities of the simple objects in their tensor product.TauCeti.SplitK0.simpleBasis_mul_simpleBasis_eq_sum_fusionCoeff: the same expansion, weighted by the fusion coefficients.TauCeti.SplitK0.simpleBasis_repr_simpleBasis_mul_simpleBasis_nonneg: the structure constants are nonnegative, so the Grothendieck ring is a ℤ₊-ring.TauCeti.fusionMatrix_classOf_unit: the fusion matrix of a simple tensor unit is the identity.TauCeti.SplitK0.fusionMatrix_map_mulVec_ringHom: the values of a ring homomorphism on the simple classes form a common eigenvector of the fusion matrices.TauCeti.SplitK0.fusionMatrix_eq_transpose_leftMulMatrix: the fusion matrix ofSis the transpose of the matrix of left multiplication by[S].TauCeti.SplitK0.isIntegral_ringHom_apply: the values of a ring homomorphism out of the Grothendieck ring are algebraic integers.
References #
- Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik, Tensor Categories, Mathematical Surveys and Monographs 205, AMS (2015), Sections 3.1 (based rings), 4.5 (the Grothendieck ring of a fusion category) and 4.16 (the split hypothesis over a general field).
The class of an object is the sum of the classes of the simple representatives, each counted with its multiplicity in the object.
The classes of the simple representatives form a ℤ-basis of split K₀.
Instances For
The basis element of a simple class is the class of its representative.
The coordinates of the class of an object in TauCeti.SplitK0.simpleBasis are its simple
multiplicities.
The class of a simple object is the basis element of its simple class.
Two objects of a finite semisimple category have the same class in split K₀ exactly when
they are isomorphic.
The class of an object of a finite semisimple category vanishes exactly when the object is zero.
Split K₀ of a finite semisimple category is a free abelian group.
Split K₀ of a finite semisimple category with finitely many simple classes is finitely
generated.
Split K₀ of a finite semisimple category has rank the number of simple classes.
This is the statement for Module.finrank, so with infinitely many simple classes both sides are
0; the cardinal form Module.Basis.mk_eq_rank'' applied to simpleBasis C holds in general.
When the tensor unit is simple, the unit of the Grothendieck ring is the basis element of the tensor unit.
The coordinates of the product of two basis elements of the Grothendieck ring are the multiplicities of the simple objects in the tensor product of the representatives.
The structure constants of the Grothendieck ring in the basis of simple classes are nonnegative: it is a ℤ₊-ring.
The product of two basis elements of the Grothendieck ring of a finite semisimple category with finitely many simple classes is the sum of the basis elements weighted by the multiplicities of the simple objects in the tensor product of the representatives.
The values of a ring homomorphism out of the Grothendieck ring of a finite semisimple category with finitely many simple classes are algebraic integers, since the Grothendieck ring is then a finitely generated abelian group.
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).
Instances For
The defining formula of TauCeti.fusionCoeff.
The fusion matrix of a simple class S: the matrix of fusion coefficients N_{ST}^U,
indexed by T (row) and U (column). Over an algebraically closed field, with
finite-dimensional morphism spaces, its row T lists the coordinates of [S] * [T] in the basis
of simple classes (TauCeti.SplitK0.simpleBasis_mul_simpleBasis_eq_sum_fusionCoeff).
Instances For
The entry (T, U) of the fusion matrix of S is the fusion coefficient N_{ST}^U.
When the tensor unit is simple, its fusion matrix is the identity matrix:
N_{𝟙 T}^U = 1 if T = U and 0 otherwise.
The fusion coefficient N_{ST}^U is the multiplicity of U in S ⊗ T.
The fusion coefficient N_{ST}^U is also the dimension of the morphisms from U to
S ⊗ T.
The coordinates of the product of two basis elements of the Grothendieck ring are the fusion coefficients.
The fusion matrix of S is the transpose of the matrix of left multiplication by [S] in the
basis of simple classes.
The product of two basis elements of the Grothendieck ring of a finite semisimple category
with finitely many simple classes is the sum of the basis elements weighted by the fusion
coefficients: [S] * [T] = ∑ U, N_{ST}^U [U].
The values of a ring homomorphism ψ on the basis of simple classes form an eigenvector of
each fusion matrix, with eigenvalue the value of ψ on that class:
∑ U, N_{ST}^U ψ [U] = ψ [S] ψ [T] for all simple classes S and T.