nLab composition

Redirected from "composite".
Contents

Context

Category theory

(,1)(\infty,1)-Category theory

Internal (,1)(\infty,1)-Categories

Directed homotopy type theory

Contents

Definition

In a plain category

Composition is the operation that takes morphisms f:xyf\colon x \to y and g:yzg\colon y \to z in a category and produces a morphism gf:xzg \circ f\colon x \to z, called the composite of ff and gg.

Note that this composition is unique by the axioms of category theory. If we instead work in a weak higher category, composition need not be unique. In this sense we may identify the composite of ff and gg with the colimit over the diagram afbgca\stackrel{f}{\to}b\stackrel{g}{\to}c. This point of view is taken and generalized in transfinite composition.

In an enriched category

In enriched category theory, for VV a monoidal category the composition operation on a VV-enriched category CC is for each triple (x,y,z)(x,y,z) of objects of CC a morphism

x,y,z:C(x,y)C(y,z)C(x,z) \circ_{x,y,z} : C(x,y) \otimes C(y,z) \to C(x,z)

in VV.

This reduces to the above definition in the case that V=V = Set. The composition morphism x,y,z\circ_{x,y,z} sends any two composable morphisms to their composite.

x,y,z:((xfy),(ygz))(xgfz). \circ_{x,y,z} : ((x \stackrel{f}{\to} y), (y \stackrel{g}{\to} z)) \;\; \mapsto \;\; (x \stackrel{g\circ f}{\to} z) \,.

For internal homs

Let (𝒞,)(\mathcal{C}, \otimes) be a closed monoidal category. Write [,]:𝒞 op×𝒞𝒞[-,-] : \mathcal{C}^{op}\times \mathcal{C} \to \mathcal{C} for the corresponding internal hom.

Definition

For X,Y,Z𝒞X, Y, Z \in \mathcal{C} three objects, the composition morphism

X,Y,Z:[Y,Z]×[X,Y][X,Z] \circ_{X,Y,Z} : [Y, Z] \times [X, Y] \to [X, Z]

is the (()X[X,])((-)\otimes X \dashv [X,-])-adjunct of the following composite of two evaluation maps, def. :

[Y,Z]×[X,Y]×X(id [Y,Z],eval X,Y)[Y,Z]×Yeval Y,ZZ. [Y, Z] \times [X , Y] \times X \stackrel{(id_{[Y,Z]}, eval_{X,Y})}{\to} [Y,Z] \times Y \stackrel{eval_{Y,Z}}{\to} Z \,.

In simplicial type theory

We work in simplicial type theory with a directed interval 𝕀\mathbb{I}. Let the 2-simplex type be defined as

Δ 2 s:𝕀 t:𝕀st\Delta^2 \coloneqq \sum_{s:\mathbb{I}} \sum_{t:\mathbb{I}} s \leq t

and let the (2,1)-horn type be defined as

Λ 1 2 s:𝟚 t:𝟚(s= 𝕀0)(t= 𝕀1)\Lambda_1^2 \coloneqq \sum_{s:\mathbb{2}} \sum_{t:\mathbb{2}} (s =_\mathbb{I} 0) \vee (t =_\mathbb{I} 1)

where PQP \vee Q is the disjunction of the types PP and QQ. Since sts \leq t implies (s= 𝕀0)(t= 𝕀1)(s =_{\mathbb{I}} 0) \vee (t =_{\mathbb{I}} 1) for all s:𝕀s:\mathbb{I} and t:𝕀t:\mathbb{I}, we have a canonical function

(λt:𝕀.t,λt:𝕀.t,P):Δ 2Λ 1 2(\lambda t:\mathbb{I}.t, \lambda t:\mathbb{I}.t, P):\Delta^2 \to \Lambda^2_1

which is a tuple consisting of two copies of the identity function on 𝕀\mathbb{I} and a dependent function PP that takes the witness that sts \leq t to a witness that (s= 𝕀0)(t= 𝕀1)(s =_{\mathbb{I}} 0) \vee (t =_{\mathbb{I}} 1). By precomposition, this leads to a function

λu.u(λt:𝕀.t,λt:𝕀.t,P):(Δ 2A)(Λ 1 2A)\lambda u.u \circ (\lambda t:\mathbb{I}.t, \lambda t:\mathbb{I}.t, P):(\Delta^2 \to A) \to (\Lambda^2_1 \to A)

for all types AA.

Let h 0,2:𝕀Δ 2h_{0,2}:\mathbb{I} \to \Delta^2 be the face map which represents the unique morphism from 00 to 22 in the 2-simplex.

Definition

A morphism f:𝕀Af:\mathbb{I} \to A is the composite of a composable pair of morphisms k:Λ 1 2Ak:\Lambda^2_1 \to A if one can construct a commutative triangle h:Δ 2Ah:\Delta^2 \to A such that

h(λt:𝕀.t,λt:𝕀.t,P)=kandhh 0,2=fh \circ (\lambda t:\mathbb{I}.t, \lambda t:\mathbb{I}.t, P) = k \; \mathrm{and} \; h \circ h_{0,2} = f

In a Segal type AA, for all elements x:Ax:A, y:Ay:A, and z:Az:A, all composites are unique composites by definition of the Segal condition, and thus one can construct a composition operation on hom-types

λ(g,f).gf:hom A(y,z)×hom A(x,y)hom A(x,z)\lambda (g, f).g \circ f:\mathrm{hom}_A(y, z) \times \mathrm{hom}_A(x, y) \to \mathrm{hom}_A(x, z)

which by the Segal condition is automatically associative and unital.

Higher arity

Strictly speaking, composition as defined above is binary composition. One can also define nn-ary composites for any natural number n0n \geq 0: given n+1n + 1 objects x 0,,x nx_0, \ldots, x_n and nn morphisms f i:x i1x if_i\colon x_{i-1} \to x_i, we get the composite f nf 1:x 0x nf_n \circ \dots \circ f_1\colon x_0 \to x_n. Since composition in a category is associative, a definition of nn-ary composition from binary composition via any choice of bracketing will be equal to that resulting from any other choice of bracketing. The unary composite of f 1:x 0x 1f_1\colon x_0\to x_1 is simply ff itself, and the nullary composite of x 0x_0 is its identity morphism.

Conversely, a category can equivalently be defined as a quiver (a directed graph) equipped with an nn-ary composition operation for every natural number n0n\ge 0, satisfying suitable associativity axioms. This definition may be called unbiased, as opposed to the usual definition which is “biased” towards 00 and 22.

Categorical semantics

In the context of formal logic, composition is the categorical semantics for the cut rule.

Notation

Traditionally, the composite of ff and gg as above is written gfg \circ f, following the notation introduced by the followers of Leibniz for composition of functions. This is often abbreviated as simply gfg f. Of course, this notation preserves the order of symbols in the elementwise definition of function composition: (gf)(x)=g(f(x))(g\circ f)(x) = g(f(x)).

On the other hand, reading a diagram

xfygz x \stackrel{f}\to y \stackrel{g}\to z

the notation fgf g reads better. One way to make this anti-Leibniz convention clearer is to write f;gf ; g (which is based on the interpretation of programming commands as morphisms in theoretical computer science). Since this convention is motivated by the drawing of diagrams, it is also sometimes called diagrammatic order. Another way is to write f *gf^* g, which interprets gg as pulling back along ff to the composite.

Therefore, the notations gfg f and fgf g are ambiguous, while gfg \circ f and f;gf ; g are less so. It seems that the notation gfg f for gfg\circ f is more common than fgf g for f;gf ; g, although the fgf g notation occurs in some important older papers.

Although diagrammatic order has advantages and partisans, especially among category theorists and computer scientists, the “classical” order of composition is firmly entrenched in much of mathematics. Many people who agree that diagrammatic order is “better” on its own merits nevertheless believe that trying to change the established “classical” order of composition creates more confusion than it removes.

In some older category theory papers, arrows were written pointing from right to left, so that the composition of arrows could be written in the “classical” style, while still preserving the diagrammatic intuition. Hom-sets were accordingly written C(b,a)C(b,a), where aa is the source, and bb is the target. This sort of convention has also been used by people working with string diagrams and surface diagrams.

References

The phrase “composite” appears in:

Last revised on June 1, 2025 at 00:24:59. See the history of this page for a list of all contributions to it.