Finn Lawler thesis outline (Rev #4)

This page is for material relevant to my Ph.D. thesis — I will try to sketch the important bits here as I write up the document itself.

Chapter 2

There are two quite different ways to construct the effective topos: we start with the Kleene algebra (,)(\mathbb{N}, \cdot) of partial recursive functions, and then

  1. construct the effective tripos,

    • this is the hyperdoctrine ET\mathbf{ET} over SetSet whose predicates over XX are \mathbb{N}-valued sets XPX \to P\mathbb{N}, ordered by ϕψ\phi \leq \psi if there exists a partial recursive function Φ\Phi such that for any xXx \in X and nϕxn \in \phi x, Φn\Phi n is defined and contained in ψx\psi x.

    and then take its category of partial equivalence relations; or

  2. construct the regular category of assemblies over \mathbb{N}

    and take its exact completion.

We show how the two are related.

The category of pers

Let EB\mathbf{E} \to \mathbf{B} be an ordered regular fibration. A partial equivalence relation over the type XBX \in \mathbf{B} is relation RR on XX that is symmetric and transitive:

R(x 1,x 2) R(x 2,x 1) R(x 1,x 2),R(x 2,x 3) R(x 1,x 3) \begin{aligned} R(x_1, x_2) & \Rightarrow R(x_2, x_1) \\ R(x_1, x_2), R(x_2, x_3) & \Rightarrow R(x_1, x_3) \end{aligned}

A morphism (R,X)(S,Y)(R, X) \to (S, Y) of pers is a relation F:X,YF \colon X, Y that satisfies

F(x,y) R(x,x)S(y,y) F(x 1,y 1)R(x 1,x 2)S(y 1,y 2) F(x 2,y 2) F(x,y 1)F(x,y 2) S(y 1,y 2) R(x,x) υ.F(x,υ) \begin{aligned} F(x,y) & \Rightarrow R(x,x) \wedge S(y,y) \\ F(x_1,y_1) \wedge R(x_1, x_2) \wedge S(y_1, y_2) & \Rightarrow F(x_2,y_2) \\ F(x,y_1) \wedge F(x,y_2) & \Rightarrow S(y_1,y_2) \\ R(x,x) & \Rightarrow \exists \upsilon . F(x, \upsilon) \end{aligned}

These form a category Per(E)Per(\mathbf{E}). The effective topos is Per(ET)Per(\mathbf{ET}).

The exact completion

The category Asm\mathbf{Asm} of assemblies is regular, so the allegory Rel(Asm)Rel(\mathbf{Asm}) is unitary and tabular. Its effective completion is the splitting of equivalences Rel(Asm)[eqvˇ]Rel(\mathbf{Asm})[\check{\mathrm{eqv}}]: an equivalence is a symmetric monad, and these are the objects of the splitting, while a morphism is a module.

The exact completion of Asm\mathbf{Asm} is category of maps in this allegory.

Allegories vs. bicategories of relations

A unitary pre-tabular allegory is the same thing as a bicategory of relations. This extends to an equivalence of 2-categories.

We define a framed bicategory of relations to be a (locally ordered) framed bicategory that is a bicategory of relations in which all cartesian-product structure morphisms are ‘tight’ (or ‘representable’) maps. Then

Theorem

The 2-categories of ordered regular fibrations and of framed bicategories of relations are equivalent.

Proof

(sketch). From a regular fibration E\mathbf{E} over B\mathbf{B} we construct a bicategory Matr(E)Matr(\mathbf{E}), whose objects are those of B\mathbf{B} and whose morphisms XYX \to Y are the objects of E(X×Y)\mathbf{E}(X \times Y). Composition is given by the usual composite of relations

SR(xz)=[υ.R(x,υ)S(υ,z)] S R(x z) = [ \exists \upsilon . R(x,\upsilon) \wedge S(\upsilon,z) ]

One then shows that this is a framed bicategory of relations, with category of tight maps given by B\mathbf{B}.

Conversely, the inclusion i:TMap()i \colon TMap(\mathcal{B}) \to \mathcal{B} gives rise to a pseudofunctor Pred()(i,I):TMap() opCatPred(\mathcal{B}) \mathcal{B}(i-, I) \colon TMap(\mathcal{B})^{\mathrm{op}} \to Cat, where II is the tensor unit of \mathcal{B}. It is a regular fibration, and Pred()Pred(-) and Matr()Matr(-) form an equivalence of 2-categories.

Proposition

The full sub-bicategory of Rel(Asm)Rel(\mathbf{Asm}) on the constant assemblies is equivalent to Matr(ET)Matr(\mathbf{ET}).

Proposition

Rel(Asm)Rel(\mathbf{Asm}) is equivalent to the splitting Matr(ET)[crfˇ]Matr(\mathbf{ET})[\check{\mathrm{crf}}] of the coreflexive morphisms in Matr(ET)Matr(\mathbf{ET}).

Revision on November 23, 2012 at 01:35:19 by Finn Lawler?. See the history of this page for a list of all contributions to it.