2025/02/03 by Peter A. Brooksbank, Heiko Dietrich, Brooksbank, Peter A. +7
Computer Science · #Category Theory (math.CT) #FOS: Mathematics #Formal Methods in Verification #Group Theory (math.GR) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Rings and Algebras (math.RA)
paper · pdf · doi:10.48550/arxiv.2502.01138
openalex publication_date 2025/02/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.