Date: Mon, 19 May 1997 09:19:34 -0300 (ADT)
Subject: Scott is Phoa, locally 

Date: Mon, 19 May 1997 13:29:05 MESZ
From: Thomas Streicher <streicher@mathematik.th-darmstadt.de>

In a paper circulated since end of last year Dana Scott has proposed a category
PEQU of algebraic lattices with partial equivalence relations as objects and
equivariant Scott continuous maps as morphisms. One nice thing about PEQU is
that Scott has shown it to be equivalent to the category EQU of T_0 spaces
with (total) equivalence relations and equivariant continuous maps.
It has been shown (by students of Scott) that PEQU is not even well-powered 
despite being regular and locally cartesian closed 
(in particular, it is a logos and thus a model for FOL).
 
If one considers $\omega$-PEQU, the category of $\omega$-algebraic lattices
with partial equivalence relations as objects and equivariant Scott continuous
maps as morphisms, then it can be shown easily to be equivalent to 
PER(P $\omega$), the category of pers over the good old P $\omega$ model of 
lambda calculus, which embeds into Ass(P $\omega$), the category of assemblies
over P $\omega$ and finally into RT(P $\omega$), the realisability topos over
P $\omega$. All these full inclusions are reflective. This realisability model
has been studied by Wesley Phoa in his Thesis (1990) and in his paper 

     "Building Domains from Graph Models" (MSCS, 1992).
 
The reason for the equivalence of $\omega$-PEQU and PER(P $\omega$) is that
any $\omega$-algebraic lattice L is contained in P $\omega$ via an inflationary
retract e : L -> P $\omega$ , p : P $\omega$ -> L. Now if R is a per on L then
P $\omega$ may be endowed with the per 
 
       e[R] := { (e(x),e(y)) | x R y }
 
and the pair e,p of equivariant Scott continuous maps establishes an 
isomorphism between (L,R) and (P $\omega$ , e[R]).
 
This observation does not hinge on countable cardinality. For any cardinal 
$\kappa$ we may consider $\kappa$-PEQU (where the bases of the algebraic 
lattices are required to have cardinality less or equal $\kappa$) 
and show it to be equivalent to PER(P $\kappa$) by the same argument as above.
The reason why this is possible is that any infinite set M contains 
List(M) x M as a retract and therefore can be endowed with a graph model 
structure -- as emphasised by Scott.
 
The benefits of this (simple) observation are the following

(1) $\kappa$-PEQU does not admit a generic (regular) mono 
    (= weak s.o. classifier) as for any partial combinatory algebra A 
    the category PER(A) does not admit such 
    (as each homset has cardinality less or equal |A| and 
     there are 2^{|A|} (regular) subobjects of (A, \Delta(A)))
    but, never mind, the required weak / strong classifiers live in
    Ass(A) / RT(A) , respectively
 
(2) Phoa already has started to investigate SDT in PER(P $\omega$),
    one may take as a dominance (S , \Delta(S)) where S is Sierpinski space
    together with [t] : ({*} , \Delta({*})) -> (S , \Delta(S)) 
    where t(*) = \top.
    The same may be taken as a dominance for PEQU without any size 
    restrictions.
 
Anyway, PEQU appears as an amalgamation of ALL realisability models over
graph models of all size. Assuming a Grothendieck universe U we may consider
(the fairly big) graph model  P U  appearing most naturally so 
as we have List(U) x U \subseteq U. 
Thus PER(P U) contains PEQU, i.e. EQU, when one restricts the underlying
algebraic lattices / T_0 spaces of PEQU / EQU to live in universe U. 
But notice that (P U , \Delta(P U)) lives outside this PEQU.
Anyway, PER(P U), Ass(P U), RT(P U) appear as the appropriate models of logic
in which to study Scott's recently proposed categories. 
>From the point of view of mathematical practice, however, the restriction to 
cardinality $\omega$ does not seem to be too restrictive as most spaces in
"real" mathematics have a countable base (e.g. separable metric spaces).

 Thomas Streicher