Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Categorification of characteristic structures

Peter A. Brooksbank, Heiko Dietrich, Joshua Maglione, E. A. O'Brien, James B. Wilson

TL;DR

The paper develops a constructive, category-theoretic framework for categorifying characteristic substructures in algebra, recasting local invariant data as global ambient-category data through counital natural transformations. By introducing category actions, capsules, and bicapsules, it provides an algebraic, computable model for natural transformations and adjunctions, enabling a systematic Extension Theorem that propagates local characteristic data to larger categories. It then shows that all characteristic substructures can be recovered from counits and bimorphisms, applies the framework to familiar substructures such as derived and verbal subgroups, and demonstrates cross-category transfer from groups to bimaps, algebras, and semisimple structures. The theory supports a constructive proof language in type theory, offering a priori certification of invariants via machine-checkable proofs. An implementation in Agda illustrates practical certification and computation of characteristic structures within this categorical paradigm, highlighting both opportunities and challenges for software-assisted algebra.

Abstract

We develop a representation theory of categories as a means to explore characteristic structures in algebra. Characteristic structures play a critical role in isomorphism testing of groups and algebras, and their construction and description often rely on specific knowledge of the parent object and its automorphisms. In many cases, questions of reproducibility and comparison arise. Here we present a categorical framework that addresses these questions. We prove that every characteristic structure is the image of a functor equipped with a natural transformation. This shifts the local description in the parent object to a global one in the ambient category. Through constructions in representation theory, such as tensor products, we can combine characteristic structure across multiple categories. Our results are constructive, stated in the language of a constructive type theory, which facilitates implementations in theorem checkers.

Categorification of characteristic structures

TL;DR

The paper develops a constructive, category-theoretic framework for categorifying characteristic substructures in algebra, recasting local invariant data as global ambient-category data through counital natural transformations. By introducing category actions, capsules, and bicapsules, it provides an algebraic, computable model for natural transformations and adjunctions, enabling a systematic Extension Theorem that propagates local characteristic data to larger categories. It then shows that all characteristic substructures can be recovered from counits and bimorphisms, applies the framework to familiar substructures such as derived and verbal subgroups, and demonstrates cross-category transfer from groups to bimaps, algebras, and semisimple structures. The theory supports a constructive proof language in type theory, offering a priori certification of invariants via machine-checkable proofs. An implementation in Agda illustrates practical certification and computation of characteristic structures within this categorical paradigm, highlighting both opportunities and challenges for software-assisted algebra.

Abstract

We develop a representation theory of categories as a means to explore characteristic structures in algebra. Characteristic structures play a critical role in isomorphism testing of groups and algebras, and their construction and description often rely on specific knowledge of the parent object and its automorphisms. In many cases, questions of reproducibility and comparison arise. Here we present a categorical framework that addresses these questions. We prove that every characteristic structure is the image of a functor equipped with a natural transformation. This shifts the local description in the parent object to a global one in the ambient category. Through constructions in representation theory, such as tensor products, we can combine characteristic structure across multiple categories. Our results are constructive, stated in the language of a constructive type theory, which facilitates implementations in theorem checkers.

Paper Structure

This paper contains 50 sections, 25 theorems, 127 equations, 11 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Constraining isomorphism by characteristic subgroups
  3. A local-to-global problem
  4. Applications to computation
  5. Structure of this paper
  6. Type theory and certifying characteristic structure
  7. Types
  8. Propositions as types
  9. Equality
  10. Subtypes and inclusion functions
  11. Partial functions
  12. Certifying that the trivial group is characteristic
  13. Algebraic structures and varieties
  14. Intentional and extensional formulations of algebra
  15. Operators, grammars, and signatures
  16. ...and 35 more sections

Key Result

Theorem 1

For the category $\mathsf{Grp}$ of groups and subcategory $\mathrel{\mathop{\mathsf{Grp}}\limits^{ \hbox{\ex@ $\longleftrightarrow$}}}$ of groups and their isomorphisms, the following equalities of sets hold:

Figures (11)

  • Figure 1: Visualizing the abstract category $\mathsf{A}$ in Example \ref{['ex:abscat']}
  • Figure 2: Visualizing the Peirce decomposition of $\mathsf{A}$
  • Figure 3: A natural map of $\mathsf{N}$ (displayed in the left dotted column) from $\mathsf{A}$ (displayed in top row) to $\mathsf{B}$ (shaded gray)
  • Figure 4: Extending a counital
  • Figure 5: Natural transformations from Example \ref{['ex:three-chars']}
  • ...and 6 more figures

Theorems & Definitions (77)

  • Definition 1.1
  • Theorem 1
  • Example 1.3
  • Example 1.3
  • Theorem 2
  • Example 1.4
  • Definition 3.1
  • Example 3.2
  • Definition 3.3
  • Definition 3.4
  • ...and 67 more