{"id":"1d7bb5e5-d9a5-4044-af3f-987a4b019921","arxiv_id":"2608.01915","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"In relational doctrines with quotients, the extensional quotient completion is characterized by the existence of a projective cover, and this transfers to doctrines of algebras for quotient-preserving monads.","lead":"This paper proves a general theorem about when a structure built from relations and quotients can be reconstructed from a smaller 'projective' part: exactly when every object is a quotient of a projective one. The same result is extended to algebras for monads, covering metric spaces and quantitative algebras and unifying earlier theorems for exact categories.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3.7's proof that G preserves quotients omits uniqueness and effectiveness checks; without these, Corollary 3.8's converse lacks justification.","rationale":"The reader flagged the reliance on prior results (Prop 2.11 and the EM-doctrine facts from [6]) as the weakest assumption. I agree that these are load-bearing, but they are published results and not directly testable within the paper. A more concrete and internal soft spot is the proof of Theorem 3.7's converse: the step showing that the constructed pseudoinverse G preserves quotients is incomplete. Quotient arrows in a relational doctrine require effectiveness and descent, as well as uniqueness of the induced map; the proof only sketches existence of a lift. This gap directly affects Corollary 3.8, the paper's central characterization, because if G does not preserve quotients, the equivalence cannot be stated in EQRD. The gap is likely fillable with a short argument, but as written it is a real omission that a careful reader must supply. Therefore I do not change the reader's CONDITIONAL verdict, but I add a specific internal check that would either confirm or dissolve the concern.","tokens_in":23503,"tokens_out":15670,"duration_ms":170241,"concrete_test":"Complete the missing steps in the preservation-of-quotients paragraph of Theorem 3.7: prove (i) Γ_[qhat]^⊥;Γ_[qhat]=d, (ii) ρ̂=Γ_[qhat];Γ_[qhat]^⊥, and (iii) uniqueness of [h] by left-composing Γ_qhat;Γ_h;σ=Γ_f;σ with Γ_qhat^⊥ and using S-surjectivity of qhat. If these verifications fail, the construction of G does not preserve quotients and the EQRD-equivalence in Corollary 3.8 is unproven.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In the proof of Theorem 3.7, direction (2)⇒(1), the authors construct a 1-arrow G:R→(S)^eq and then verify that G preserves quotients. Their verification only addresses existence of a lift [h] in the universal property; it does not establish that [qhat] is an effective descent quotient arrow. Specifically, they omit: (a) the descent condition Γ_[qhat]^⊥;Γ_[qhat]=d, (b) the effectiveness condition ρ̂=Γ_[qhat];Γ_[qhat]^⊥, and (c) uniqueness of the lift [h]. These are all required by the definition of quotient arrow in Section 2.1. Without them, G cannot be shown to be a 1-arrow in EQRD, so the converse of Corollary 3.8 (that a projective cover forces R to be an extensional quotient completion) is not justified. The uniqueness can likely be supplied by using S-surjectivity of qhat (inherited from q being a quotient and F an isomorphism) to cancel Γ_qhat from the equation Γ_qhat;Γ_h;σ=Γ_f;σ, but this argument is not written. This is a concrete gap in the core proof of the paper's main characterization.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":23812,"tokens_out":5477,"duration_ms":67635,"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":[{"comment":"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":"Section 3, proof of Theorem 3.7, (2)⇒(1), paragraph \"We check that G preserves quotients\""},{"comment":"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.","section":"Section 3, proof of Theorem 3.7, (2)⇒(1), construction of the pseudoinverse G"}],"minor_comments":[{"comment":"Typo: \"those obtained though the extensional quotient completion\" should be \"through\".","section":"Abstract and Introduction"},{"comment":"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":"Throughout"},{"comment":"Reference to \"Theorem 3.3\" should be \"Proposition 3.3\".","section":"Section 3, proof of Proposition 3.4"},{"comment":"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":"Section 2.2"},{"comment":"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":"Section 3, Example 3.9"},{"comment":"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.","section":"Section 4, Example 4.6"}],"recommendation":"major_revision","confidential_remarks":"The paper is within the scope of the journal and the main result is attractive, but the referee is not able to certify the central theorem from the proof as written because of the missing quotient-preservation checks in Theorem 3.7. The reliance on the authors' earlier results [6,7] is acceptable if those results are indeed published with full proofs, but the authors should state them precisely enough that the reader can see exactly which statements are being imported. The Example 3.9 use of the Axiom of Choice is worth a remark, since the paper otherwise works in a purely constructive setting for realizability; it is not an error, but the shift in ambient logic should be explicit."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nNow 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.\n\nThe 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.\n\nBottom 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.","headline":"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.","tokens_in":24298,"tokens_out":3917,"would_cite":true,"duration_ms":48002,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18A32","18D05","18E10","18C20","03G15","06F35"],"pacs":[],"model":"deepseek-v4-flash","headline":"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","keywords":["relational doctrines","quotient completion","projective covers","Eilenberg-Moore doctrines","monads","exact completion","quantitative algebras","metric spaces"],"falsifier":"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.","tokens_in":23392,"feed_emoji":"➗","tokens_out":2335,"duration_ms":29331,"temperature":0.7,"pith_summary":"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.","feed_headline":"Quotient completions are exactly doctrines with projective covers","feed_subtitle":"Algebra doctrines over free algebras now include metric and quantitative examples, generalizing exact completion.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Projective covers characterize relational quotient completions","Quotient completion = doctrines with enough projectives","Free algebras yield covers, extending quotient completions","Projective covers prove algebra doctrines are quotient completions","Exact completion generalizes to metric algebras via projective covers"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Projective covers characterize relational quotient completions","Quotient completion = doctrines with enough projectives","Free algebras yield covers, extending quotient completions","Projective covers prove algebra doctrines are quotient completions","Exact completion generalizes to metric algebras via projective covers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000221,"raw_usage":{"total_tokens":1233,"prompt_tokens":639,"completion_tokens":594,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":383,"completion_tokens_details":{"reasoning_tokens":520}},"tokens_in":383,"tokens_out":594,"duration_ms":7260,"temperature":1.0,"reasoning_tokens":520,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T18:14:14.596153+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}