The graph of a function is the subset that “carves out” of the cartesian product .
The traditional standard definition of a graph of a function is this:
The graph of a function is that subset of the cartesian product defined by the property that belongs to the graph of if and only if :
This can be understood as a special case of a graph of a functor by the following observation
For a function, define a function
by regarding a set as a 0-category and a 0-category as a (-1)-category-enriched category and then setting
Then is the characteristic function of in that the diagram
is a pullback diagram.
In other words this means that in the context of (-1)-category-enriched category theory the graph of a function , regarded as an enriched functor is the category of elements of the corresponding profunctor. More on this at graph of a functor.
It is easy to identify the properties of those subsets of that are the graphs of functions, and if they have the same graph (given and ). Consequently, it is common, especially (but not only) in material set theory, to define a function from to as such a subset, that is to identify a function with its graph. On the other hand, from a more categorial foundation, as discussed above, it's common to define a subset to be a characteristic function!
In dependent type theory, a graph of a function is the type
More generally, we can say that the graph of a binary relation from to is a subset of ; belongs to the graph if and only if is related to . (Note that every subset of defines a unique relation; such a subset is the graph of a function if and only if the relation is both functional and entire.)
Notice that with a function regarded as a profunctor as described above, a relation corresponds to a general such profunctor. More precisely we have a pullback square
where
is the relation regarded as a subset of in the traditional sense;
is the characteristic function of this subset.
So in this sense the ordinary notion of relation as a subset does really define the graph of the relation, while the relation itself is more naturally understood as the corresponding 0-profunctor/characteristic function .
The graph of a binary relation from to is related to the notion of graph from graph theory; more precisely, such relations correspond to directed loop graphs (in the sense defined at graph) with vertex set , and either can be defined as a subset of . In a similar way, spans from to correspond to directed pseudographs with vertex set .
For the case of a relation from to without , see under the cograph below.
The graph of a relation of arbitrary arity is similarly a subset of an arbitrary cartesian product; see relation theory for more on this.
Bill Lawvere has also considered the cograph of a function, which is dually a quotient set of the disjoint union ; is identified with if (and additional identifications may follow). However it may make more sense to define the cograph to be a quotient poset of (the discrete poset) ; we declare if (and no additional relationships follow). By regarding again a set as a 0-category, the latter notion of cograph is a special case of the notion of cograph of a functor, as follows:
A function determines a functor from the interval category to Set by setting , and .
Then let be the corresponding category of elements, given by the 2-pullback
which is computed by the strict pullback
The cograph of in the sense of Lawvere is the set of connected components of this category, i.e. .
The notion of cograph of a function may be even more related to the sense of graph in graph theory; although the identifications are not done there, the cograph draws a picture in which any relation (or multispan) of any arity becomes a directed graph (or directed multigraph) whose vertex set is the disjoint union of the relation's domains. When the vertex set is broken up into a disjoint union in this way, graph theorists study this as multipartite graphs; in particular, directed bipartite graphs with vertex set broken up as correspond precisely to binary relations from to .
The notion of graph of a function is a special case of the notion graph of a functor obtained for functors between 0-categories.
Accordingly, the notion of cograph of a function is a special case of the notion of cograph of a functor.
Last revised on January 30, 2024 at 13:20:52. See the history of this page for a list of all contributions to it.