feat: add pivotal and spherical categories roadmap#57
Open
kim-em wants to merge 3 commits into
Open
Conversation
Add a roadmap for pivotal and spherical monoidal categories, discharging
the standing TODO in Mathlib's `Rigid/Basic.lean` ("Define pivotal
categories") and building the theory it opens onto: the dual and
double-dual functors, pivotal structures as trivializations of the double
dual, left and right traces and dimensions, spherical categories, the two
structural examples (`FDRep G` and the pointed categories `Vec^ω_G`), the
classification of pivotal structures by characters of the universal grading
group (DGNO10), and the full synoptic chart of tensor categories from
Henriques-Penneys-Tener (arXiv:1509.02937, Figure 2). Wire its
`Suggested.lean` into the root and list it in the top-level README; the
signatures elaborate against pinned Mathlib with only `sorry` warnings.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Address a second-opinion review of the Suggested.lean pins: - `Pivotal` and `Balanced` now carry their defining axioms as genuine fields (naturality plus monoidal/tensor compatibility of `φ`; the balancing axiom for the twist), instead of storing a bare natural iso. A bare iso is not a pivotal structure, and the Freyd-Yetter and torsor milestones are false without monoidality. - Add a concrete `MonoidalAut` structure so `pivotal_torsor` and the DGNO classification quantify over monoidal (not plain) natural automorphisms. - Correct the README trace formulas: under Mathlib's `ε_ A B : B ⊗ A ⟶ 𝟙` the left trace closes with the evaluation of `(X, Xᘁ)` and the right trace with that of `(Xᘁ, Xᘁᘁ)` (they were swapped). - Bundle the normalized 3-cocycle (`ThreeCocycle`) so `VecTwisted`'s monoidal structure is built only for genuine cocycles, not an arbitrary `ω`. - Gate the fusion-level milestones (`frobeniusPerronDim`, `universalGradingGroup`, the DGNO equivalence) on an explicit `IsFusion k C` hypothesis tying the coefficient field to `C`. - Fix README wording: `FDRep` is registered right-rigid (not full rigid); `Vec^ω_G` is fusion only for finite `G`; and a Layer-0 typo. Still builds with only `sorry` warnings. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…list Replace the componentwise `Pivotal`/`Balanced`/`MonoidalAut` structures (which had carried monoidality as separate `naturality`/`tensor` fields, with the unit coherence demoted to a docstring after an instance-diamond on `𝟙ᘁᘁ`) by the honest form: - pin the double-dual functor's strong-monoidal structure as a real `(doubleDualFunctor C).Monoidal` instance (a genuine Layer-0 `sorry` target); - define `Pivotal` as a natural iso `𝟭 C ≅ (-)ᘁᘁ` together with Mathlib's `NatTrans.IsMonoidal` predicate on it. Naturality is then free (it is an iso of functors) and monoidality is Mathlib's complete unit-and-tensor condition — nothing hand-rolled that could be silently incomplete, and no axiom living only in a comment. `MonoidalAut` and `Balanced` get the same treatment (whole natural iso `𝟭 C ≅ 𝟭 C`; `Balanced` keeps the balancing axiom as a real field). Still builds with only `sorry` warnings. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a roadmap for pivotal and spherical monoidal categories. It discharges the standing TODO in Mathlib's
CategoryTheory/Monoidal/Rigid/Basic.lean("Define pivotal categories (rigid categories equipped with a natural isomorphismᘁᘁ ≅ 𝟙 C)") and specifies the theory it opens onto: the dual functorC ⥤ (Cᵒᵖ)ᴹᵒᵖand the double-dual endofunctor built from it, pivotal structures as monoidal trivializations of the double dual, the left and right categorical traces and dimensions, spherical categories, quantum and Frobenius–Perron dimension, the two structural examples (FDRep Gwith its standard spherical structure, and the pointed categoriesVec^ω_Gwhose pivotal structures form a torsor overHom(G, kˣ)), Frobenius–Schur indicators, the classification of pivotal structures by characters of the universal grading group (Drinfeld–Gelaki–Nikshych–Ostrik), and the full synoptic chart of tensor categories from Henriques–Penneys–Tener (arXiv:1509.02937, Figure 2), including the Drinfel'd-centre arrows and thebalanced+rigid ≃ braided+pivotalequivalence.The core definitions are stated over a
RightRigidCategory(both HPT trace formulas and the double dual use only right duals, and Mathlib registersFDRep k Gas right rigid viaFGModuleCat); the classification results are stated at the fusion-category-over-an-algebraically-closed-characteristic-0-field bar.README.mdis the definitive spec;Suggested.leanpins the load-bearing objects and named milestones assorry-targets and elaborates against the pinned Mathlib with onlysorrywarnings.🤖 Prepared with Claude Code