Michael Shulman
Cauchy factorization


A morphism m:AB in a 2-category K is called ff and retract-closed or rff if K(X,A)K(X,B) is fully faithful and closed under retracts for all X. Explicitly this means that (in addition to being ff) if b:XB is a retract of ma for some a:XA, then bma for some aA.

A morphism e:AB 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:CD is rff.


  • Since rffs are stable under pullback, e is cso if and only if whenever it factors through an rff m:CB, then m 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 Cat, the Cauchy surjective functors are those for which every object of B is a retract of an object of A.

  • 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 Cat is Cauchy surjective.

Factorization System

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

Given f:AB, let R f be its retractor. This is a 2-categorical finite limit which comes with projections p:R fA and q:R fB and 2-cells ρ:fpq and σ:qfp such that ρσ=1 q, and which is universal with these properties.


In any 2-category, if q:R fB is eso, then f is Cauchy surjective.


Suppose that q is eso and let AgCmB be such that fmg and m is rff; we want to show m is an equivalence. But since m is rff and q is a retract of fpmgp, it follows that q factors through m; whence m is an equivalence since q is eso.

Now suppose that K is regular, and for any f:AB, let R fjC fmB be an (eso,ff) factorization of q. Since f is a retract of f1 A, there is a canonical s:AR f with ps1 A and fqsmjs.


In a regular 2-category, if f:AB is ff and C fA (hence C fA), then f is rff.


Suppose f is ff and C fA, and let b:XB and a:XA be such that b is a retract of a. Then bqc and apc for some c:XR f. Then we have jc:XC f with mjcb. But since C fA in Sub(B), we have a y:XA with fyb as well; hence f is rff.


In a regular 2-category K,

  1. Every morphism f factors as a Cauchy surjective morphism followed by an rff.
  2. Therefore, (cso,rff) is a factorization system on K.
  3. A morphism f is cso if and only if q:R fB is eso.
  4. Likewise, f is rff if and only if it is ff and C fA.

Given any f:AB, let j, m, and s be as above, and define e=js:AC f. Then memjsqsf. Is easy to check that R fR e; thus R eC f is eso, so by Lemma 1 e is Cauchy surjective.

Now let R m be the retractor of m, with p:R mC f, q:R mB, and corresponding factorization R mjC mmB. 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 v, like j, is eso, and thus so is jv:PC m. Now mjvqv is a retract of mpvmjuqu, and q is a retract of fp, so qu is a retract of fpu. Therefore, mjv:PB is also a retract of fpu, so there is a morphism w:PR f with mjwqwmjv (and pwpu). 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,}

m is ff and jv is eso, so we have C mC f in Sub(B); thus by Lemma 2 m is rff.

Therefore, with fme we have factored f as a cso followed by an rff; this shows the first two statements. Moreover, e satisfies the condition of Lemma 1, so if f is cso and hence equivalent to e, so does it. Likewise, m satisfies the condition of Lemma 2, so if f is rff and hence equivalent to m, so does it.

Internal logic

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


In a regular 2-category, a morphism f:AB 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).

The context y:B,x:A,ρ:hom B(f(x),y),σ:hom B(y,f(x))ρσ=1 y is easily seen to be precisely R f.


In a regular 2-category, a morphism f:AB 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)

The validity of this sequent says that the pullback of f:AB along q:R fB is eso. But since both f and q factor through the ff m:C fB, this pullback is equivalent to the pullback of e:AC f along j:R fC f. Since j is eso, this pullback being eso is equivalent to e:AC f being eso. And since f is ff, so is e; thus this is equivalent to e being an equivalence.

Revised on February 28, 2009 05:19:27 by Mike Shulman (