distributivity pullback

Distributivity pullback

Distributivity pullback


A distributivity pullback is the data which encodes a particular exponentiation along a morphism in a category. In other words, it is a cofree object with respect to a pullback functor.



For morphisms g:ZAg:Z\to A and f:ABf:A\to B in a category, a pullback around (f,g)(f,g) is a diagram

X p Z g A q f Y r B\array{ X & \xrightarrow{p} & Z & \xrightarrow{g} & A\\ ^q\downarrow &&&& \downarrow^f\\ Y && \xrightarrow{r} && B}

in which the outer rectangle is a pullback.

A morphism of pullbacks around (f,g)(f,g) consists of s:XXs:X\to X' and t:YYt:Y\to Y' such that ps=pp's=p, qs=tqq s=t q', and r=rsr = r's.


For g:ZAg:Z\to A and f:ABf:A\to B as above, a distributivity pullback around (f,g)(f,g) is a terminal object of the category of pullbacks around (f,g)(f,g).

If the above diagram is a distributivity pullback, we say that it exhibits rr as a distributivity pullback of gg along ff.


Connection to exponentiation


A morphism f:ABf:A\to B is exponentiable if and only if all distributivity pullbacks along ff exist.


The universal property of a distributivity pullback says exactly that YrBY\xrightarrow{r} B is the exponential of gg along ff.

Connection to distributivity

In a category with pullbacks, for any pullback around (f,g)(f,g) with ff and qq exponentiable, we have a canonical Beck-Chevalley isomorphism

r *f *q *p *g *. r^* f_* \xrightarrow{\cong} q_* p^* g^* .

The mate of the inverse of this is a transformation

δ p,q,r:r !q *p *f *g ! \delta_{p,q,r}:r_! q_* p^* \to f_* g_!

A pullback around (f,g)(f,g) with ff and qq exponentiable is a distributivity pullback if and only if δ p,q,r\delta_{p,q,r} is an isomorphism.


See (Weber).

Invertibility of δ\delta expresses that dependent products (the functors f *f_* and q *q_*) distribute over dependent sums (the functors g !g_! and r !r_!).

For instance, in the category of sets, if (C z) zZ(C_z)_{z\in Z} is a ZZ-indexed family of sets, then

(f *g !C) b= f(a)=b g(z)=aC z (f_* g_! C)_b = \prod_{f(a)=b} \sum_{g(z)=a} C_z


(r !q *p *C) b= r(y)=b q(x)=yC p(x) (r_! q_* p^* C)_b = \sum_{r(y)=b} \prod_{q(x)=y} C_{p(x)}

As a very simple example, if B=1B=1, A={0,1}A=\{0,1\}, and Z={00,01,02,10,11}Z=\{00,01,02,10,11\} with g(ij)=ig(i j) = i, then YY is the set of sections of gg, XX the set of pairs of a section and an element of AA, and pp the evaluation. Then if C=(C 00,C 01,C 02,C 10,C 11)C = (C_{00}, C_{01}, C_{02}, C_{10}, C_{11}), we have

f *g !C=(C 00+C 01+C 02)×(C 10+C 11) f_* g_! C = (C_{00} + C_{01} + C_{02}) \times (C_{10} + C_{11})


r !q *p *C=(C 00×C 10)+(C 00×C 11)+(C 01×C 10)+(C 01×C 11)+(C 02×C 10)+(C 02×C 11). r_! q_* p^* C = (C_{00}\times C_{10}) + (C_{00}\times C_{11}) + (C_{01}\times C_{10}) + (C_{01}\times C_{11}) + (C_{02}\times C_{10}) + (C_{02}\times C_{11}).

In the internal dependent type theory of the ambient category, if we express ff and gg as dependent types

b:BA(b):Typeandb:B,a:A(b)Z(b,a):Type b:B \vdash A(b) : Type \qquad and \qquad b:B, a:A(b) \vdash Z(b,a) : Type

then the exponential rr of gg along ff in a distributivity pullback is the dependent product type

b:B a:A(b)Z(b,a):Type. b:B \vdash \prod_{a:A(b)} Z(b,a) : Type.

and the distributivity isomorphism δ\delta says that for any further dependent type

b:B,a:A(b),z:Z(b,a)W(b,a,z):Type b:B, a:A(b), z:Z(b,a) \vdash W(b,a,z) : Type

in the context of b:Bb:B we have an isomorphism

ϕ: a:A(b)Z(b,a) a:A(b)W(b,a,ϕ(a)) a:A(b) z:Z(b,a)W(b,a,z). \sum_{\phi:\prod_{a:A(b)} Z(b,a) } \prod_{a:A(b)} W(b,a,\phi(a)) \qquad \cong \qquad \prod_{a:A(b)} \sum_{z:Z(b,a)} W(b,a,z).

This isomorphism (or more specifically the left-to-right map) has traditionally been called the “axiom of choice” in Martin-Lof type theory, since if \sum and \prod are interpreted according to propositions as types then it looks like the set-theoretic axiom of choice. However, this is not really appropriate, since this is a provable statement rather than an additional axiom, and does not have any of the usual strong consequences of the set-theoretic axiom of choice. See axiom of choice for further discussion.

Connection to pullback complements

If pp is an isomorphism, then a distributivity pullback is also a final pullback complement.


Last revised on July 29, 2017 at 04:04:29. See the history of this page for a list of all contributions to it.