Todd Trimble
Lemma on wide pushouts

Throughout this article, let C be an -pretopos. Define a (finitary) polynomial endofunctor on C to be an endofunctor F:CC of the form

F(c)= n0a n×c nF(c) = \sum_{n \geq 0} a_n \times c^n

where the a n are objects of C. We wish to prove the following result.


Let F be a polynomial endofunctor such that the constant term a 0 is 0. Let {f j:pc j} jJ be an arbitrary cone; write ( j) pc j for the wide pushout. Then the canonical map

( j) FpF(c j)F(( j) pc j)(\sum_j)_{F p} F(c_j) \to F((\sum_j)_p c_j)

is a monomorphism.


Let W:JC be any diagram in C, and let F i be a family of functors such that the canonical arrows colimF iWF i(colimW) are all monic. Then, for F= ia iF i, the canonical arrow colimFWF(colimW) is monic.


Easy, using the fact that the functors I:C IC and a×:CC preserve both colimits and monos.

This lemma reduces us to showing that the finite power functors F i(c)=c i satisfy the conclusion of the theorem.


Let F i be the i th power functor, and suppose that for any finite cone diagram W, the canonical arrow

colimF iWF i(colimW)colim F_i \circ W \to F_i(colim W)

is monic. Then, the same is true for any infinite cone diagram W.


The i th power functor preserves filtered colimits, and arbitrary wide pushouts are filtered colimits of finite wide pushouts. In more detail, we firstly know that a wide pushout of a cone with vertex p is a coproduct in a comma category pC, and a coproduct is a filtered colimit of finite coproducts. Secondly, if W:JC is any cone diagram, we have a chain of maps

colim JF iW colim finiteSJcolimF iW S mono colim finiteSJF i(colimW S) F i(colim finiteSJcolimW S) F i(colim JW)\array{ colim_J F_i \circ W & \cong & colim_{\text{finite}\, S \subseteq J} colim F_i \circ W_S \\ & \stackrel{mono}{\to} & colim_{\text{finite} \, S\subseteq J} F_i(colim W_S) \\ & \cong & F_i(colim_{\text{finite}\, S\subseteq J} colim W_S) \\ & \cong & F_i(colim_J W) }

where W S denotes the restriction of W to S, the shape of a finite subcone. Here the monicity in the second line is by hypothesis, and the fact that taking colimits of filtered diagrams respects monos (because filtered colimits interchange with finite limits). The isomorphism in the third line obtains since finite power functors preserve filtered colimits. This completes the proof.

This lemma reduces us to proving the theorem only in the case for finite cones and finite power functors.


Suppose the theorem holds for finite power functors F i(c)=c i and finite wide pushouts when interpreted in the case C=Set. Then it holds for finite power functors and finite wide pushouts interpreted in any pretopos (or indeed, in any coherent category) C.


Indeed, the theorem is manifestly expressible as a statement in a coherent theory, classified by a coherent topos, and by the completeness theorem for coherent logic (Deligne’s theorem: every coherent topos has enough points), to check provability in the theory under coherent logic, it suffices to check that it holds in every Set-model of the theory.

Thus, we have boiled down the proof to a set-theoretic statement. Notice that finite wide pushouts are iterated ordinary pushouts, so ordinary pushouts suffice. The case for the squaring functor is sufficiently representative that we content ourselves with a proof just in this case. For that, we simply quote the answer given on Math Overflow:


In the category of sets, given a pair of functions

Af 1Pf 2B,A \stackrel{f_1}{\leftarrow} P \stackrel{f_2}{\to} B,

the canonical arrow

ϕ:A 2+ P 2B 2(A+ PB) 2\phi: A^2 +_{P^2} B^2 \to (A +_P B)^2

is monic.


The pushout C=A+ PB is the set of equivalence classes on A+B where xA+B is deemed equivalent to xA+B iff there is a zig-zag path

x=x 0f i 1p 0f i 2x 1x n1f i n1p n1f i nx n=xx = x_0 \stackrel{f_{i_1}}{\leftarrow} p_0 \stackrel{f_{i_2}}{\to} x_1 \leftarrow \ldots x_{n-1} \stackrel{f_{i_{n-1}}}{\leftarrow} p_{n-1} \stackrel{f_{i_n}}{\to} x_n = x'

where for each k, either p k belongs to P and the arrows out of p k alternate between f 1 and f 2, or (we are in a “holding pattern” where) p k belongs to A or B and the two arrows out of p k are both identities.

Given (x,y) in A 2 or B 2, and (x,y) in A 2 or B 2, if there is a zig-zag path from x to x, and a zig-zag path from y to y, then there is a zig-zag path from (x,y) to (x,y) with respect to the pair of maps

A×Af 1×f 1P×Pf 2×f 2B×B;A \times A \stackrel{f_1 \times f_1}{\leftarrow} P \times P \stackrel{f_2 \times f_2}{\to} B \times B;

one just pairs together zig-zag paths in the separate x- and y-components. (If the zig-zag to get from y to y is longer than the zig-zag from x to x, one can always insert a holding pattern in the x-component so that the zig-zag in the y-component can “catch up”, i.e., so that the lengths of the zig-zags match up.) This means precisely that the map ϕ is monic.

Revised on October 9, 2011 06:45:47 by Todd Trimble