nLab free object




Let U:CDU: C\to D be a forgetful functor and xDx\in D an object of the category DD.

A free CC-object on xx with respect to UU is an object of CC that satisfies the universal property that F(x)F(x) would have, if FF were a left adjoint to UU (the corresponding free functor) (the free construction on xx).

If UU actually has a left adjoint, then F(x)F(x) is a free CC-object on xx for every xx, and conversely if there exists a free CC-object on every xDx\in D then UU has a left adjoint. But individual free objects can exist without the whole left adjoint functor existing. In general, we have a “partially defined adjoint”, or JJ-relative adjoint where JJ is the inclusion of a full subcategory (on those objects admitting free objects).

More precisely: a free CC-object on xx consists of an object yCy\in C together with a morphism η x:xUy\eta_x \colon x\to U y in DD such that for any other zCz\in C and morphism f:xUzf\colon x\to U z in DD, there exists a unique g:yzg\colon y\to z in CC with U(g)η x=fU(g) \circ \eta_x = f.

In other words, it is an initial object of the comma category (x/U)(x/U). A free CC-object on xx is also sometimes called a universal arrow from xx to the functor UU. It can also be identified with a semi-final lift of an empty UU-structured sink.

Sometimes one says an object cc of CC is free (relative to a forgetful functor U:CDU: C \to D which is often tacitly understood) if there is some object xx of DD and some arrow xUcx \to U c that is initial in (x/U)(x/U). For example, the Quillen-Suslin theorem says that finitely generated projective modules over polynomial algebras over a field are free; the tacit forgetful functor is from the category of modules over a polynomial algebra to SetSet. In this way, freeness is understood as a property of an object.

Similarly, a cofree object is given by a cofree functor.


For more examples see at free construction.

A general way to construct free objects is with a transfinite construction of free algebras (in set-theoretic foundations), or with an inductive type or higher inductive type (in type-theoretic foundations).

Last revised on April 27, 2019 at 04:07:19. See the history of this page for a list of all contributions to it.