[001R] Theorem 1·d (Local criteria).
[001S] 1·d·a (LI/LF criteria).

The fact that φ\vf is exact is equivalent, through ZZ, to a condition LI of local initiality or to a condition LF of local finality:

  • (local initiality) xX0x\in X_0, xSUxVx\downarrow S \to Ux\downarrow V is initial [this is the functor sending (xSa)(x\to Sa) into (UxUSaφVTa)(Ux \to USa \xto{\vf} VTa), TN];
  • (local finality) yY0y\in Y_0, TyUVyT\downarrow y \to U\downarrow Vy is final [this is the functor sending (Tay)(Ta\to y) into (USaφVTaVy)(USa \xto{\vf} VTa \to Vy), TN].
[001T] 1·d·b (π0\pi_0\triangledown criterion).

For every P,Q,x:PX,y:QYP,Q, x : P \to X, y : Q \to Y we consider the diagram of comma objects, where xφyx \tdown_\vf y is a strict pullback, and xy:xφyUxVyx\btdown y : x \tdown_\vf y \to Ux\downarrow Vy [the dotted arrow, TN] is the functor induced by the universal property of said comma object.

If π0(xy)\pi_0(x\btdown y) is a bijection we say that φ\vf is exact at (xy)\smat{x \\ y} and we write (xy)φ\smat{x \\ y}\vDash \vf. So, φ\vf exact equals the following condition (π0\pi_0\tdown): for all P,Q,x:PX,y:QYP,Q, x : P \to X, y : Q \to Y, we have (xy)φ\smat{x \\ y}\vDash\vf.

The proof is by inspection of the strict pullback xφyx \tdown_\vf y and of the functor xyx\btdown y; xφyx \tdown_\vf y is the subcategory of the product on objects of the form {p,a,qXpfSaTagYq}\left\{ p,a,q \mid \nbsmat{ Xp &\overset{f}\to& Sa \\ Ta &\underset{g}\to& Yq } \right\}, and xyx\btdown y is defined sending such an object to {p,qUXpfUSaVTagVYq}\left\{ p,q \mid \nbsmat{UXp &\overset{f}\to& USa \\ &\swarrow&\\ VTa &\underset{g}\to& VYq } \right\}.