Projective covers, doctrines of algebras and the relational quotient completion

Fabio Pasquali; Francesco Dagnino

REVIEW 2 major objections 6 minor 24 references

Projective covers, doctrines of algebras and the relational quotient completion

T0 review · 2 major / 6 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that an extensional relational doctrine with quotients is a relational quotient completion exactly when it has a projective cover, and that monadic doctrines of algebras inherit this property from their free-algebra sub-doc

desk verdict Genuinely new unification of exact and elementary quotient completions via projective covers; proofs mostly solid, with one real but fixable gap in Theorem 3.7. read the letter →

arxiv 2608.01915 v1 pith:RDU6KDPY submitted 2026-08-03 math.CT

Francesco Dagnino , Fabio Pasquali This is my paper · ORCID

classification math.CT MSC 18A3218D0518E1018C2003G1506F35

keywords relationaldoctrinesquotientcompletionprojectivecoversEilenberg-Mooremonadsexactquantitativealgebrasmetricspaces

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper characterizes the extensional quotient completion of a relational doctrine as precisely those extensional doctrines with quotients that have enough projectives, i.e., admit a projective cover. It then shows that for any quotient-preserving monad on such a doctrine, the resulting Eilenberg-Moore doctrine of algebras is again an extensional quotient completion of its restriction to free algebras over projectives. This generalizes the classical results on exact completion and monadic categories over exact ones, and opens the door to new examples such as quantitative algebras over metric spaces. A sharper version, Theorem 4.16, shows that when quotient arrows split, every monad on the doctrine yields an algebra doctrine that is a projective cover of free algebras.

What carries the argument

The defining objects are the relational quotient completion (R)^eq, which freely adds quotients to a relational doctrine R, and the notion of R-projective object: an object P such that every arrow out of P lifts through any quotient arrow. A full subcategory G is an R-projective cover when every object admits a quotient arrow from an object in G. The biadjunction EQ ⊣ U_eq between relational doctrines and extensional doctrines with quotients underlies the characterization, while for monads the Eilenberg-Moore doctrine R^T, whose relations are those closed under the algebra structure, provides the bridge to free algebras.

What would settle it

Construct an extensional relational doctrine with quotients that has enough projectives but is not equivalent to the quotient completion of its projective subdoctrine; or exhibit a quotient-preserving monad T on such a doctrine for which the Eilenberg-Moore doctrine R^T does not satisfy the quotient-completion characterization, directly contradicting Corollary 3.8 and Theorem 4.4.

Watch

Extended reading notes

Core claim

The central result is that for an extensional relational doctrine R with quotients and a full subcategory G of its base category, G is an R-projective cover if and only if R is equivalent to (I_G^*R)^eq, the extensional quotient completion of the restriction of R to G. In other words, the doctrines that arise from the relational quotient completion are exactly the extensional relational doctrines with quotients and enough projectives. The paper further proves that for a quotient-preserving monad T, the free algebras generated by a projective cover form a projective cover of the Eilenberg-Moore doctrine R^T, so R^T is itself an extensional quotient completion of its restriction to those free

Load-bearing premise

The arguments rely on previously established facts, taken as given, that the relational quotient completion forms a biadjunction with the forgetful functor, and that the Eilenberg-Moore doctrine of a quotient-preserving monad is extensional and has quotients; if either of these prior results is flawed, the main theorems lose their foundation.

Editorial extensions

If this is right

Relational doctrines that come from the quotient completion are exactly those that have enough projectives, giving a clean recognition principle for when quotients can be freely added.
For any quotient-preserving monad on such a doctrine, the corresponding algebra doctrine is again a quotient completion of its restriction to free algebras over projectives, so algebraic presentations by generators and relations work at this level of generality.
The classical results on exact completion and monadic categories over exact categories are recovered as special cases, unifying two previously separate frameworks.
The theory applies to metric spaces and quantitative algebras, yielding new examples of doctrines that are quotient completions, such as those built from the list monad and the k-Lipschitz monad on metric spaces.
When quotient arrows split, every monad (not just quotient-preserving ones) gives rise to an algebra doctrine that is a projective cover of free algebras, mirroring the assumption that epimorphisms split in the classical setting.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The projective-cover characterization may serve as a completeness criterion for other doctrines: if a doctrine of interest can be shown to have enough projectives, then its internal logic and quotient structure are already captured by the free quotient completion of its projective core.
The finite-distance metric doctrine described in Remark 3.10 is presented as a counterexample to having enough projectives; a detailed inspection of that failure could suggest a general obstruction to being a quotient completion in terms of the absence of a projective cover.
The paper's framework suggests a notion of 'algebraic presentation' for relational doctrines: an object is presented by projective generators and a quotient relation, which may be formalized as a relational analogue of having a syntactic presentation.
The use of the list monad and the k-Lipschitz monad indicates that quantitative algebraic theories may correspond to quotient-preserving monads on the doctrine of metric relations; developing this correspondence could yield a theory of quantitative equational presentations.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this paper deserves a serious referee. The projective-cover characterization (Thm 3.7 / Cor 3.8) is real and not a routine extension: it subsumes Carboni–Vitale and Maietti–Rosolini, and the monad theorems (4.4, 4.16) genuinely extend Vitale’s result to relational doctrines, with quantitative algebra examples as new territory. The authors are working inside their own framework; the load-bearing dependence on [5,6,7] is openly visible. That is a mild weakness, not a red flag: [7] is published, the framework is not being invented on the fly, and the long proof in Section 2.2 plugging the missing reference for Example 2.9(1) is a good-faith repair.

Now the stress-test note. I think it partly does not land: the claimed omitted uniqueness in Thm 3.7 is not actually missing. The preceding argument for arrows \hat f establishes uniqueness of lifts using R-projectivity and fullness, and the same reasoning applies to h. What is genuinely missing is the explicit verification that [\hat q] is an effective descent quotient arrow: the paper checks the existence part of the universal property but does not spell out that its kernel equals G(ρ) and that Γ^⊥;Γ is the identity in (S)^eq. These likely follow from q being effective/descent and from identities in the quotient completion being the equivalence relations themselves, but the paper should say so. So I read the gap as real but smaller than the stress-test claims: an exposition fix, not a structural failure.

The weakest premise remains Prop 2.11 and the assertion that R^T has quotients for quotient-preserving monads. Both are cited from prior work, not reproved. The cited papers are real and well-matched, and I have no independent verification; if one of those earlier results is wrong, this paper collapses. For a referee report I would ask the authors to expand the kernel/descent check and to flag exactly which parts of Prop 2.11 they are invoking.

Bottom line: for people working on doctrines, exact completion, or quantitative algebra, this is worth reading and citing. The central claim is plausible and well-connected to external benchmarks. Send it to peer review.

Referee Report

2 major / 6 minor

Summary. The paper develops a notion of projective object and projective cover for relational doctrines with quotients, and characterizes the essential image of the extensional quotient completion as precisely those doctrines admitting a projective cover. The main characterization is Theorem 3.7, with Corollary 3.8 as the clean statement: an extensional relational doctrine with quotients R is equivalent to (I_G^*R)^eq if and only if G is an R-projective cover. This generalizes the classical exact-completion theorem and the elementary quotient completion theorem. The paper then applies this to Eilenberg-Moore doctrines of monads on relational doctrines: Theorem 4.4 shows that, for quotient-preserving monads, projective covers lift to covers by free algebras on the cover, and Theorem 4.16 gives a stronger version under the assumption that quotient arrows split. Several worked examples are given, including metric relations, bimodules over metric spaces, and assemblies.

Significance. If the main characterization is correct, it is a genuine and useful common generalization: it recovers the Carboni--Vitale exact-completion characterization and the Maietti--Rosolini elementary quotient completion, while also covering quantitative and metric examples not accessible through either prior framework. The paper contains a full proof of the identification of (Spn_C)^eq with JmSpn_{C^{ex/wlex}}, which is a useful contribution in itself, and the examples (assemblies, list monad on metric relations, and the k-Lipschitz monad on metric spaces) are substantial and instructive. The main proof is detailed, but one load-bearing verification in Theorem 3.7 is incomplete as written; the gap is local and appears fixable. The dependence on the authors' earlier framework is real but standard for a research paper in this area.

major comments (2)

[Section 3, proof of Theorem 3.7, (2)⇒(1), paragraph "We check that G preserves quotients"] The verification that G preserves quotients is incomplete. Starting from a quotient arrow q:X→W in R for ρ, the authors construct [h] and derive the equality Γ_{q̂};Γ_h;σ = Γ_f;σ. But to conclude that [q̂] is a quotient arrow for ρ̂, the definition in §2.1 requires more: (i) ρ̂ ≤ Γ_{q̂};Γ_{q̂}^⊥, (ii) the descent and effectiveness conditions Γ_{q̂}^⊥;Γ_{q̂}=d_{P_W} and ρ̂=Γ_{q̂};Γ_{q̂}^⊥, and (iii) uniqueness of [h]. Only existence of a lift is addressed; uniqueness and the effective-descent conditions are not shown. Without them, G is not proved to be a 1-arrow in EQRD, so the converse direction of Corollary 3.8 is not justified. This is a concrete gap. It is likely fixable: uniqueness should follow from the S-surjectivity of q̂ inherited from q and the faithfulness of the fully faithful F, and effectiveness should follow from the effective-descent property of q together with F being an
[Section 3, proof of Theorem 3.7, (2)⇒(1), construction of the pseudoinverse G] A second, related omission occurs in the same proof when the authors assert that the 2-arrows θ and φ are invertible. The existence of θ_X uses that both p_X and q_{⟨P_X,ρ_X⟩} are quotient arrows for the same relation F_{P_X,P_X}(ρ_X); invertibility should be justified by the universal property, but the uniqueness part is not spelled out. Similarly, the arrows f_{⟨X,ρ⟩} and g_{⟨X,ρ⟩} are claimed to be inverse to each other, yet the proof does not explicitly verify that the two composites are identities, rather than merely idempotent endomorphisms. These checks are needed to establish the equivalence in EQRD, not just an adjunction.

minor comments (6)

[Abstract and Introduction] Typo: "those obtained though the extensional quotient completion" should be "through".
[Throughout] Several cross-references use the wrong article type: in Lemma 2.13 the reference to "Theorem 2.12" should be to Lemma 2.12; in Corollary 2.14 "Theorem 2.13" should be Lemma 2.13; in the proof of Lemma 2.15 "Theorem 2.15" should be Lemma 2.15; in the proof of Proposition 4.1 "Theorem 2.7" should be Proposition 2.7; and after Corollary 3.8 "Theorem 2.10" should be Remark 2.10.
[Section 3, proof of Proposition 3.4] Reference to "Theorem 3.3" should be "Proposition 3.3".
[Section 2.2] Example 2.9(1) says the proof is postponed to Section 2.2, but Section 2.2 is not announced in the Introduction. A brief forward reference in the Introduction would help the reader.
[Section 3, Example 3.9] The phrase "the two equaitons above" has a typo ("equaitons"). Also, the notation for the realizability relation is not defined precisely; please clarify that r.a is Kleene equality.
[Section 4, Example 4.6] Typo: "we riterX" should be "we write X". Also, the phrase "the commutative triangle with the unit ensures that a0 is the identity" should specify that this is in the base category Met.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the projective-cover characterization is an independent theorem proved from the definitions; citations to earlier work supply background framework, not the target result.

full rationale

The paper's central claim (Theorem 3.7 / Corollary 3.8) is not a restatement of its inputs. The proof constructs a pseudoinverse G:R→(S)^eq explicitly from the projective-cover data, and verifies it is a 1-arrow in EQRD; this is real mathematical content, analogous to the standard exact-completion characterization [3]. No parameter is fitted and no theorem is assumed as input. The cited earlier framework ([5],[6],[7]) defines relational doctrines, the quotient completion construction, and the biadjunction EQ⊣U_eq; these are background facts, not the projective-cover characterization, and they are external to the claimed new result. The monadic results (Theorem 4.4, 4.16) likewise reduce to prior facts about Eilenberg-Moore doctrines (quoted from [6]) plus the paper's own Proposition 4.3 and Proposition 3.5; this is ordinary dependence on prior work, not circularity. The possible omission of uniqueness/effectiveness checks in the quotient-preservation verification in Theorem 3.7 is a proof-completeness concern, not a circular-reasoning concern. No step reduces by definition or by self-citation to the conclusion it is supposed to establish.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

No fitted parameters or hand-chosen constants appear; the paper is purely structural mathematics. The central theorems depend on prior results from the authors' own framework, plus the Axiom of Choice in one example.

assumptions (3)

domain assumption The relational quotient completion is a 2-functor EQ: RD to EQRD left biadjoint to the forgetful U_eq (Prop 2.11), taken from [7].
Used throughout Section 3 to define F# via the counit Q_R; if the biadjunction were not valid, the characterization theorem has no transpose.
domain assumption For a quotient-preserving monad T on R in EQRD, the Eilenberg-Moore doctrine R^T is extensional and has quotients, proved in [6].
Invoked at the start of Sec 4.1 and needed for Theorem 4.4 and Cor 4.17.
domain assumption Axiom of Choice: used in Example 3.9 to select representatives in each non-empty realization set when constructing realizers for partitioned assemblies.
The example depends on AC to show partitioned assemblies form a projective cover; the paper explicitly says 'Using the Axiom of Choice'.

invented entities (1)

R-projective object and R-projective cover (Def 3.1, 3.6)
purpose: Characterize which extensional relational doctrines with quotients are extensional quotient completions.
New definitions introduced in this paper; they recover regular projectives in the exact completion case, so they are grounded in existing theory, but there is no external empirical handle.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Projective covers, doctrines of algebras and the relational quotient completion." pith.science (2026). https://pith.science/paper/RDU6KDPY

@misc{pith2026260801915,
  author       = {Pith},
  title        = {Pith review of: Projective covers, doctrines of algebras and the relational quotient completion},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RDU6KDPY}},
  note         = {Machine review of arXiv:2608.01915}
}

read the original abstract

The extensional quotient completion of relational doctrines provides a common generalization of both the exact completion of categories with weak finite limits and the elementary quotient completion of existential elementary doctrines. In this paper, we study projective objects in relational doctrines with quotients, characterizing those obtained through the extensional quotient completion as those admitting a projective cover. We apply this result to doctrines of algebras for monads on relational doctrines with quotients, describing in which cases these arise as the extensional quotient completion of their restriction to (appropriate subcategories of) free algebras. This extends a similar result for monadic categories over exact ones, covering also more examples such as monads over the category of metric spaces giving rise to variants of quantitative algebras.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 2 canonical work pages

[7]

Dagnino, F

F. Dagnino, F. Pasquali, The relational quotient completion, Annals of Pure and Applied Logic 177 (6) (2026) 103728.doi:https://doi.org/ 10.1016/j.apal.2026.103728

arXiv 2026
[1]

Barr, Exact categories, Springer Berlin Heidelberg, Berlin, Heidel- berg, 1971, pp

M. Barr, Exact categories, Springer Berlin Heidelberg, Berlin, Heidel- berg, 1971, pp. 1–120.doi:10.1007/BFb0058580

work page doi:10.1007/bfb0058580 1971
[2]

Carboni, R

A. Carboni, R. Celia Magno, The free exact category on a left exact one, Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics 33 (1982) 295 – 301

1982
[3]

Carboni, E

A. Carboni, E. Vitale, Regular and exact completions, Journal of Pure and Applied Algebra 125 (1998) 79–117

1998
[4]

E. M. Vitale, On the characterization of monadic categories over set, Cahiers de Topologie et G´ eom´ etrie Diff´ erentielle Cat´ egoriques 35 (4) (1994) 351–358. URLhttp://eudml.org/doc/91556

1994
[5]

Dagnino, F

F. Dagnino, F. Pasquali, Quotients and extensionality in relational doctrines, in: M. Gaboardi, F. van Raamsdonk (Eds.), 8th Interna- tional Conference on Formal Structures for Computation and Deduction, FSCD 2023, Vol. 260 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2023, pp. 25:1–25:23.doi:10.4230/LIPIcs.FSCD.2023.25. 34

work page doi:10.4230/lipics.fscd.2023.25 2023
[6]

Dagnino, F

F. Dagnino, F. Pasquali, Cauchy-completions and the rule of unique choice in relational doctrines, Theory and Applications of Categories 43 (9) (2025) 243–280. URLhttp://www.tac.mta.ca/tac/volumes/43/9/43-09abs.html

2025
[8]

M. E. Maietti, G. Rosolini, Elementary quotient completion, Theory and Applications of Categories 27 (17) (2013) 445–463

2013

Show all 24 references

[9]

M. E. Maietti, F. Pasquali, G. Rosolini, Elementary Quotient Com- pletions, Church’s Thesis, and Partioned Assemblies, Logical Methods in Computer Science Volume 15, Issue 2 (Jun 2019).doi:10.23638/ LMCS-15(2:21)2019. URLhttps://lmcs.episciences.org/4302

2019
[10]

Mardare, P

R. Mardare, P. Panangaden, G. D. Plotkin, Quantitative algebraic rea- soning, in: M. Grohe, E. Koskinen, N. Shankar (Eds.), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, ACM, 2016, pp. 700–709.doi:10.1145/2933575.2934518

2016
[11]

Mardare, P

R. Mardare, P. Panangaden, G. D. Plotkin, On the axiomatizability of quantitative algebras, in: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, IEEE Computer Society, 2017, pp. 1–12.doi:10.1109/LICS.2017.8005102

2017
[12]

Ad´ amek, Varieties of quantitative algebras and their monads, in: C

J. Ad´ amek, Varieties of quantitative algebras and their monads, in: C. Baier, D. Fisman (Eds.), Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022, ACM, 2022, pp. 9:1–9:10.doi:10.1145/3531130.3532405

2022
[13]

Street, The formal theory of monads, Journal of Pure and Applied Algebra 2 (2) (1972) 149 – 168.doi:10.1016/0022-4049(72)90019-9

R. Street, The formal theory of monads, Journal of Pure and Applied Algebra 2 (2) (1972) 149 – 168.doi:10.1016/0022-4049(72)90019-9

1972 doi
[14]

Tarski, On the calculus of relations, Journal of Symbolic Logic 6 (3) (1941) 73–89.doi:10.2307/2268577

A. Tarski, On the calculus of relations, Journal of Symbolic Logic 6 (3) (1941) 73–89.doi:10.2307/2268577

1941 doi
[15]

Shulman, Framed bicategories and monoidal fibrations, Theory and Applications of Categories 20 (18) (2008) 650–738

M. Shulman, Framed bicategories and monoidal fibrations, Theory and Applications of Categories 20 (18) (2008) 650–738. 35

2008
[16]

F. W. Lawvere, Metric spaces, generalized logic, and closed categories, Rend. Sem. Mat. Fis. Milano 43 (1973) 135–166

1973
[17]

Maietti, G

M. Maietti, G. Rosolini, Quotient completion for the foundation of constructive mathematics, Logica Universalis 7 (3) (2013) 371–402. doi:10.1007/s11787-013-0080-2. URLhttps://doi.org/10.1007/s11787-013-0080-2

2013 doi
[18]

M. E. Maietti, F. Pasquali, G. Rosolini, Quasitoposes as elementary quotient completions (2024).arXiv:2111.15299. URLhttps://arxiv.org/abs/2111.15299

2024 arXiv
[19]

Tomita, Realizability Without Symmetry, in: C

H. Tomita, Realizability Without Symmetry, in: C. Baier, J. Goubault- Larrecq (Eds.), 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Vol. 183 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz- Zentrum f¨ ur Informatik,...

2021 doi
[20]

Abramsky, E

S. Abramsky, E. Haghverdi, P. J. Scott, Geometry of interaction and linear combinatory algebras, mscs 12 (5) (2002) 625–665.doi:10.1017/ S0960129502003730

2002
[21]

van Oosten, Realizability: An Introduction to its Categorical Side, Vol

J. van Oosten, Realizability: An Introduction to its Categorical Side, Vol. 152 of Studies in Logic and the Foundations of Mathematics, North Holland Publishing Company, 2008

2008
[22]

Carboni, Some free constructions in realizability and proof theory, Journal of Pure and Applied Algebra 103 (1995) 117–148

A. Carboni, Some free constructions in realizability and proof theory, Journal of Pure and Applied Algebra 103 (1995) 117–148

1995
[23]

Barr, Relational algebras, in: S

M. Barr, Relational algebras, in: S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, S. Swierczkowski (Eds.), Reports of the Midwest Category Seminar IV, Springer Berlin Heidelberg, Berlin, Heidelberg, 1970, pp. 39–55

1970
[24]

M. M. Clementino, W. Tholen, From lax monad extensions to topolog- ical theories, Textos Matematicos 46 (2014) 99–123. 36

2014

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [7]

Dagnino, F

F. Dagnino, F. Pasquali, The relational quotient completion, Annals of Pure and Applied Logic 177 (6) (2026) 103728.doi:https://doi.org/ 10.1016/j.apal.2026.103728

arXiv 2026

[2] [1]

Barr, Exact categories, Springer Berlin Heidelberg, Berlin, Heidel- berg, 1971, pp

M. Barr, Exact categories, Springer Berlin Heidelberg, Berlin, Heidel- berg, 1971, pp. 1–120.doi:10.1007/BFb0058580

work page doi:10.1007/bfb0058580 1971

[3] [2]

Carboni, R

A. Carboni, R. Celia Magno, The free exact category on a left exact one, Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics 33 (1982) 295 – 301

1982

[4] [3]

Carboni, E

A. Carboni, E. Vitale, Regular and exact completions, Journal of Pure and Applied Algebra 125 (1998) 79–117

1998

[5] [4]

E. M. Vitale, On the characterization of monadic categories over set, Cahiers de Topologie et G´ eom´ etrie Diff´ erentielle Cat´ egoriques 35 (4) (1994) 351–358. URLhttp://eudml.org/doc/91556

1994

[6] [5]

Dagnino, F

F. Dagnino, F. Pasquali, Quotients and extensionality in relational doctrines, in: M. Gaboardi, F. van Raamsdonk (Eds.), 8th Interna- tional Conference on Formal Structures for Computation and Deduction, FSCD 2023, Vol. 260 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2023, pp. 25:1–25:23.doi:10.4230/LIPIcs.FSCD.2023.25. 34

work page doi:10.4230/lipics.fscd.2023.25 2023

[7] [6]

Dagnino, F

F. Dagnino, F. Pasquali, Cauchy-completions and the rule of unique choice in relational doctrines, Theory and Applications of Categories 43 (9) (2025) 243–280. URLhttp://www.tac.mta.ca/tac/volumes/43/9/43-09abs.html

2025

[8] [8]

M. E. Maietti, G. Rosolini, Elementary quotient completion, Theory and Applications of Categories 27 (17) (2013) 445–463

2013