Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: proving a property of free constructions using glueing

Nathanael Arkor (Jan 17 2026 at 15:55):

Glueing is a useful technique for proving properties of free constructions. I am looking for an example/examples where glueing-like arguments are used to prove a result of the form:

If $C$ has property $P$, then $F(C)$ also has property $P$.

(where $C$ is a category and $F$ is some free construction). This would be useful for situations in which it is not easy to describe $F$ very concretely.

For instance, an example of the kind of statement I am thinking of would be:

If $C$ has products, then the free cocartesian category on $C$ also has products.

It seems like glueing is the right kind of tool for this task, but I'm not familiar enough with the glueing literature to know where to look.

Rémy Tuyéras (Jan 17 2026 at 16:56):

"Having products", and many similar categorical properties, can often be expressed as a lifting property. A free construction typically behaves like a left adjoint. Here, however, one often wants the converse direction: a right adjoint, so that lifting properties can be transported back along the functor.

If $C$ has property $P$, then $F(C)$ also has property $P$

Taken at this level of generality, this is a difficult problem. It is closely related to questions studied in rewriting systems and in theories with similar concerns (for instance, coherence and strictification phenomena, and themes adjacent to the homotopy hypothesis for Grothendieck's infinity-groupoids).

Rémy Tuyéras (Jan 17 2026 at 17:46):

Nathanael Arkor said:

It seems like glueing is the right kind of tool for this task, but I'm not familiar enough with the glueing literature to know where to look.

If you really want to pursue this approach (and you have the mathematical courage to go that route), you will likely have to analyze how colimits of objects $C$ decompose inside a category presented as the models of a theory.

In practice, this often means working with the reflector between presheaves and the category of models:

$L:[T,\mathbf{Set}] \leftrightarrow \mathbf{Mod}(T):U$

The image of the reflector induces an implicit rewriting system on objects of $\mathbf{Mod}(T)$. Since $L$ preserves colimits (and, in a precise sense, creates them), you can navigate that rewriting system while reasoning upstream in the presheaf category.

So what is the difficulty? The explicit form of $L$ typically involves quotients that identify the "boundaries" of your glueings. If you do not approach those identifications methodically, the bookkeeping becomes heavy.

When I was working on this question more actively (I still think about it, but less intensely now :sweat_smile:), I wrote a paper precisely to make those quotient identifications in glueing constructions explicit. A natural next step is to extract the underlying rewriting system suggested by the construction of $L$, and then use it to tackle statements of the form:

If $C$ has property $P$, then $F(C)$ also has property $P$

If you are interested, the paper was published in MDPI here, but the arXiv version is more polished (typos corrected, etc.): https://arxiv.org/abs/1511.09332

Nathanael Arkor (Jan 28 2026 at 09:21):

Sorry, I missed your reply earlier. The reason I want to use glueing is to avoid reasoning about the free construction explicitly: I want to derive its properties formally from its universal property. The approach you seem to be suggesting would involve understanding what the free construction looks like, but this is infeasible in the examples I am interested in.

Rémy Tuyéras (Jan 28 2026 at 13:42):

Would you be able to describe the specific examples you are interested in and what you imagine the glueing-based techniques could do (maybe you can describe some imaginary theorems so we can see the level of abstraction you want for the framework)?

Nathanael Arkor (Jan 28 2026 at 14:12):

I provided an example that I think acts as a prototype for the kind of statement I would like to prove. It's just that in my actual examples, the structures are more complicated. However, there will certainly be no hope of a glueing-style argument for the more complicated structures if there is not one for the free cocartesian category construction.

Morgan Rogers (he/him) (Jan 29 2026 at 17:42):

@Nathanael Arkor I think Remy was asking for more a more precise pointer to what this approach is supposed to be rather than a result it might prove. Searching "glu" at the link you opened with finds mentioned of "the gluing approach" without it being immediately obvious which part of the preceding page of text that's referring to.

Nathanael Arkor (Jan 29 2026 at 20:15):

Ah, I have in mind the kind of applications of glueing described in Example 29 of Hyland–Schalk's Glueing and orthogonality for models of linear logic. For convenience:
image.png
image.png

Nathanael Arkor (Jan 29 2026 at 20:15):

For instance, one can prove that the inclusion of a category into its finite coproduct completion is fully faithful using these techniques, without studying the presentation of the category itself.