The colimit of a sequence of monomorphisms

Lemma 1.

Let C\C be a countably extensive category with quotients of congruences. Then C\C has colimits of sequences of monomorphisms.

Proof. Suppose we have a sequence X0↪X1↪⋯X_0 \hookrightarrow X_1 \hookrightarrow \cdots with corresponding monomorphisms fm,n:Xm↪Xnf_{m,n} : X_m \hookrightarrow X_n for m≤nm \le n. Define YY to be the coproduct of all XnX_n. Now for each m≤nm\le n, define Em,n≔XmE_{m,n} \coloneqq X_m with two maps im,in∘fm,n:Em,n⇉Yi_m, i_n \circ f_{m,n} : E_{m,n} \rightrightarrows Y, and similarly for m≥nm \ge n define Em,n≔XnE_{m,n} \coloneqq X_n with two maps im∘fn,m,in:Em,n⇉Yi_m \circ f_{n,m}, i_n : E_{m,n} \rightrightarrows Y. Then the coproduct of all Em,nE_{m,n}, with the induced morphisms to YY, forms a congruence. Here, to prove that the maps are jointly monomorphic, and again when proving transitivity, we use extensivity to split the domain of the generalized elements of ∐m,n≥0∞Em,n\coprod_{m,n \geq 0}^\infty E_{m,n} so that, without loss of generality, we may assume that each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence. □\square

Lemma 2.

Let C\C be a countably extensive category with coequalizers of kernel pairs. Assume that X0↪X1↪⋯X_0 \hookrightarrow X_1 \hookrightarrow \cdots is a sequence of monomorphisms that has a cocone (Xn↪Y)(X_n \hookrightarrow Y) consisting of monomorphisms. Then this sequence has a colimit.

Proof. We consider the morphism ∐n≥0Xn→Y\coprod_{n \geq 0} X_n \to Y induced by the monomorphisms Xn↪YX_n \hookrightarrow Y. By assumption, its kernel pair ∐n≥0Xn×Y∐n≥0Xn\coprod_{n \geq 0} X_n \times_Y \coprod_{n \geq 0} X_n exists, and the two projections to ∐n≥0Xn\coprod_{n \geq 0} X_n have a coequalizer. We will prove that this coequalizer is a colimit of the sequence X1↪X2↪⋯X_1 \hookrightarrow X_2 \hookrightarrow \cdots. For this, it suffices to find a natural bijection between cocones (hn:Xn→T)n≥0(h_n : X_n \to T)_{n \geq 0} and morphisms h:∐n≥0Xn→Th : \coprod_{n \geq 0} X_n \to T that coequalize the two projections, where T∈CT \in \C is any object.

A morphism h:∐n≥0Xn→Yh : \coprod_{n \geq 0} X_n \to Y is equivalent to a family of morphisms (hn:Xn→T)n≥0(h_n : X_n \to T)_{n \geq 0}. Since C\C is countably extensive, the canonical morphism ∐n,m≥0Xn×YXm→∐n≥0Xn×Y∐m≥0Xm\textstyle \coprod_{n,m \geq 0} X_n \times_Y X_m \to \coprod_{n \geq 0} X_n \times_Y \coprod_{m \geq 0} X_m is an isomorphism. Hence, hh coequalizes the two projections if and only if for all n,m≥0n,m \geq 0 the diagram

Xn×YXm→Xn↓↓Xm→T \begin{CD} X_n \times_Y X_m @>>> X_n \\ @VVV @VVV \\ X_m @>>> T \end{CD}

commutes. Without loss of generality, we may assume n≤mn \leq m. But then Xn×YXm≅XnX_n \times_Y X_m \cong X_n, and the diagram simplifies to

Xn→=Xn↓↓Xm→T, \begin{CD} X_n @>{=}>> X_n \\ @VVV @VVV \\ X_m @>>> T, \end{CD}

which is precisely the cocone condition for (hn:Xn→T)n≥0(h_n : X_n \to T)_{n \geq 0}. □\square

Context

This page is referenced by the following categories.