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.
Are 'formal limit' and 'formal colimit' sufficiently precise and recognised terms to require an nLab page? They crop up here and there, such as on [[ind-pro-object]].
For context, I was looking to understand this MO answer:
image.png
I guess the definition would be that a "formal colimit of Xs" is an object of the free cocompletion of the category of Xs under some class of colimits?
Just as you might define a "formal sum" of elements of some set to be an element of the free abelian group generated by .
Seems like a reasonable topic for a page to me. I wonder if there's something more general to be said about the meaning of the word "formal".
Right, so we're seeing instances such as [[pro-object]] where the class of limit is mentioned:
A pro-object of a category is a "formal filtered limit" of objects of .
I would be tempted just to redirect those terms to [[free cocompletion]].