nLab generalized element



Idea and definition

In a broad, non-technical sense, an “element” is a “building block”, “component”, or “basic part” of a more substantial whole. Ordinary or global elements of a set are simply the points of that set, and hence sufficiently capture this broad notion of “element” in Set, since by definition sets are no more than collections of points.

However, in general, knowing about the points of an object is insufficient to count as knowing its elements (construed broadly). From the point of view of the category Set, most things that can be said and done about elements of a set XX, can more generally be said and done for morphisms x:UXx \colon U\to X, for any other set UU. The point is just that many constructions can be performed “elementwise”. For instance, the fact that elements of X×YX\times Y are exactly pairs (x,y)(x,y) of an element of XX and an element of YY, when performed “elementwise” for morphisms out of UU, expresses the universal property of a product. In structural set theory such as ETCS, one sometimes (but not necessarily) takes this point of view for axiomatizing the structure of SetSet.

On the other hand, once elements of objects are regarded as morphisms into these objects, the same reasoning applies to every category CC. Accordingly, for CC any category and XX an object of CC, one may refer to a morphism x:UXx \colon U \to X a generalized element of XX. One says this is a generalized element with stage of definition given by UU, or a figure of shape UU in XX.

The perspective of generalized elements of objects of a category CC is related to regarding CC as its image under the Yoneda embedding

Y:C[C op,Set] Y : C \hookrightarrow [C^{op}, Set]

into its presheaf category. Under this embedding, every object XX of CC is mapped to the functor – the representable functor represented by it –

GenEl(X):C opSet GenEl(X) : C^{op} \to Set

that sends each object UU of CC to the set of generalized elements of XX at stage UU.

It is also worth noting that the internal logic or type theory of a category provides us a way to go backwards formally. By reasoning about “abstract elements” in a set-theoretic style like ordinary elements, the interpretation then “compiles” such proofs to category-theoretic ones which actually apply to all generalized elements.


In SetSet

The primordial example is when CC is the category Set of sets and II is a terminal object in SetSet — that is, a set with one element. Then elements of any set cc are in one-to-one correspondence with functions f:Icf: I \to c. This correspondence works as follows: given any element of cc there is a unique function f:Icf: I \to c with this element in its image, and conversely each function f:Icf: I \to c has a unique element of cc in its image.

In concrete categories

In the same way, in a concrete category whose underlying-set functor is represented by II, the II-elements of an object are the same as the elements of its underlying set. (The category of sets is actually a special case of this, since it is concrete, with the identity functor represented by a terminal object.)

Global elements

Generalizing from SetSet in another way, in any category with a terminal object II, we call a morphism f:Icf : I \to c a global element of the object cc.

In toposes

The stability or slice theorem for toposes says that if E\mathbf{E} is a topos, then also the slice category E/U\mathbf{E}/U is a topos for any object UU, and the pullback functor U *:EE/UU^\ast: \mathbf{E} \to \mathbf{E}/U is a logical functor.

Observe that in E/U\mathbf{E}/U, an ordinary (i.e. global) point of an object U *XU^\ast X, a section U *1U *XU^\ast 1 \to U^\ast X, corresponds to a generalized element UXU \to X in E\mathbf{E}. Thus the slice theorem guarantees that generalized points with domain UU may be treated exactly as ordinary points, just in a more variable topos E/U\mathbf{E}/U.

In monoidal categories

On the other hand, it is common to take II to be the unit object whenever CC is a monoidal category. The generalized elements defined over this II are important in enriched category theory).

For generators

Arguably, the most general case where generalized elements defined at only one stage II are “sufficient” when II is some sort of generator of the category. However, not every category has a single object as any sort of generator! Instead, in arbitrary categories, generalized elements of all possible stages of definition must often be used to replace global elements. Thus while a set is determined by its global elements, an object of an arbitrary category is determined by all of its generalized elements (this is one way to state the Yoneda lemma).

In presheaf categories

For C=[D op,Set]C = [D^{op}, Set] a presheaf category and for I=Δ pt=(d{})I = \Delta_{pt} = (d \mapsto \{\bullet\}) the presheaf constant at the singleton set, the generalized elements of a presheaf FF are the global sections of this presheaf, equivalently these are the elements in the limit set over FF.

On the other hand, if I=D(,d)I=D(-,d) is a representable presheaf, then the generalized elements of FF at stage dd are precisely the elements of the set F(d)F(d), by the Yoneda lemma.

In abelian categories

An element in an abelian category is an equivalence class of generalised elements.

Relationship to type theory

In the internal type theory of a category CC, the generalized elements of XX at stage UU can be identified with terms of type XX in context u:Uu\colon U:

u:Ux(u):X. u\colon U \vdash x(u) \colon X \,.

See the references below.

The fact that all type-theoretic constructions can be performed in any context implies that we can manipulate ordinary elements, and end up speaking also about generalized elements defined at arbitrary stages.


In type theory

The interpretation of terms in type theory as generalized elements of objects in a category is discussed for instance on p. 8 of

  • Steve Awodey, Andrej Bauer, Propositions as [[Types]], Journal of Logic and Computation. Volume 14, Issue 4, August 2004, pp. 447-471 (pdf)

Last revised on March 24, 2024 at 22:11:09. See the history of this page for a list of all contributions to it.