Categorification of characteristic structures

TL;DR

This paper introduces a categorical framework for understanding characteristic structures in algebra, enabling global descriptions and combinations across categories, with constructive methods suitable for theorem proving.

Contribution

It develops a new representation theory of categories that characterizes structures via functors and natural transformations, facilitating reproducibility and comparison.

Findings

Every characteristic structure is the image of a functor with a natural transformation.

The framework allows combining structures across categories using tensor products.

Results are constructive and suitable for implementation in theorem checkers.

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.