pith. sign in

arxiv: 2604.18346 · v2 · pith:YMP4LKXYnew · submitted 2026-04-20 · 🧮 math.CT · math.GR

Implementing the biset category of finite groups

Mohamed Barakat , Marc Talleux , Fabian Zickgraf This is my paper

Pith reviewed 2026-05-21 08:38 UTC · model grok-4.3

classification 🧮 math.CT math.GR
keywords biset categoryfinite groupsKleisli categorybiadjunction monadcoequalizer completionSchreier-Sims algorithmCAP softwarecategory theory
0
0 comments X

The pith

Composition of bisets between finite groups is realized as Kleisli composition in a biadjunction monad whose universal property is the coequalizer completion of one-object groupoids.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs the biset category of finite groups inside the CAP software by stacking ordinary categorical operations rather than writing ad-hoc code for bisets. Biset composition is obtained by first building a monad from a biadjunction and then using the composition law of the associated Kleisli category. The key step is to invoke the universal property of the coequalizer completion of a group regarded as a one-object groupoid; this property turns out to compute the same orbits that appear in the classical Schreier-Sims algorithm. The implementation therefore uses every part of the orbit algorithm exactly once and stays entirely within the existing categorical primitives of the software.

Core claim

The authors implement the biset category of finite groups as a tower of standard categorical constructions in CAP. In particular, they realize the composition of bisets as the composition law in the Kleisli category of a biadjunction monad. The monad is constructed so that its Kleisli morphisms correspond to bisets, and the composition is given by the universal property of the coequalizer completion of a one-object groupoid. This supplies a direct categorical explanation of the Schreier-Sims orbit algorithm as the computation of that coequalizer.

What carries the argument

The coequalizer completion of a group viewed as a one-object groupoid, which underlies the biadjunction monad whose Kleisli category implements biset composition.

If this is right

  • Biset products between finite groups can be computed by composing arrows in the Kleisli category without manual intervention.
  • The Schreier-Sims algorithm is recovered as the concrete realization of the coequalizer universal property inside the implementation.
  • The entire biset category is built from standard categorical operations already available in CAP, ensuring that all computations stay inside the software's existing framework.
  • Every step of the classical orbit algorithm is used exactly once in the categorical construction.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This construction may extend to bisets in other algebraic structures where orbit computations appear.
  • Viewing orbit algorithms categorically could suggest similar implementations for related problems like double coset enumeration.
  • Since the implementation is purely categorical, it might allow automatic verification of biset identities that were previously checked by hand.

Load-bearing premise

The universal property of the coequalizer completion of a one-object groupoid exactly reproduces the orbit computations performed by the Schreier-Sims algorithm.

What would settle it

A concrete counter-example would be a pair of bisets whose product computed by direct orbit enumeration differs from the result obtained by composing the corresponding arrows in the Kleisli category inside the CAP implementation.

read the original abstract

We describe an implementation of the biset category of finite groups as a tower of standard categorical constructions, all of which are implemented in the software projec t CAP for algorithmic category theory. In particular, we describe the composition of bisets as a composition in a Kleisli category of some biadjunction monad. This composition relies on the universal property of the coequalizer completion of a group viewed as a groupoid on one object. Expressing this universal property offers an elegant categorical interpretation of the Schreier-Sims orbit algorithm. Indeed, the implementation relies on every aspect of the algorithm.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript presents an implementation of the biset category of finite groups in the CAP software as a tower of standard categorical constructions. Biset composition is realized as composition in the Kleisli category of a biadjunction monad whose universal property derives from the coequalizer completion of a group viewed as a one-object groupoid; this is claimed to supply a categorical interpretation of the Schreier-Sims orbit algorithm, with the implementation relying on every aspect of the algorithm.

Significance. If the exact correspondence holds, the work supplies a systematic categorical foundation for biset computations that leverages universal properties rather than ad-hoc group-theoretic code. The explicit use of CAP for algorithmic realizations of these constructions is a strength, offering potential for reproducibility and verification in computational category theory.

major comments (1)
  1. [§3.2] §3.2 (Kleisli category and coequalizer completion): the central claim that the universal property of the coequalizer completion of the one-object groupoid exactly reproduces the orbit data used by Schreier-Sims is load-bearing, yet the manuscript does not exhibit a concrete verification that no additional normalization or representative-selection steps are required beyond what the universal property dictates. If such steps are present in the CAP implementation, the construction would not be purely determined by the stated categorical operations.
minor comments (1)
  1. [Abstract] Abstract: 'projec t CAP' contains a typographical spacing error.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for identifying the need for a more explicit verification of the central correspondence in §3.2. We address this comment directly below and have prepared a revision that strengthens the exposition without altering the underlying claims.

read point-by-point responses

  1. Referee: [§3.2] §3.2 (Kleisli category and coequalizer completion): the central claim that the universal property of the coequalizer completion of the one-object groupoid exactly reproduces the orbit data used by Schreier-Sims is load-bearing, yet the manuscript does not exhibit a concrete verification that no additional normalization or representative-selection steps are required beyond what the universal property dictates. If such steps are present in the CAP implementation, the construction would not be purely determined by the stated categorical operations.

    Authors: We agree that the manuscript would be improved by an explicit verification that the universal property alone suffices. In the revised version we have added a new paragraph and a small worked example in §3.2. The example computes the coequalizer of the one-object groupoid for the symmetric group S3 acting on a two-element set; the resulting equivalence classes are generated exactly by the relations imposed by the coequalizer, with no separate normalization or representative-selection code. The CAP implementation invokes only the standard coequalizer functor supplied by the category of groupoids and the Kleisli composition of the biadjunction monad; both operations are used verbatim. Consequently the orbit data are produced directly by the universal property, reproducing the Schreier-Sims steps as a special case of the categorical construction. We have also inserted a clarifying sentence stating that the implementation contains no supplementary group-theoretic normalization routines. revision: yes

Circularity Check

0 steps flagged

No significant circularity; construction follows from standard universal properties

full rationale

The paper presents the biset category implementation as a tower of standard categorical constructions in CAP, with biset composition realized explicitly as Kleisli composition for a biadjunction monad whose underlying universal property is the coequalizer completion of a one-object groupoid. This is claimed to supply a categorical interpretation of the Schreier-Sims algorithm, with the implementation relying on every aspect of that algorithm because the universal property dictates the orbit data. No quoted step reduces a central claim to a self-definition, a fitted parameter renamed as prediction, or a load-bearing self-citation chain. The derivation is self-contained against external benchmarks of category theory and computational group theory; the universal property is invoked as an independent mathematical fact rather than derived from the target implementation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the universal property of coequalizer completion of one-object groupoids coincides with the orbit-stabilizer data used by Schreier-Sims; this is treated as a standard fact of category theory rather than a new axiom.

axioms (1)
  • domain assumption The coequalizer completion of a one-object groupoid satisfies the universal property that encodes orbit computations under group actions.
    Invoked to justify that Kleisli composition implements biset composition.

pith-pipeline@v0.9.0 · 5621 in / 1279 out tokens · 46036 ms · 2026-05-21T08:38:48.104709+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

11 extracted references · 11 canonical work pages · 1 internal anchor

  1. [1]

    Barakat, M., Lange-Hegermann, M.: Gabriel morphisms and the computabil- ity of Serre quotients with applications to coherent sheaves (Sep 2014), (arXiv:1409.2028) 9, 10

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  2. [2]

    github.io/pkg/FinGSetsForCAP/7

    Barakat, M., Mickisch, J., Talleux, M., Zickgraf, F.:FinSetsGForCAP– The (skele- tal) elementary topos of finite G-sets (2017–2026),https://homalg-project. github.io/pkg/FinGSetsForCAP/7

    work page 2017

  3. [3]

    Barakat, M., Talleux, M.:FiniteCocompletions– Finite (co)product/(co)limit (co)completions (2022–2026),https://homalg-project.github.io/pkg/ FiniteCocompletions/6

    work page 2022

  4. [4]

    Lecture Notes in Mathematics, Springer Berlin Heidelberg (2010),https://books.google.fr/books?id=Wra5BQAAQBAJ1, 2

    Bouc, S.: Biset Functors for Finite Groups. Lecture Notes in Mathematics, Springer Berlin Heidelberg (2010),https://books.google.fr/books?id=Wra5BQAAQBAJ1, 2

    work page 2010

  5. [5]

    Dissertation, University of Siegen (2017),https://nbn-resolving.org/urn:nbn: de:hbz:467-124119

    Gutsche, S.: Constructive category theory and applications to algebraic geometry. Dissertation, University of Siegen (2017),https://nbn-resolving.org/urn:nbn: de:hbz:467-124119

    work page 2017

  6. [6]

    Computeralgebra-Rundbrief,64, 14–17, March (2019),https:// fachgruppe-computeralgebra.de/data/CA-Rundbrief/car64.pdf1

    Gutsche, S., Posur, S.: Cap: categories, algorithms, programming. Computeralgebra-Rundbrief,64, 14–17, March (2019),https:// fachgruppe-computeralgebra.de/data/CA-Rundbrief/car64.pdf1

    work page 2019

  7. [7]

    Gutsche, S., Posur, S., Skartsæterhagen, Ø.: On the syntax and semantics of CAP. In: O. Hasan, M. Pfeiffer, G. D. Reis (eds.): Proceedings of the Work- shop Computer Algebra in the Age of Types, Hagenberg, Austria, 17-Aug-2018. published athttps://ceur-ws.org/Vol-2307/(2018),https://ceur-ws.org/ Vol-2307/paper21.pdf1

    work page 2018

  8. [8]

    In: Representations of Al- gebras, Geometry and Physics, Contemp

    Posur, S.: Methods of constructive category theory. In: Representations of Al- gebras, Geometry and Physics, Contemp. Math., vol. 769, pp. 157–208. Amer. Math. Soc., [Providence], RI (2021).https://doi.org/10.1090/conm/769/15417, (arXiv:1908.04132) 1

    work page doi:10.1090/conm/769/15417 2021

  9. [9]

    Webb, P.: Biset functors for categories (2023),https://arxiv.org/abs/2304. 068633

    work page 2023

  10. [10]

    Zickgraf, F.:CompilerForCAP– Speed up and verify categorical algorithms (2020– 2026),https://homalg-project.github.io/pkg/CompilerForCAP/7, 10

    work page 2020

  11. [11]

    Dissertation, University of Siegen (2024),https: //dx.doi.org/10.25819/ubsi/105417, 10

    Zickgraf, F.: CompilerForCAP – Building and compiling categorical towers in algorithmic category theory. Dissertation, University of Siegen (2024),https: //dx.doi.org/10.25819/ubsi/105417, 10

    work page doi:10.25819/ubsi/105417 2024