The Relational Quotient Completion

TL;DR

This paper develops a categorical framework unifying traditional and quantitative quotients using relational doctrines, introducing quotient completions that handle intensional and extensional notions of equality, with applications to algebraic structures.

Contribution

It introduces relational doctrines and a universal quotient completion, unifying qualitative and quantitative quotients within a categorical setting, and applies these to algebraic and topological structures.

Findings

Unified framework for qualitative and quantitative quotients

Construction of extensional quotient completion

Application to algebraic structures and topological separation

Abstract

Taking a quotient roughly means changing the notion of equality on a given object, set or type. In a quantitative setting, equality naturally generalises to a distance, measuring how much elements are similar instead of just stating their equivalence. Hence, quotients can be understood quantitatively as a change of distance. In this paper, we show how, combining Lawvere's doctrines and the calculus of relations, one can unify quantitative and usual quotients in a common picture. More in detail, we introduce relational doctrines as a functorial description of (the core of) the calculus of relations. Then, we define quotients and a universal construction adding them to any relational doctrine, generalising the quotient completion of existential elementary doctrine and also recovering many quantitative examples. This construction deals with an intensional notion of quotient and breaks extensional equality of morphisms. Then, we describe another construction forcing extensionality, showing how it abstracts several notions of separation in metric and topological structures. Combining these two constructions, we get the extensional quotient completion, whose essential image is characterized through the notion of projective cover. As an application, we show that, under suitable conditions, relational doctrines of algebras arise as the extensional quotient completion of free algebras. Finally, we compare relational doctrines to other categorical structures where one can model the calculus of relations.