free object in nLab
Context
Category theory
Contents
Definition
Let U:C→DU: C\to D be a forgetful functor and x∈Dx\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 x∈Dx\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 y∈Cy\in C together with a morphism η x:x→Uy\eta_x \colon x\to U y in DD such that for any other z∈Cz\in C and morphism f:x→Uzf\colon x\to U z in DD, there exists a unique g:y→zg\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:C→DU: C \to D which is often tacitly understood) if there is some object xx of DD and some arrow x→Ucx \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.
Examples
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.