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


view this post on Zulip 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 CC has property PP, then F(C)F(C) also has property PP.

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

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

If CC has products, then the free cocartesian category on CC 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.

view this post on Zulip 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 CC has property PP, then F(C)F(C) also has property PP

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).

view this post on Zulip 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 CC 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,Set]Mod(T):UL:[T,\mathbf{Set}] \leftrightarrow \mathbf{Mod}(T):U

The image of the reflector induces an implicit rewriting system on objects of Mod(T)\mathbf{Mod}(T). Since LL 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 LL 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 LL, and then use it to tackle statements of the form:

If CC has property PP, then F(C)F(C) also has property PP

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