nLab wide pullback (Rev #30, changes)

Showing changes from revision #29 to #30: Added | ~~Removed~~ | ~~Chan~~ged

Context

Limits and colimits

\tableofcontents

Definition

A wide pullback in a category $\mathcal{C}$ is a product (of arbitrary cardinality) in a slice category $\mathcal{C} \downarrow C$ . In terms of $\mathcal{C}$ , this can be expressed as a limit over a category obtained from a discrete category by adjoining a terminal object.

Yet more explicitly, the wide pullback of a family of morphisms $f_i\colon A_i \to C$ (a wide cospan) is an object $P$ equipped with projection $p_i\colon P\to A_i$ such that $f_i p_i$ is independent of $i$ , and which is universal with this property.

Binary wide pullbacks are the same as ordinary pullbacks, a.k.a. fiber products.

Of course, a wide pushout is a wide pullback in the opposite category.

Properties

A category has wide pullbacks (of all small cardinalities) if and only if it has (binary) pullbacks and cofiltered limits.
The saturation of the class of wide pullbacks is the class of limits over categories $C$ whose fundamental groupoid $\Pi_1(C)$ is trivial.

On the other hand, together with a terminal object, wide pullbacks generate all limits:

Proposition

A category $C$ with all wide pullbacks and a terminal object $1$ is complete. If $C$ is complete and $F\colon C \to D$ preserves wide pullbacks and the terminal object, then it preserves all limits.

Proof

To build up arbitrary products $\prod_{i \in I} c_i$ in $C$ , take the wide pullback of the family $c_i \to 1$ . Then to build equalizers of diagrams $f, g\colon c \rightrightarrows d$ , construct the pullback of the diagram

\array{ & & d \\ & & \downarrow \delta \\ c & \underset{\langle f, g \rangle}{\to} & d \times d }

From products and equalizers, we can get arbitrary limits.

In dependent type theory

~~In dependent type theory, the wide pullback of a family of functions $f:\prod_{i:I} A(i) \to C$ is given by the type~~

Wide pullbacks

~~$\sum_{y:C} \prod_{i:I} \sum_{x:A(i)} f(i, x) =_C y$~~

In dependent type theory, the wide pullback of a family of functions $f:\prod_{i:I} A(i) \to C$ is given by the type

\sum_{y:C} \prod_{i:I} \sum_{x:A(i)} f(i, x) =_C y

Since dependent type theory is the internal logic of locally cartesian closed (infinity,1)-categories, this implies that any locally cartesian closed (infinity,1)-category with a terminal object is complete.

Wide pushouts

Recall that the binary pushout of a family of functions $f:\prod_{x:\mathbb{2}} A \to C(x)$ indexed by the boolean domain $\mathbb{2}$ is a higher inductive type $\bigsqcup_{x:\mathbb{2}}^{A, f} C(x)$ generated by the functions

\mathrm{in}:\prod_{x:\mathbb{2}} C(x) \to \bigsqcup_{x:\mathbb{2}}^{A, f} C(x)

\mathrm{glue}:\prod_{z:A} \mathrm{in}(0, f(0, z)) = \mathrm{in}(1, f(1, z))

The glue constructor can be rephrased to the constructor

\mathrm{glue}:\prod_{z:A} \sum_{c:\bigsqcup_{x:\mathbb{2}}^{A, f} C(x)} \prod_{x:\mathbb{2}} \mathrm{in}(x, f(x, z)) = c

which by the type theoretic axiom of choice is the same as the constructor

\mathrm{glue}:\sum_{C:A \to \bigsqcup_{x:\mathbb{2}}^{A, f} C(x)} \prod_{z:A} \prod_{x:\mathbb{2}} \mathrm{in}(x, f(x, z)) = C(z)

or the two constructors

\mathrm{contr}:A \to \bigsqcup_{x:\mathbb{2}}^{A, f} C(x)

\mathrm{glue}:\prod_{z:A} \prod_{x:\mathbb{2}} \mathrm{in}(x, f(x, z)) = \mathrm{contr}(z)

Then generalizing from the boolean domain $\mathbb{2}$ to any index type $I$ , the wide pushout of a family of functions $f:\prod_{x:I} A \to C(x)$ is a higher inductive type $\bigsqcup_{x:I}^{A, f} C(x)$ generated by the functions

\mathrm{in}:\prod_{x:I} C(x) \to \bigsqcup_{x:I}^{A, f} C(x)

\mathrm{contr}:A \to \bigsqcup_{x:I}^{A, f} C(x)

\mathrm{glue}:\prod_{z:A} \prod_{x:I} \mathrm{in}(x, f(x, z)) = \mathrm{contr}(z)

Wide pushouts are an example of a non-recursive higher inductive type.

Related concepts

connected limit

Notions of pullback:

pullback, fiber product (limit over a cospan)
wide pullback
lax pullback, comma object (lax limit over a cospan)
(∞,1)-pullback, homotopy pullback, ((∞,1)-limit over a cospan)
base change, context extension
pullback bundle
contravariant functor

References

The terminology wide pullback appears in:

Paul Taylor, Quantitative domains, groupoids and linear logic, Category Theory and Computer Science: Manchester, UK, September 5–8, 1989 Proceedings. Springer Berlin Heidelberg, 1989.

Wide pullbacks are considered under the term fibred product in:

Robert Paré, Simply connected limits. Can. J. Math., Vol. XLH, No. 4, 1990, pp. 731-746, CMS

Revision on February 10, 2024 at 06:15:36 by John Walsh See the history of this page for a list of all contributions to it.