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.
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 has property , then also has property .
(where is a category and is some free construction). This would be useful for situations in which it is not easy to describe very concretely.
For instance, an example of the kind of statement I am thinking of would be:
If has products, then the free cocartesian category on 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.
"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 has property , then also has property
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).
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 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:
The image of the reflector induces an implicit rewriting system on objects of . Since 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 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 , and then use it to tackle statements of the form:
If has property , then also has property
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