Todd Trimble
Lemma on wide pushouts

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

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

where the a na_n are objects of CC. We wish to prove the following result.


Let FF be a polynomial endofunctor such that the constant term a 0a_0 is 00. Let {f j:pc j} jJ\{f_j: p \to c_j\}_{j \in J} be an arbitrary cone; write ( j) pc j(\sum_{j})_p c_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:JCW: J \to C be any diagram in CC, and let F iF_i be a family of functors such that the canonical arrows colimF iWF i(colimW)colim F_i \circ W \to F_i(colim W) are all monic. Then, for F= ia iF iF = \sum_i a_i F_i, the canonical arrow colimFWF(colimW)colim F \circ W \to F(colim W) is monic.


Easy, using the fact that the functors I:C IC\sum_I: C^I \to C and a×:CCa \times -: C \to C preserve both colimits and monos.

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


Let F iF_i be the i thi^{th} power functor, and suppose that for any finite cone diagram WW, 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 WW.


The i thi^{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 pp is a coproduct in a comma category pCp \downarrow C, and a coproduct is a filtered colimit of finite coproducts. Secondly, if W:JCW: J \to C 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 SW_S denotes the restriction of WW to SS, 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 iF_i(c) = c^i and finite wide pushouts when interpreted in the case C=SetC = Set. Then it holds for finite power functors and finite wide pushouts interpreted in any pretopos (or indeed, in any coherent category) CC.


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 SetSet-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+ PBC = A +_P B is the set of equivalence classes on A+BA + B where xA+Bx \in A + B is deemed equivalent to xA+Bx' \in A + 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 kk, either p kp_k belongs to PP and the arrows out of p kp_k alternate between f 1f_1 and f 2f_2, or (we are in a “holding pattern” where) p kp_k belongs to AA or BB and the two arrows out of p kp_k are both identities.

Given (x,y)(x, y) in A 2A^2 or B 2B^2, and (x,y)(x', y') in A 2A^2 or B 2B^2, if there is a zig-zag path from xx to xx', and a zig-zag path from yy to yy', then there is a zig-zag path from (x,y)(x, y) to (x,y)(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 xx- and yy-components. (If the zig-zag to get from yy to yy' is longer than the zig-zag from xx to xx', one can always insert a holding pattern in the xx-component so that the zig-zag in the yy-component can “catch up”, i.e., so that the lengths of the zig-zags match up.) This means precisely that the map ϕ\phi is monic.

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