Pith. sign in

REVIEW 4 major objections 5 minor 1 cited by

On the squares functor and the Gaitsgory-Rozenblyum conjectures

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Pith's one-line read The paper proves the final open Gaitsgory–Rozenblyum conjecture: the squares functor and the Gray tensor product are linked by a natural equivalence.

desk verdict Credible proof of the last Gaitsgory–Rozenblyum conjecture, with a real black-box dependency on the authors' own unpublished preprints. read the letter →

arxiv 2507.07807 v2 pith:53ULBHYG submitted 2025-07-10 math.CT math.AT

classification math.CTmath.AT MSC 18N1018N60
keywords (∞2)-categoriesdouble∞-categoriesGraytensorproductsquaresfunctorcompanionsdirectedČechnerveGaitsgory–Rozenblyumconjectureshighercategorytheory
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 proves the final unresolved conjecture in the $(\infty,2)$-categorical foundations of Gaitsgory and Rozenblyum: for any $(\infty,2)$-categories $C,D,E$ there is a natural equivalence $\mathrm{Map}(C^h\times D^v,\mathrm{Sq}(E))\simeq \mathrm{Map}(C\otimes D,E)$, which is equivalently the statement $\mathrm{Gr}(C^h\times D^v)\simeq C\otimes D$. It also establishes the universal property of the squares functor: $\mathrm{Sq}(C)$ is the double $\infty$-category freely obtained from the vertical inclusion $C^v$ by adjoining companions, with a dual statement for the horizontal inclusion. The result closes the last of eight conjectures from [GR17], and the uniqueness of the comparison follows because the Gray tensor product has no nontrivial automorphism. A reader should care because the Gray tensor product is the central device for controlling lax phenomena in higher category theory, and this gives it a description purely in terms of squares and double categories.

What carries the argument

The machine at the center is the squares functor $\mathrm{Sq}$, which sends an $(\infty,2)$-category $C$ to the double $\infty$-category whose objects are the objects of $C$, whose horizontal and vertical arrows are the arrows of $C$, and whose 2-cells are lax commutative squares in $C$; its left adjoint $\mathrm{Gr}$ realizes a double $\infty$-category as an $(\infty,2)$-category. Around this sit the directed Čech nerve of a filtration, which is the relative form of squares, and the notion of a companion: a horizontal arrow $F$ companion to a vertical arrow $f$ is witnessed by a unit and a counit satisfying triangle identities. The proof reduces arbitrary $(\infty,2)$-categories to globular sums and assembles $\mathrm{Gr}(C^h\times D^v)$ from pushouts, using Maehara's Gray tensor product on space-valued presheaves over $\Theta_2$ to identify the resulting colimit with $C\otimes D$.

What would settle it

The quickest check is to compute both sides for the first non-trivial shapes: take $C=[1]$, $D=[1]$, and $E=[1;1]$, and compare $\mathrm{Map}(C^h\times D^v,\mathrm{Sq}(E))$ with $\mathrm{Map}(C\otimes D,E)$; if they are not equivalent, Theorem B is false. The paper's own reduction says it suffices to check globular sums, so a reader could also verify the pushout decompositions of Lemmas 4.6 and 4.8 directly in the category of gaunt 2-categories.

Watch

Extended reading notes

Core claim

The central claim is Theorem B: the squares functor and the Gray tensor product are governed by the same universal property. Concretely, for $(\infty,2)$-categories $C,D,E$, mapping out of the product of the horizontal inclusion of $C$ and the vertical inclusion of $D$ into the squares of $E$ is naturally equivalent to mapping out of $C\otimes D$ into $E$. Since $\mathrm{Sq}$ has a left adjoint $\mathrm{Gr}$, this is equivalent to $\mathrm{Gr}(C^h\times D^v)\simeq C\otimes D$, settling [GR17, Proposition 10.4.5.4]. The paper also proves Theorem A, the universal property of squares: functors $\mathrm{Sq}(C)\to Q$ are exactly functors $C^v\to Q$ that send every arrow of $C$ to a vertical arrow of $Q$ admitting a companion, and the analogous statement for horizontal arrows holds under a local completeness assumption. Because Proposition 2.18 shows the Gray tensor product has no nontrivial endomorphisms, the comparison map originally written down by Gaitsgory and Rozenblyum must coincide with the one produced here.

Load-bearing premise

The proof takes several results from the authors' earlier preprints as black boxes—effectivity of generalized double ∞-categories, the companion theorems, and the identification of the Gray tensor product used here with Gaitsgory–Rozenblyum's—so the central equivalence stands only if those cited theorems are correct.

Editorial extensions

If this is right

  • All eight Gaitsgory–Rozenblyum conjectures about the Gray tensor product and the squares functor are now resolved.
  • The Gray tensor product can be described as $\mathrm{Gr}(C^h\times D^v)$, giving a double-categorical description of the tensor product.
  • Theorem A gives a usable mapping-space criterion: maps out of $\mathrm{Sq}(C)$ are detected by maps out of $C^v$ that preserve companions, and dually for $C^h$.
  • Any comparison between different models of the Gray tensor product is unique, because the bifunctor has no nontrivial endomorphisms.

Reading between the lines

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

  • By the same density argument, the equivalence $\mathrm{Gr}(C^h\times D^v)\simeq C\otimes D$ is likely to extend to $(\infty,n)$-categories with an $n$-dimensional squares functor, but the paper does not claim this.
  • Because the proof invokes effectivity of generalized double $\infty$-categories and the companion theorems as black boxes, a fully self-contained proof would need those results checked independently; the paper does not provide that check.
  • The uniqueness of the comparison map suggests that any construction of a Gray tensor product satisfying the same universal property will automatically agree with Maehara's, which may simplify future comparisons among tensor products.
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.

Referee Report

4 major / 5 minor

Summary. The paper develops the theory of the squares functor Sq on (∞,2)-categories and its left adjoint Gr, in order to resolve the last open Gaitsgory–Rozenblyum conjecture. The two main advertised results are: Theorem A, a universal property of Sq(C) as the free double ∞-category obtained by adding companions to the vertical inclusion Cv, and Theorem B, the natural equivalence Map(Ch×Dv, Sq(E)) ≃ Map(C⊗D, E), equivalently Gr(Ch×Dv) ≃ C⊗D. The proof of Theorem B proceeds by density arguments reducing to globular sums, a series of pushout computations, and the uniqueness of endomorphisms of the Gray tensor product. The paper also contains a status table for all eight conjectures from [GR17].

Significance. If correct, the paper settles a long-standing conjecture in the (∞,2)-categorical foundations of derived algebraic geometry, and it provides a clean statement of the universal property of the squares construction. The strategy is well organized, and the reduction to generators of the form [n;m] together with the uniqueness argument via Proposition 2.18 are valuable contributions. However, the proof is not self-contained: several load-bearing lemmas are imported from unpublished preprints by the same authors, notably the epimorphism claims of Lemma 4.4. The paper therefore presents a convincing architecture, but the verification burden is not fully met within the manuscript as it stands.

major comments (4)
  1. [Section 4, Lemma 4.4] The epimorphism claims for the canonical maps a⊗b→a×b and a×b→b are the central pivot of the proof of Theorem 4.1: they are used to obtain uniqueness of the dashed factorization in Construction 4.5, to apply Lemma 4.3 in Lemma 4.6, and to pass from the outer pushout to the right pushout in Lemma 4.8. Yet Lemma 4.4 is proved only by citing [Lou25, Lemma 1.6.12] and [Lou24, Proposition 2.2.1.50], both unpublished preprints by the first author. Please state the precise results being cited and show that they apply to the combinations of globular sums used here, or give a direct proof of these epimorphism assertions. Without this, the chain supporting Gr(Ch×Dv)≃C⊗D is not established in the paper.
  2. [Section 4, Lemma 4.8] The proof of Lemma 4.8 ends with the assertion that the square τ0[m]×[k] → τ0[m]; [m]×[k] → [m] is a pushout in ∞Cat, justified only by the phrase 'as can be directly verified by reducing to m=k=1'. A reduction from arbitrary m,k to m=k=1 requires an argument showing that the square is preserved under the operations that build general m,k, and that argument is not supplied. Since Lemma 4.8 is used in Lemma 4.9 and in the final colimit computation of Theorem 4.1, please provide the missing verification or a proof that the reduction is legitimate.
  3. [Section 3, Theorem 3.10] Theorem 3.10, which is the foundation for Theorem A, is proved by a direct appeal to [Lou25, Theorem 3.4.1], and the intermediate Lemma 3.13 is dismissed with 'one may readily verify' while Lemma 3.15 invokes [Rui25a, Theorem 4.13]. Since Theorem A is one of the two advertised theorems of the paper, these inputs should either be proved in the manuscript or stated explicitly as assumptions with precise statements of the cited results. As written, the reader cannot independently check the main theorem of Section 3.
  4. [Section 2, Proposition 2.22 and Lemma 2.20] The paper's claim that the Gray tensor product used here coincides with the one in [GR17] proceeds through Proposition 2.22, whose proof relies on [Lou25, Theorem 1.4.14, Lemma 1.6.12, Proposition 1.4.22] and [Lou24, Lemma 2.1.1.5], and on Lemma 2.20, which is only verified by citing [Lou24, Lemma 2.1.1.5] and a 'readily verified' computation in PShSet(Θ2). This identification is load-bearing for the advertised resolution of the Gaitsgory–Rozenblyum conjecture, because the conjecture is about the Gray tensor product of [GR17]. Please make these dependencies explicit and supply the missing verification of Lemma 2.20 or a precise reference for it.
minor comments (5)
  1. [Abstract and §1.4] The phrase 'all conjectures are now resolved' overstates what is proved in this paper, since several of the eight conjectures are resolved only by cited works; consider saying that with the present paper, proofs of all eight conjectures now exist in the literature.
  2. [§1.4] There is a typo in 'cateogries' near the discussion of Grandis–Paré's theorem.
  3. [Theorem A] The description of the image in Theorem A leaves implicit that the companion of a vertical arrow is unique up to contractible choice; Remark 3.7 supplies this, but stating it in the theorem would make the statement easier to read.
  4. [Lemma 3.15] The notation MapDbl∞Cat([0,0],Q), MapDbl∞Cat([1]v,Q)′, and MapDbl∞Cat(Sq([1]),Q)′ is introduced only inside the proof diagram; the two middle columns are not named, which makes the diagram harder to follow.
  5. [Proposition 2.18] The proof uses a density argument claiming full faithfulness of certain restriction functors on cocontinuous bifunctors; the argument is compressed and would benefit from a reference to a standard nerve theorem or a short explanation of why the restriction is fully faithful.

Circularity Check

0 steps flagged · score 1.0 of 10

No circularity: Theorem B is a genuine comparison theorem; the self-cited black boxes (Lemma 4.4, Proposition 2.22) are independent statements about (∞,ω)- and double ∞-categories, not the target Gaitsgory–Rozenblyum conjecture.

full rationale

The central claim, Theorem B, is a nontrivial comparison rather than a repackaging of its inputs. Sq(C) is defined from the Gray tensor product by the levelwise formula Map(⟨n,m⟩,Sq(C))=Map([n]⊗[m],C), and the substance of Theorem B is that Gr(Ch×Dv), the object corepresented by this Sq, actually computes C⊗D. The proof reduces to the generating shapes [n;m] and [k;l] by density, then builds C⊗D through a chain of pushouts (Construction 4.5, Lemmas 4.6–4.10) whose epimorphicity input is Lemma 4.4. The principal black boxes are self-citations: Lemma 4.4 cites [Lou25, Lemma 1.6.12] and [Lou24, Proposition 2.2.1.50]; Proposition 2.22 identifies ⊗L with ⊗ using [Lou25] and [Lou24]; Theorem 3.10 uses [Lou25, Theorem 3.4.1]. These are load-bearing and not independently formalized, which is a trust and correctness risk, but they are not circular: they concern effectivity, epimorphicity, and companions, and none of them states or presupposes [GR17, Proposition 10.4.5.4]. No fitted parameter is renamed as a prediction, no definition presupposes the target equivalence, and uniqueness of the comparison is proved separately via Proposition 2.18. The paper is not self-contained, but heavy self-citation is not circularity here because the cited results have stated assumptions that do not include the target result; the central claim therefore retains independent mathematical content.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The proof relies on a network of results from the same authors' earlier preprints; these are not derived in the paper and are not formally verified. There are no fitted parameters or new postulated objects.

assumptions (4)
  • standard math Standard density results for ∞-categories and (∞,2)-categories: ∆ is dense in ∞Cat, Θ2 is dense in (∞,2)Cat, and [∆;∆] is dense in (∞,2)Cat.
    Used throughout, e.g., Construction 2.9 and the density reductions in the proofs of Proposition 2.18 and Lemma 4.7.
  • domain assumption [Lou25, Theorem 3.4.1]: the effectivity of generalized double ∞-categories holds.
    Invoked as a black box in the proof of Theorem 3.10 to replace a companion-complete double ∞-category by the Čech nerve of an eso filtration. This is from the first author's preprint and is not proved here.
  • domain assumption [Rui25a, Theorems 4.13 and 4.15]: companionship in Sq([1]) is universal, and complete double ∞-categories admit companion-preserving dualities.
    Used in Lemma 3.15 and Theorem 3.14; these results come from the second author's preprint and are not included in this paper.
  • domain assumption [Lou24, Lemma 2.1.1.5] and [Lou25] results on colimits in set-valued presheaves and comparisons of Gray tensor products (e.g., Proposition 2.22).
    Support Lemma 2.20, Proposition 2.21, Proposition 2.22, and Lemma 4.6. These are cited as established, not reproved in the manuscript.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the squares functor and the Gaitsgory-Rozenblyum conjectures." pith.science (2026). https://pith.science/paper/53ULBHYG

@misc{pith2026250707807,
  author       = {Pith},
  title        = {Pith review of: On the squares functor and the Gaitsgory-Rozenblyum conjectures},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/53ULBHYG}},
  note         = {Machine review of arXiv:2507.07807}
}
abstract

In the seminal work of Gaitsgory and Rozenblyum on derived algebraic geometry, eight conjectures regarding the theory of $(\infty,2)$-categories are stated. This paper aims to clarify the status of these claims, and to provide a proof for the last remaining open one. Along the way, we demonstrate the universal property of the so-called squares functor, a construction that plays an important role in the $(\infty,2)$-categorical foundations of Gaitsgory-Rozenblyum.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. The Gray Product of $(\infty, n)$-Categories via Lax Grids

    math.CT 2026-06 unverdicted novelty 7.0 of 10

    Univalent Segal sheaves on lax grids are monoidally equivalent to (∞,n)-categories with Campion's Gray product, constructed by Day convolution.

Reference graph

Works this paper leans on

23 extracted references · 17 canonical work pages · cited by 1 Pith paper

  1. [1]

    Fernando Abell \'a n, Comparing lax functors of ( ,2) -categories, arXiv preprint arXiv:2311.12746 (2023)

  2. [2]

    Dimitri Ara and Georges Maltsiniotis, Joint et tranches pour les -cat\'egories strictes, Soci \'e t \'e Math \'e matique de France, 2020

  3. [3]

    Timothy Campion, The G ray tensor product of ( ,n) -categories , arXiv preprint arXiv:2311.00205 (2023)

  4. [4]

    Timothy Campion, Krzysztof Kapulkin, and Yuki Maehara, Comical sets: A cubical model for ( ,n) -categories , arXiv preprint arXiv:2005.07603 (2020), 2

  5. [5]

    Timothy Campion and Yuki Maehara, A model-independent G ray tensor product for ( ,2) -categories , arXiv preprint arXiv:2304.05965, 2023

  6. [6]

    Brandon Doherty, Krzysztof Kapulkin, and Yuki Maehara, Equivalence of cubical and simplicial approaches to ( ,n) -categories, Advances in Mathematics 416 (2023), 108902

  7. [7]

    Charles Ehresmann, Cat\'egories structur\'ees III , Cah. Topol. G\'eom. Diff\'er. Cat\'eg. 5 (1963), 1--21

  8. [8]

    Andrea Gagna, Yonatan Harpaz, and Edoardo Lanari, Gray tensor products and lax functors of ( ,2) -categories, Advances in Mathematics 391 (2021), 107986

Show all 23 references
  1. [9]

    5, 1369--1385

    Saul Glasman, Day convolution for -categories, Mathematical Research Letters 23 (2016), no. 5, 1369--1385

  2. [10]

    Marco Grandis and Robert Par\'e, Adjoint for double categories, Cah. Topol. G\'eom. Diff\'er. Cat\'eg. 45 (2004), no. 3, 193--240

  3. [11]

    Dennis Gaitsgory and Nick Rozenblyum, A study in derived algebraic geometry. V ol. I . C orrespondences and duality , Mathematical Surveys and Monographs, vol. 221, American Mathematical Society, Providence, RI, 2017

  4. [12]

    391, Springer, 2006

    John Walker Gray, Formal category theory: adjointness for 2-categories, vol. 391, Springer, 2006

  5. [13]

    Math., vol

    Andr\'e Joyal and Myles Tierney, Quasi-categories vs Segal spaces , Categories in algebra, geometry and mathematical physics, Contemp. Math., vol. 431, Amer. Math. Soc., 2007, pp. 277--326

  6. [14]

    F\'elix Loubaton, Categorical theory of ( , ) -categories, arXiv preprint arXiv:2406.05425 (2024)

  7. [15]

    , Effectivity of G eneralized D ouble - C ategories , arXiv:2503.19242, 2025

  8. [16]

    170, Princeton University Press, 2009

    Jacob Lurie, Higher topos theory, Annals of Mathematics Studies, vol. 170, Princeton University Press, 2009

  9. [17]

    , Higher algebra, available at http://www.math.harvard.edu/lurie (2017)

  10. [18]

    Yuki Maehara, The G ray tensor product for 2-quasi-categories , Advances in Mathematics 377 (2021), 107461

  11. [19]

    1, 1-21 (2023)

    Viktoriya Ozornova, Martina Rovelli, and Dominic Verity, Gray tensor product and saturated n -complicial sets, Higher Structures 7,no. 1, 1-21 (2023)

  12. [20]

    Charles Rezk, A model for the homotopy theory of homotopy theory, Trans. Amer. Math. Soc. 353 (2001), no. 3, 973--1007

  13. [21]

    Jaco Ruit, Homotopy coherent companionships and conjunctions, arXiv preprint arXiv:2408.14335 (2025)

  14. [22]

    , On multiple -categories and formal category theory via -equipments, Ph. D . thesis, Universiteit Utrecht, 2025

  15. [23]

    B asic homotopy theory , Advances in Mathematics 219 (2008), no

    Dominic Verity, Weak complicial sets I . B asic homotopy theory , Advances in Mathematics 219 (2008), no. 4, 1081--1149

Pith tools

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