Subject: Re: functions Omega->Omega

From: categories <[email-masked]>
Date: Wed, 2 Jul 1997 13:33:45 -0300 (ADT)

Date: Tue, 1 Jul 1997 16:22:06 -0400 (EDT)
From: Todd Wilson <[email-masked]>

Paul Taylor asks:

> 	f(a) & a  =  f(true) & a
> 
> I wonder whether anyone has noticed this formula before?

There is a section of my thesis devoted to operators on Heyting
algebras that satisfy this formula.  More generally, I considered
"extensional operators" l : A -> A (A is a H.A.), which are
characterized by any of the following equivalent conditions:

(a) x C y implies l(x) C l(y)  (x,y in A, C a Heyting-congruence on A)
(b) a & l(x) <= l(a * x) <= a -> l(x)  (a,x in A, * in {&,->})
(c) a * l(x) = a * l(a o x)   (a,x in A, *,o in {&,->})
(d)  a * x = a * y  implies  a o l(x) = a o l(y) (a,x,y in A, *,o in {&,->})
(e)  x <-> y <= l(x) <-> l(y)  (x,y in A)

The name "extensional operator" comes from (e).  If A is complete,
extensional operators on A are in 1-1 correspondence with morphisms
Omega -> Omega in the topos Sh(A).  "Logical operators" are what I
called extensional operators satisfying l(true) = true -- or,
equivalently, x <= l(x) (x in A).  The quasinuclei of Banaschewski are
then precisely the monotone logical operators, and nuclei are
(therefore) precisely the extensional closure operators.

Arbitrary extensional operators can be "built" from "below" or from
"above" by specific extensional operators, generalizing the way nuclei
can be built from open, closed, and quasiclosed nuclei, and several
"structure theorems" of this kind exist.  One can also characterize
the subsets of A that can appear as the fixedpoint sets of logical
operators (equivalently the prefixedpoint sets of extensional
operators).

My thesis goes on to study "regular operators" -- the regular elements
in the lattice of logical operators, or, equivalently, those operators
r satisfying r(a->b) = a->r(b) (a,b in A) -- which have an amazing
number of properties (e.g., they are idempotent, they preserve
"regular" joins and "stable" meets, their fixedpoint sets are the same
as the fixedpoint sets of logical operators, any two regular operators
commute, and the join of regular operators is function composition, to
name several).  The set of regular operators on a frame A forms a
complete Boolean algebra isomorphic to N^2(A)/--, i.e., the
double-negation quotient of the *second assembly* of A (where N(A) =
the frame of nuclei on A = the frame of frame congruences on A; see
Johnstone, Stone Spaces, pp. 51--57, for more information on the
functor N and its iterates).  This provides a concrete embedding of
any frame into a complete Boolean algebra.

I have used the theory regular operators to derive an explicit formula
for joins of nuclei, characterize "free meets" in frames, and to
answer some questions about fibrewise-Boolean locales.  My thesis also
characterizes universal monos (and obtains some results about limits
and colimits) in the categories of frames and kappa-frames, and
generalizes some results of Banaschewki on finitely generated frame
extensions.  It appeared as CMU tech report CMU-CS-94-186.

Todd Wilson
Computer Science Department
Cornell University

---

From: categories <[email-masked]>
Date: Sat, 12 Jul 1997 14:55:00 -0300 (ADT)

Date: Fri, 11 Jul 1997 16:56:25 -0400 (EDT)
From: Andre Scedrov <[email-masked]>

          > I wonder whether anyone has noticed this formula before?

Similar formulas and their analogs in intuitionistic second-order 
propositional calculus are discussed in my paper in the Annals Pure 
Appl. Logic 27 (1984) 155-164. That paper was motivated by Higgs's 
observation that every monic  Omega -> Omega  in a topos is an involution, 
see Peter Johnstone's paper "Automorphisms of Omega" in Alg. Universalis 
9 (1979) 1-7. 

 Andre Scedrov

---

From: categories <[email-masked]>
Date: Mon, 14 Jul 1997 20:25:22 -0300 (ADT)

Date: Mon, 14 Jul 1997 14:24:43 -0400
From: Philip J. Scott <[email-masked]>

>see Peter Johnstone's paper "Automorphisms of Omega" in Alg. Universalis

For a logical proof of Higgs' theorem, based on the above observations
of Scedrov, see Lambek-Scott (Introd. to Higher Order Cat. Logic), p.160,
Exercise 4. A further result along these lines is in Lemma 12.3, p. 190 of
our book.

                        Phil Scott