Throughout this article, let be an -pretopos. Define a (finitary) polynomial endofunctor on to be an endofunctor of the form
where the are objects of . We wish to prove the following result.
Let be a polynomial endofunctor such that the constant term is . Let be an arbitrary cone; write for the wide pushout. Then the canonical map
is a monomorphism.
Let be any diagram in , and let be a family of functors such that the canonical arrows are all monic. Then, for , the canonical arrow is monic.
Easy, using the fact that the functors and preserve both colimits and monos.
This lemma reduces us to showing that the finite power functors satisfy the conclusion of the theorem.
Let be the power functor, and suppose that for any finite cone diagram , the canonical arrow
is monic. Then, the same is true for any infinite cone diagram .
The 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 is a coproduct in a comma category , and a coproduct is a filtered colimit of finite coproducts. Secondly, if is any cone diagram, we have a chain of maps
where denotes the restriction of to , 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 and finite wide pushouts when interpreted in the case . Then it holds for finite power functors and finite wide pushouts interpreted in any pretopos (or indeed, in any coherent category) .
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 -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
the canonical arrow
The pushout is the set of equivalence classes on where is deemed equivalent to iff there is a zig-zag path
where for each , either belongs to and the arrows out of alternate between and , or (we are in a “holding pattern” where) belongs to or and the two arrows out of are both identities.
Given in or , and in or , if there is a zig-zag path from to , and a zig-zag path from to , then there is a zig-zag path from to with respect to the pair of maps
one just pairs together zig-zag paths in the separate - and -components. (If the zig-zag to get from to is longer than the zig-zag from to , one can always insert a holding pattern in the -component so that the zig-zag in the -component can “catch up”, i.e., so that the lengths of the zig-zags match up.) This means precisely that the map is monic.