Matrix taxonomy and Bourn localization

DOI10.1007/S10485-022-09692-YarXiv2208.09509WikidataQ114744375 ScholiaQ114744375MaRDI QIDQ6408313FDOQ6408313

Authors: Michael Hoefnagel, Pierre-Alain Jacqmin 

Publication date: 19 August 2022

Abstract: In a recent paper, an algorithm has been presented for determining implications between a particular kind of category theoretic property represented by matrices -- the so called `matrix properties'. In this paper we extend this algorithm to include matrix properties involving pointedness of a category, such as the properties of a category to be unital, strongly unital or subtractive, for example. Moreover, this extended algorithm can also be used to determine whether a given matrix property is the Bourn localization of another, thus leading to new characterizations of Mal'tsev, majority and arithmetical categories. Using a computer implementation of our algorithm, we can display all such properties given by matrices of fixed dimensions, grouped according to their Bourn localizations, as well as the implications between them.

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Categoricity and completeness of theories (03C35) Equational logic, Mal'tsev conditions (08B05) Categories of algebras (08C05) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Formalization of mathematics in connection with theorem provers (68V20) Epimorphisms, monomorphisms, special classes of morphisms, null morphisms (18A20) Embedding theorems, universal categories (18B15) Computer assisted proofs of proofs-by-exhaustion type (68V05) Protomodular categories, semi-abelian categories, Mal'tsev categories (18E13) Computational methods for problems pertaining to category theory (18-08)

This page was built for publication: Matrix taxonomy and Bourn localization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6408313)