Todd Trimble Lemma on wide pushouts

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

F(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.

Theorem

Let $F$ be a polynomial endofunctor such that the constant term $a_0$ is $0$ . Let $\{f_j: p \to c_j\}_{j \in J}$ be an arbitrary cone; write $(\sum_{j})_p c_j$ for the wide pushout. Then the canonical map

(\sum_j)_{F p} F(c_j) \to F((\sum_j)_p c_j)

is a monomorphism.

Lemma

Let $W: J \to C$ be any diagram in $C$ , and let $F_i$ be a family of functors such that the canonical arrows $colim F_i \circ W \to F_i(colim W)$ are all monic. Then, for $F = \sum_i a_i F_i$ , the canonical arrow $colim F \circ W \to F(colim W)$ is monic.

Proof

Easy, using the fact that the functors $\sum_I: C^I \to C$ and $a \times -: C \to C$ 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.

Lemma

Let $F_i$ be the $i^{th}$ power functor, and suppose that for any finite cone diagram $W$ , the canonical arrow

colim F_i \circ W \to F_i(colim W)

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

Proof

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 $p \downarrow C$ , and a coproduct is a filtered colimit of finite coproducts. Secondly, if $W: J \to C$ is any cone diagram, we have a chain of maps

\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.

Lemma

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$ .

Proof

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:

Lemma

In the category of sets, given a pair of functions

A \stackrel{f_1}{\leftarrow} P \stackrel{f_2}{\to} B,

the canonical arrow

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

is monic.

Proof

The pushout $C = A +_P B$ is the set of equivalence classes on $A + B$ where $x \in A + B$ is deemed equivalent to $x' \in A + B$ iff there is a zig-zag path

x = 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 \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 $\phi$ is monic.

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