nLab distributivity pullback

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Discuss this page |
Distributivity pullback

Context

Category theory

Distributivity pullback

Idea

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.

Definition

Definition

For morphisms g:Z→Ag:Z\to A and f:A→Bf: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:X→X′s:X\to X' and t:Y→Y′t:Y\to Y' such that p′s=pp's=p, qs=tq′q s=t q', and r=r′sr = r's.

Definition

For g:Z→Ag:Z\to A and f:A→Bf: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.

Properties

Connection to exponentiation

Theorem

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

Proof

The universal property of a distributivity pullback says exactly that Y→rBY\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_!
Theorem

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.

Proof

See (Weber, Proposition 2.2.3).

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) z∈Z(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

while

(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})

and

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:B⊢A(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.

References

Last revised on April 28, 2021 at 15:00:52. See the history of this page for a list of all contributions to it.

EditDiscussPrevious revisionChanges from previous revisionHistory (4 revisions) Cite Print Source