Duality in a finite semisimple rigid category #
In a rigid monoidal abelian category with additive tensor product the right dual of a simple
object is simple (TauCeti.simple_rightDual), so duality acts on the simple isomorphism classes:
TauCeti.SimpleClasses.dual (in TauCeti/CategoryTheory/Simple/Rigid.lean) sends the class of
X to the class of Xᘁ. This file shows that this action is the involution of the Grothendieck
ring as a based ring, and that the fusion coefficients satisfy Frobenius reciprocity with respect
to it.
- The involution. If the category is moreover finite semisimple with simple tensor unit, then
every simple object
Xis isomorphic to its double dualXᘁᘁ. The coevaluation𝟙_ C ⟶ X ⊗ Xᘁis nonzero, hence split by someX ⊗ Xᘁ ⟶ 𝟙_ C, and Frobenius reciprocity turns that splitting into a nonzero morphismX ⟶ Xᘁᘁbetween simple objects. So the duality on simple classes is an involution, and the duality[X] ↦ [Xᘁ]of the Grothendieck ring is an involutive anti-automorphism permuting the basis of simple classes. - Frobenius reciprocity. Over an algebraically closed field, with finite-dimensional morphism
spaces, the fusion coefficients satisfy
N_{S* T}^U = N_{S U}^TandN_{S T*}^U = N_{U T}^S, whereS*is the dual class. Equivalently, the fusion matrix ofS*is the transpose of that ofS. The coefficient of the unit class isN_{S T}^𝟙 = 1ifS = T*and0otherwise. In multiplicity form,N_{S T}^Uis the multiplicity ofTinSᘁ ⊗ Uand ofSinU ⊗ Tᘁ. - Transitivity. If the tensor unit is simple, the tensor product of nonzero objects is nonzero,
so for all simple classes
SandUsome simple summandTofSᘁ ⊗ UhasN_{S T}^U > 0, and likewise on the other side. This is the transitivity of the based ring in the sense of Etingof–Gelaki–Nikshych–Ostrik. Consequently, the matrices of multiplication on either side by the sum of all simple classes have positive entries, which is what makes the Perron–Frobenius theorem for positive matrices apply to them.
No pivotal structure is used: the dual class is formed with right duals throughout, and
ExactPairing S Sᘁ supplies both reciprocity isomorphisms.
Main declarations #
TauCeti.nonempty_iso_rightDual_rightDual: a simple object is isomorphic to its double dual.TauCeti.SimpleClasses.dual_dual: duality of simple classes is an involution.TauCeti.exists_nonzero_to_tensor_rightDual_of_nonzero_from_simpleandTauCeti.exists_nonzero_rightDual_of_nonzero_from_simple: Frobenius reciprocity and duality for simple constituents.TauCeti.SplitK0.dual_simpleBasisandTauCeti.SplitK0.dual_dual: the duality of the Grothendieck ring permutes the simple basis and is an involution.TauCeti.fusionCoeff_dual_left,TauCeti.fusionCoeff_dual_rightandTauCeti.fusionCoeff_classOf_unit: Frobenius reciprocity for fusion coefficients.TauCeti.fusionMatrix_dual: the fusion matrix of the dual class is the transpose.TauCeti.fusionCoeff_eq_simpleMultiplicities_rightDual_tensorandTauCeti.fusionCoeff_eq_simpleMultiplicities_tensor_rightDual: Frobenius reciprocity in multiplicity form.TauCeti.exists_fusionCoeff_pos_rightandTauCeti.exists_fusionCoeff_pos_left: transitivity of the fusion rules.TauCeti.sum_fusionCoeff_pos_leftandTauCeti.sum_fusionCoeff_pos_right: multiplication by the sum of all simple classes has a positive matrix.
References #
- [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §§3.1, 3.3, 4.8, 4.9
In a finite semisimple rigid category with simple tensor unit, every simple object is isomorphic to its double right dual.
Frobenius reciprocity for simple constituents: if a simple object U maps nontrivially to
X ⊗ Y, then X maps nontrivially to U ⊗ Yᘁ.
Right duality preserves simple constituents: a nonzero morphism from a simple object U to
Y gives a nonzero morphism Uᘁ ⟶ Yᘁ.
In a finite semisimple rigid category with simple tensor unit, duality of simple classes is an involution.
Duality of simple classes is an involution.
The class of the representative of the dual simple class is the class of the right dual of the representative.
The duality of the Grothendieck ring sends the basis element of a simple class to the basis element of the dual class.
In a finite semisimple rigid category with simple tensor unit, the duality of the Grothendieck ring is an involution.
The duality of the Grothendieck ring is an involution.
Frobenius reciprocity for fusion coefficients: N_{S* T}^U = N_{S U}^T, coming from
(Sᘁ ⊗ T ⟶ U) ≃ (T ⟶ S ⊗ U).
Frobenius reciprocity for fusion coefficients: N_{S T*}^U = N_{U T}^S, coming from
(U ⊗ T ⟶ S) ≃ (U ⟶ S ⊗ Tᘁ).
The fusion matrix of the dual class is the transpose of the fusion matrix:
N_{S* T}^U = N_{S U}^T.
Frobenius reciprocity in multiplicity form: N_{S T}^U is the multiplicity of T in
Sᘁ ⊗ U, coming from (Sᘁ ⊗ U ⟶ T) ≃ (U ⟶ S ⊗ T).
Frobenius reciprocity in multiplicity form: N_{S T}^U is the multiplicity of S in
U ⊗ Tᘁ, coming from (S ⊗ T ⟶ U) ≃ (S ⟶ U ⊗ Tᘁ).
Transitivity of the fusion rules: for simple classes S and U there is a simple class
T with N_{S T}^U > 0, that is, U is a summand of S ⊗ T. Any simple summand T of the
nonzero object Sᘁ ⊗ U will do.
Transitivity of the fusion rules: for simple classes S and U there is a simple class
T with N_{T S}^U > 0, that is, U is a summand of T ⊗ S. Any simple summand T of the
nonzero object U ⊗ Sᘁ will do.
The matrix of multiplication on the left by the sum of all simple classes has positive
entries: ∑ S, N_{S T}^U > 0 for all simple classes T and U.
The matrix of multiplication on the right by the sum of all simple classes has positive
entries: ∑ S, N_{T S}^U > 0 for all simple classes T and U.
The multiplicity of the tensor unit in S ⊗ T is 1 if S is the dual class of T, and 0
otherwise: N_{S T}^𝟙 = δ_{S, T*}.