Michael Shulman Cauchy factorization

Definitions

A morphism m:ABm:A\to B in a 2-category KK is called ff and retract-closed or rff if K(X,A)K(X,B)K(X,A)\to K(X,B) is fully faithful and closed under retracts for all XX. Explicitly this means that (in addition to being ff) if b:XBb:X\to B is a retract of mam a for some a:XAa:X\to A, then bmab\cong m a' for some aAa'\in A.

A morphism e:ABe:A\to B is called Cauchy surjective or cso if it is left orthogonal to all rffs; that is, if

K(B,C) K(B,D) K(A,C) K(A,D)\array{K(B,C) & \to & K(B,D)\\ \downarrow & & \downarrow \\ K(A,C) & \to & K(A,D)}

is a pullback whenever m:CDm:C\to D is rff.

Remarks

  • Since rffs are stable under pullback, ee is cso if and only if whenever it factors through an rff m:CBm:C\to B, then mm is an equivalence.

  • Every eso is cso, since every rff is ff. Conversely, in a (2,1)-category, every ff is rff, and thus every cso is eso.

  • In CatCat, the Cauchy surjective functors are those for which every object of BB is a retract of an object of AA.

  • Every equifier or inverter is rff. Therefore, every Cauchy surjective morphism is cofaithful and coconservative. In “Modulated bicategories” by Carboni, Johnson, Street, and Verity it is shown that conversely, every coconservative functor in CatCat is Cauchy surjective.

Factorization System

In CatCat, (cso,rff) is a factorization system. We now show that the same is true in any regular 2-category.

Given f:ABf:A\to B, let R fR_f be its retractor. This is a 2-categorical finite limit which comes with projections p:R fAp:R_f\to A and q:R fBq:R_f\to B and 2-cells ρ:fpq\rho:f p \to q and σ:qfp\sigma:q \to f p such that ρσ=1 q\rho \sigma = 1_q, and which is universal with these properties.

Lemma

In any 2-category, if q:R fBq:R_f\to B is eso, then ff is Cauchy surjective.

Proof

Suppose that qq is eso and let AgCmBA\overset{g}{\to} C \overset{m}{\to} B be such that fmgf\cong m g and mm is rff; we want to show mm is an equivalence. But since mm is rff and qq is a retract of fpmgpf p \cong m g p, it follows that qq factors through mm; whence mm is an equivalence since qq is eso.

Now suppose that KK is regular, and for any f:ABf:A\to B, let R fjC fmBR_f \overset{j}{\to} C_f \overset{m}{\to} B be an (eso,ff) factorization of qq. Since ff is a retract of f1 Af 1_A, there is a canonical s:AR fs:A\to R_f with ps1 Ap s \cong 1_A and fqsmjsf\cong q s \cong m j s.

Lemma

In a regular 2-category, if f:ABf:A\to B is ff and C fAC_f\subset A (hence C fAC_f\simeq A), then ff is rff.

Proof

Suppose ff is ff and C fAC_f\simeq A, and let b:XBb:X\to B and a:XAa:X\to A be such that bb is a retract of aa. Then bqcb \cong q c and apca\cong p c for some c:XR fc:X\to R_f. Then we have jc:XC fj c:X\to C_f with mjcbm j c \cong b. But since C fAC_f\simeq A in Sub(B)Sub(B), we have a y:XAy:X\to A with fybf y \cong b as well; hence ff is rff.

Theorem

In a regular 2-category KK, 1. Every morphism ff factors as a Cauchy surjective morphism followed by an rff. 1. Therefore, (cso,rff) is a factorization system on KK. 1. A morphism ff is cso if and only if q:R fBq:R_f\to B is eso. 1. Likewise, ff is rff if and only if it is ff and C fAC_f\simeq A.

Proof

Given any f:ABf:A\to B, let jj, mm, and ss be as above, and define e=js:AC fe = j s:A\to C_f. Then memjsqsfm e \cong m j s\cong q s \cong f. Is easy to check that R fR eR_f \cong R_e; thus R eC fR_e\to C_f is eso, so by Lemma ee is Cauchy surjective.

Now let R mR_m be the retractor of mm, with p:R mC fp':R_m\to C_f, q:R mBq':R_m\to B, and corresponding factorization R mjC mmBR_m \overset{j'}{\to} C_m \overset{m'}{\to} B. Let

P u R f v j R m p C f\array{P & \overset{u}{\to}& R_f\\ ^v \downarrow && \downarrow ^j\\ R_m & \underset{p'}{\to} & C_f}

be a pullback. Then vv, like jj, is eso, and thus so is jv:PC mj' v:P \to C_m. Now mjvqvm' j' v \cong q' v is a retract of mpvmjuqum p' v\cong m j u \cong q u, and qq is a retract of fpf p, so quq u is a retract of fpuf p u. Therefore, mjv:PBm' j' v:P\to B is also a retract of fpuf p u, so there is a morphism w:PR fw:P\to R_f with mjwqwmjvm j w \cong q w \cong m' j' v (and pwpup w\cong p u). Now in the square

P jw C f jv m C m m B,\array{P & \overset{j w}{\to} & C_f\\ ^{j' v}\downarrow && \downarrow ^m\\ C_m & \underset{m'}{\to} & B,}

mm is ff and jvj' v is eso, so we have C mC fC_m\subset C_f in Sub(B)Sub(B); thus by Lemma mm is rff.

Therefore, with fmef\cong m e we have factored ff as a cso followed by an rff; this shows the first two statements. Moreover, ee satisfies the condition of Lemma , so if ff is cso and hence equivalent to ee, so does it. Likewise, mm satisfies the condition of Lemma , so if ff is rff and hence equivalent to mm, so does it.

Internal logic

From the characterization of csos and rffs in Theorem , we can conclude that csos and rffs have the expected descriptions in the internal logic.

Corollary

In a regular 2-category, a morphism f:ABf:A\to B is Cauchy surjective if and only if the following sequent is valid in the internal logic:

y:B|(x:A)(ρ:hom B(f(x),y))(σ:hom B(y,f(x)))(ρσ=1 y).y:B | \top \vdash (\exists x:A)(\exists \rho:hom_B(f(x),y))(\exists \sigma:hom_B(y,f(x)))(\rho \sigma = 1_y).
Proof

The context y:B,x:A,ρ:hom B(f(x),y),σ:hom B(y,f(x))|ρσ=1 yy:B, x:A, \rho:hom_B(f(x),y), \sigma:hom_B(y,f(x)) | \rho \sigma = 1_y is easily seen to be precisely R fR_f.

Corollary

In a regular 2-category, a morphism f:ABf:A\to B is rff if and only if it is ff and the following sequent is valid in the internal logic:

x:A,y:B,ρ:hom B(f(x),y),σ:hom B(y,f(x))|ρσ=1 y(x:A)(f(x)y)x:A,y:B,\rho:hom_B(f(x),y), \sigma:hom_B(y,f(x)) | \rho \sigma = 1_y \vdash (\exists x':A)(f(x')\cong y)
Proof

The validity of this sequent says that the pullback of f:ABf:A\to B along q:R fBq:R_f \to B is eso. But since both ff and qq factor through the ff m:C fBm:C_f\to B, this pullback is equivalent to the pullback of e:AC fe:A\to C_f along j:R fC fj:R_f\to C_f. Since jj is eso, this pullback being eso is equivalent to e:AC fe:A\to C_f being eso. And since ff is ff, so is ee; thus this is equivalent to ee being an equivalence.

Last revised on February 28, 2009 at 05:19:27. See the history of this page for a list of all contributions to it.