{"id":"8145769e-7087-468b-a4b5-088feb1536ba","arxiv_id":"1909.00172","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Finitely presented promonoidal structures on an additive category extend uniquely to right exact monoidal structures on the associated Freyd category, equivalently on finitely presented functors.","lead":"This mathematics paper shows how certain tensor product data on a small additive category lift uniquely to right exact tensor products on its category of finitely presented functors, using Freyd categories and a new multilinear universal property. The construction is explicit and implemented in the CAP computer algebra project, giving a unified computational approach to tensor products of finitely presented modules and graded modules.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 2.2.2 states a left-exactness sequence as a right-exactness criterion; since the universal property Theorem 2.3.1 rests on it, the lifting proof is not valid as written.","rationale":"The paper develops a constructive multilinear universal property for Freyd categories and uses it to lift f.p. promonoidal structures to right exact monoidal structures, comparing with Day convolution. The reader identified the equivalence A(A) ≅ fp(A^op, Ab) as the weakest assumption, but that is a cited standard result. The real soft spot is internal: Lemma 2.2.2, a key criterion used throughout the proof of the universal property, is stated with an exact sequence that characterizes left exactness rather than right exactness, and its proof is only a sketch. The natural arrow for right exactness goes from F(a) to F(coker α), not from F(coker α) to F(a), so the sequence as written is not well-formed. This is not a minor typo; the entire constructive framework in Section 2.3 uses this lemma to prove that the extended functors are right exact and that the equivalence is an equivalence. Without a corrected lemma, the lifting results of Section 3 (Lemmas 3.3.2, 3.3.4, 3.3.6) and the Day convolution comparison (Theorem 4.2.1) lack a valid foundation. The paper's computational claims and examples may well be correct, but the submitted proof does not establish the central claim. The appropriate verdict is CONDITIONAL: the paper should be accepted only after Lemma 2.2.2 is corrected and the subsequent proofs are revised to use the correct right-exactness sequence.","tokens_in":19428,"tokens_out":17003,"duration_ms":200054,"concrete_test":"Instantiate Lemma 2.2.2 in the case n = 1 with A = Ab, F = −⊗_Z Z/2, and α: Z → Z the multiplication by 2. Right exactness of F implies F(coker α) ≅ coker(F(α)) = Z/2. Compare the sequence stated in the lemma, 0 → F(coker α) → F(a) → F(b), with the actual right-exactness sequence F(b) → F(a) → F(coker α) → 0. Verify whether the second arrow in the lemma's sequence is even a well-defined natural map. If, as expected, there is no natural map F(coker α) → F(a), the lemma is false as written; if a corrected sequence is needed, re-run the proofs of Lemmas 2.3.3 and 2.3.5 with the corrected statement to confirm the universal property still holds.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central technical tool is Theorem 2.3.1, whose proof uses Lemma 2.2.2. As stated, Lemma 2.2.2 claims that a multilinear functor F is right exact iff for every tuple of morphisms (b_i → a_i), the sequence 0 → F(coker α_1, ..., coker α_n) → F(a_1, ..., a_n) → ⊕_{j=1}^n F(a_1, ..., a_{j-1}, b_j, a_{j+1}, ..., a_n) is exact. For n = 1, this would say that F(coker α) is a subobject of F(a), i.e., that F is left exact. But right exactness (Definition 2.2.1) requires the natural map F(a) → F(coker α) to exhibit F(coker α) as the cokernel of F(b) → F(a). The exact sequence characterizing right exactness is ⊕_j F(a_{n−j}; b_j) → F(a_n) → F(coker α_n) → 0, not the sequence in the paper. Moreover, the second arrow in the stated sequence has no natural definition: there is no canonical map F(coker α) → F(a). This lemma is used in Lemma 2.3.3 to prove right exactness of the extended functor, in Lemma 2.3.5 to prove the equivalence of the universal property, and indirectly in all lifting lemmas of Section 3 and in Theorem 4.2.1. If Lemma 2.2.2 is not replaced by a correct right-exactness criterion, the proof of the paper's main claim—that every f.p. promonoidal structure extends to a right exact monoidal structure on the Freyd category—does not go through. The issue is internal to the argument, not a matter of disagreement with prior consensus.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a constructive theory of right exact tensor products on the category of finitely presented functors fp(A^op,Ab), working mainly in the equivalent language of Freyd categories A(A). The central technical tool is a multilinear 2-categorical universal property of Freyd categories (Theorem 2.3.1). Using this property, the authors define finitely presented promonoidal structures on an additive category A and show that they extend to right exact monoidal, braided monoidal, and closed structures on A(A) (Section 3.3). They then compare the resulting tensor product with Day convolution restricted to finitely presented functors (Theorem 4.2.1). The final sections give applications to finitely presented modules, iterated Freyd categories, free abelian categories, and explicit constructive implementations of the tensor product, associator, unitors, and braiding.","tokens_in":19789,"tokens_out":12702,"duration_ms":111818,"significance":"If the proofs are repaired, the paper would provide a useful unified and computational framework for constructing right exact tensor products on categories of finitely presented functors. Its emphasis on explicit constructions and on implementability in the CAP project is a genuine strength, as is the connection established with Day convolution. The main theorems are standard in spirit and likely correct, but the proof of the central universal property contains a load-bearing technical error, so the present version is not acceptable without revision.","major_comments":[{"comment":"The exactness criterion stated in Lemma 2.2.2 is not a criterion for right exactness. For n=1 it asserts exactness of 0 -> F(coker alpha) -> F(a) -> F(b), which says that F(coker alpha) is the kernel of F(a) -> F(b); right exactness, as defined in Definition 2.2.1, instead requires the sequence F(b) -> F(a) -> F(coker alpha) -> 0 to be exact. The proof of Lemma 2.3.3 checks the stated left-exact sequence, and Lemma 2.3.5 explicitly invokes Lemma 2.2.2, so the proof of Theorem 2.3.1 and all subsequent lifting results (Lemmas 3.3.2, 3.3.4, 3.3.6, and Theorem 4.2.1) do not go through as written. The lemma should be replaced by the correct right-exactness criterion, e.g. exactness of the sequence bigoplus_j F(a^{n-j}; b_j) -> F(a^n) -> F(coker alpha_n) -> 0, or right exactness of the extended functor should be proved directly from Definition 2.2.1.","section":"Lemma 2.2.2; used in Lemmas 2.3.3 and 2.3.5"},{"comment":"There is an apparent direction mismatch in the presentation of the extended functor. If objects of A(A) are written as A = (a <- rho_a r_a) with rho_a: r_a -> a, then A is the cokernel of rho_a, and a right exact extension should be presented as coker( bigoplus_j F(a^{n-j}; r_{a_j}) -> F(a^n) ). The displayed formula in Construction 2.3.2 and the exact rows 0 -> widehat F(A^n) -> F(a^n) -> bigoplus_j F(a^{n-j}; r_{a_j}) instead present widehat F(A^n) as a kernel. This direction error is consistent with the incorrect statement of Lemma 2.2.2 and should be corrected in the same revision.","section":"Construction 2.3.2 and Lemma 2.3.3"}],"minor_comments":[{"comment":"In Definition 2.1.1 the category is written as ApPq in two places; this should be ApAq.","section":"Definition 2.1.1"},{"comment":"The quantifiers in Lemmas 3.3.1 and 3.3.5 say 'for all a,b,c in ApAq' and 'for all a,b in ApAq', but the proassociator and probraiding are only defined for objects of A; these should read 'for all a,b,c in A' and 'for all a,b in A'.","section":"Lemmas 3.3.1 and 3.3.5"},{"comment":"The displayed description of Hom_R(R/<z>, R) in Equation (9) is typeset in a garbled way and should be re-set so that the reader can see the intended R-module structure.","section":"Example 5.1.2, Equation (9)"},{"comment":"Even after correcting the statement, the proof of the converse direction is only described as a diagram chase; since this lemma is load-bearing, a fuller proof should be supplied for the corrected criterion.","section":"Lemma 2.2.2 proof"},{"comment":"The proof is labeled 'Proof by induction' and is very terse; the induction step for the closed monoidal structure on ApXq should at least cite the relevant lemmas from Section 3.3 explicitly.","section":"Theorem 5.2.1"}],"recommendation":"major_revision","confidential_remarks":"The central theorem is a known universal property and the overall strategy of the paper is sound, so the errors in Lemma 2.2.2 and Construction 2.3.2 appear repairable within the scope of the manuscript. I recommend major revision rather than rejection, but the revised version must fix the direction of the right-exactness criterion and re-verify all proofs that rely on it."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe one thing you should know: this paper has a promising framework for right exact tensor products on fp(A^op, Ab) via Freyd categories, but the proof of the central technical tool, Theorem 2.3.1, relies on Lemma 2.2.2, and that lemma as stated is not a right-exactness criterion. For n=1 it would say F(coker α) is a subobject of F(a), which is left exactness. The sequence should run ⊕_j F(a_{n−j}; b_j) → F(a_n) → F(coker α_n) → 0. The lemma is used in Lemma 2.3.3 and Lemma 2.3.5, and the lifting results in Section 3 inherit the flaw. So the main theorem—that every f.p. promonoidal structure extends to a right exact monoidal structure—is not established as written.\n\nThat said, the paper is not a waste. The notion of f.p. promonoidal structure is natural, the explicit lifting constructions are useful, and the Day convolution comparison in Theorem 4.2.1 is honest and illuminating. The CAP implementation and concrete examples in Section 5 give the work practical value. The citation practice is fine: the self-citations to Posur's constructive Freyd categories are appropriate and not inflated.\n\nThe soft spots are concentrated in Sections 2.2–2.3. Besides the lemma statement, the proof of Lemma 2.2.2 is sketched as a 'diagram chase' without enough detail. Theorem 3.3.8 relies on weak kernels and is not fully constructive, which contrasts with the paper's advertised constructivity. If Lemma 2.2.2 is fixed—and I think it can be, since the intended criterion is standard—the rest of the formal development may well be sound.\n\nMy bottom line: this deserves serious refereeing, but not acceptance in its current form. Have the authors correct the lemma and re-check Section 2.3, and this could be a solid contribution.","headline":"The constructive framework is valuable and the Day-convolution comparison is illuminating, but the proof of the main universal property rests on a misstated right-exactness lemma that must be corrected.","tokens_in":20324,"tokens_out":6239,"would_cite":false,"duration_ms":56675,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18E10","18E05","18A25"],"pacs":[],"model":"deepseek-v4-flash","headline":"Every finitely presented promonoidal structure on a small additive category extends to a right exact monoidal structure on the category of finitely presented functors, and the lifted tensor coincides with Day convolution.","keywords":["Freyd category","finitely presented functor","computable abelian category","promonoidal structure","monoidal structure","Day convolution","right exact tensor product","constructive category theory"],"falsifier":"A concrete test: take $R = \\mathbb{Q}[x]$, $A = \\operatorname{Rows}_R$, and the protensor $T(A,B) = A \\otimes_R B$; build the associator by Construction 5.4.6 and check the pentagon identity on four finitely presented non-projective modules such as $\\mathbb{Q}[x]/(x)$, $\\mathbb{Q}[x]/(x^2)$, $\\mathbb{Q}[x]/(x-1)$, and $\\mathbb{Q}[x]/(x^2+x+1)$ — any failure of the pentagon diagram in $R\\text{-}\\mathrm{fpmod}$ would disprove Lemma 3.3.2. A second test for Theorem 4.2.1: pick a non-representable finitely presented functor $F$ and a functor $G$, compute the Day convolution $F \\ast_P G$ from the defining coend, and compare it with the lifted tensor $F \\,\\widehat{\\otimes}_T\\, G$; the paper predicts a natural isomorphism for all such pairs.","tokens_in":19205,"feed_emoji":"➕","tokens_out":26961,"duration_ms":186997,"temperature":0.7,"pith_summary":"The paper establishes that a tensor product on the category of finitely presented functors over a small additive category can be specified by finite data on the base objects and then extended, constructively, to a genuine right exact tensor product on all finitely presented functors. The input data, called a finitely presented promonoidal structure, is a bilinear protensor $T\\colon A \\times A \\to \\mathcal{A}(A)$ together with associativity, unit, and braiding isomorphisms whose coherence identities are only required on objects of $A$. The main result is that such data lifts to a right exact monoidal, braided monoidal, or closed monoidal structure on the Freyd category $\\mathcal{A}(A)$, which is equivalent to the category $\\mathrm{fp}(A^{\\mathrm{op}}, \\mathrm{Ab})$ of finitely presented functors. Since the constructions use only cokernels of finite data, the lifted tensor products are computable, and Theorem 4.2.1 shows they coincide with the restriction of Day convolution. The payoff is a unified machine: one mechanism yields tensor products on finitely presented modules, finitely presented graded modules, iterated Freyd categories, and free abelian categories, a setting relevant to algebraic motives.","feed_headline":"Finitely presented tensor products lift from objects to functors","feed_subtitle":"Coherence is verified once on base objects; the lifted tensor matches Day convolution.","key_machinery":"The load-bearing machinery is the multilinear 2-categorical universal property of Freyd categories (Theorem 2.3.1). A Freyd category $\\mathcal{A}(A)$ is the universal way to adjoin cokernels to an additive category $A$: objects are morphisms $\\rho\\colon a \\leftarrow r$ of $A$, thought of as formal cokernels, and $\\mathcal{A}(A) \\simeq \\mathrm{fp}(A^{\\mathrm{op}}, \\mathrm{Ab})$. The theorem says that an $n$-ary multilinear functor $F\\colon A^n \\to B$ into a category with cokernels extends to exactly one right exact functor $\\widehat{F}\\colon \\mathcal{A}(A)^n \\to B$, given on formal cokernels as $\\widehat{F}(A_1,\\dots,A_n) = \\operatorname{coker}\\big((F(\\mathrm{id}_{A_i}; \\rho_{A_i}))_i\\big)$. Because this is an equivalence of functor categories, natural transformations — and hence associators, unitors, braidings, and the coherence identities they must satisfy — are uniquely determined by their restrictions to the embedded objects of $A$. The paper packages the input as a finitely presented promonoidal structure and lets this universal property carry every coherence proof: each identity on $\\mathcal{A}(A)$ reduces to its restricted version on $A$, and the extensions are given by explicit cokernel constructions that a computer can execute.","core_discovery":"The paper's central claim is that finitely presented promonoidal structures on an additive category are exactly the restrictions to the embedded $A$ of right exact monoidal structures on the Freyd category $\\mathcal{A}(A)$, and that the extension is canonical. Concretely, a finitely presented proassociator $\\Pi$ extends to an associator $\\widehat{\\Pi}$, finitely presented prounitors extend to unitors, and a finitely presented probraiding extends to a braiding (Lemmas 3.3.1 through 3.3.6); the pentagon, triangle, and hexagon identities hold on all of $\\mathcal{A}(A)$ exactly when their restrictions to $A$ hold. The engine is Theorem 2.3.1, a multilinear 2-categorical universal property: $n$-ary multilinear functors from $A^n$ to a category with cokernels correspond bijectively to right exact $n$-ary functors from $\\mathcal{A}(A)^n$, so every natural transformation between right exact multifunctors is determined by its values on $A$. Theorem 4.2.1 then shows the lifted tensor product, viewed on $\\mathrm{fp}(A^{\\mathrm{op}}, \\mathrm{Ab}) \\simeq \\mathcal{A}(A)$, is naturally isomorphic to the Day convolution built from the profunctor $P(a,b,c) = T(a,b)(c)$ and restricted to finitely presented functors; the paper's constructions are therefore the finitely presented shadow of Day convolution, obtained without coends.","pith_inferences":["My inference: the restricted-coherence strategy should extend to any algebraic structure whose defining identities are equalities of natural transformations between right exact multilinear functors, for example Hopf-like structures or module actions, since Theorem 2.3.1 reduces each such identity to its values on the embedded base category $A$.","My inference: Theorem 4.2.1 suggests a 'finitely presented Day convolution' computed directly on $\\mathrm{fp}(A^{\\mathrm{op}}, \\mathrm{Ab})$: given finite presentations of $F$ and $G$, the defining coend collapses to a finite colimit, which would make Day convolution executable over bases where internal homs fail.","My inference: one testable consequence of the cokernel-based lifting is an invariance statement the paper leaves implicit: different small generating categories inside the same Freyd category that present the same finitely presented functors should induce naturally isomorphic right exact tensor products."],"forward_implications":["Monoidal structures propagate through the hierarchy of iterated Freyd categories: if $A$ is additive, closed monoidal, and has weak kernels and weak cokernels, then so does every iterated Freyd category of $A$ (Theorem 5.2.1), and every promonoidal structure on $A^{\\mathrm{op}}$ yields a right exact monoidal structure on the free abelian category of $A$ (Theorem 5.3.1).","The paper's tensor product on finitely presented functors is computable: Section 5.4 gives explicit formulas for tensoring morphisms, unitors, associators, and braidings purely in terms of the protensor data, which is exactly the algorithmic content needed for computer implementation.","For finitely presented modules over a ring $R$, the construction recovers the usual tensor product, and Example 5.1.1 shows why the protensor $T$ genuinely takes values in $\\mathcal{A}(A)$ rather than in $A$: tensoring two row modules with a fixed module $M$ can land outside the row modules when $M$ is not a row module.","The lifted monoidal structure can fail to be closed even when the original category is closed: Example 5.1.2 exhibits a closed monoidal category without weak kernels, the ring $\\mathbb{Q}\\langle x_i, z\\rangle/\\langle x_i z\\rangle$, whose induced tensor product on the Freyd category has no right adjoint, so internal homs must be checked separately.","On finitely presented functors, the Day-convolution comparison (Theorem 4.2.1) means the f.p. promonoidal data determine the associator, unitors, and braiding of the restricted Day convolution up to natural isomorphism, so the coherence of the convolution on f.p. functors is governed entirely by representable values."],"supporting_citations":[{"why":"Supplies the Freyd category construction, its cokernels, and the abelianity criterion (weak kernels) on which the paper's categorical framework rests.","marker":"[Fre66]"},{"why":"Coins the term Freyd category and supplies the iterated-Freyd description of free abelian categories used in Theorem 5.3.1.","marker":"[Bel00]"},{"why":"Provides the constructive treatment of Freyd categories behind the equivalence $\\mathcal{A}(A) \\simeq \\mathrm{fp}(A^{\\mathrm{op}}, \\mathrm{Ab})$ and the identification of $\\operatorname{Rows}_R$ with finitely presented modules.","marker":"[Pos17]"},{"why":"Introduces Day convolution and closed monoidal structures on functor categories; it is the comparison target of Theorem 4.2.1 and the source of the right-adjoint formulas in Section 4.1.","marker":"[Day70]"},{"why":"Reformulates promonoidal categories in profunctor language, the classical backdrop that Remark 4.2.2 connects to the paper's finitely presented prostructures.","marker":"[Day74]"},{"why":"Supplies the coherence theorem used in Example 5.1.1 to recognize the associator of $A \\otimes_R M \\otimes_R B$, and standard coend calculus for Section 4.","marker":"[ML98]"},{"why":"The motivic construction whose lifting result is recovered as a corollary of the paper's extension procedure in Theorem 5.3.1.","marker":"[BHP18]"},{"why":"The companion constructive-category-theory software that implements the monoidal special case of the constructions in Section 5.4.","marker":"[BP19]"}],"fun_headline_variants":["Right exact tensor products on finitely presented functors via Freyd","Multilinear universal property lifts tensor products to fp functors","Finitely presented tensor products match Day convolution canonically","No coends needed: fp tensor products equal restricted Day convolution"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is the constructive equivalence between the Freyd category $\\mathcal{A}(A)$ and the category $\\mathrm{fp}(A^{\\mathrm{op}}, \\mathrm{Ab})$ of finitely presented functors (Theorem 2.1.6): every claim about tensor products is proved in $\\mathcal{A}(A)$ and transferred to finitely presented functors through this equivalence, so if the equivalence were not constructive the claimed computable tensor products would not follow; a secondary standing premise is that $A$ is small, needed for the Day-convolution coends in Section 4.","fun_headline_variants_meta":{"raw":{"variants":["Right exact tensor products on finitely presented functors via Freyd","Multilinear universal property lifts tensor products to fp functors","Finitely presented tensor products match Day convolution canonically","No coends needed: fp tensor products equal restricted Day convolution"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000248,"raw_usage":{"total_tokens":1525,"prompt_tokens":902,"completion_tokens":623,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":518,"completion_tokens_details":{"reasoning_tokens":554}},"tokens_in":518,"tokens_out":623,"duration_ms":412322,"temperature":1.0,"reasoning_tokens":554,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T06:00:42.606051+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete test: take $R = \\mathbb{Q}[x]$, $A = \\operatorname{Rows}_R$, and the protensor $T(A,B) = A \\otimes_R B$; build the associator by Construction 5.4.6 and check the pentagon identity on four finitely presented non-projective modules such as $\\mathbb{Q}[x]/(x)$, $\\mathbb{Q}[x]/(x^2)$, $\\mathbb{Q}[x]/(x-1)$, and $\\mathbb{Q}[x]/(x^2+x+1)$ — any failure of the pentagon diagram in $R\\text{-}\\mathrm{fpmod}$ would disprove Lemma 3.3.2. A second test for Theorem 4.2.1: pick a non-representable finitely presented functor $F$ and a functor $G$, compute the Day convolution $F \\ast_P G$ from the defining coend, and compare it with the lifted tensor $F \\,\\widehat{\\otimes}_T\\, G$; the paper predicts a natural isomorphism for all such pairs.","supporting_citations":[],"review_version":1}