*** Welcome to piglix ***

Chu space


Chu spaces generalize the notion of topological space by dropping the requirements that the set of open sets be closed under union and finite intersection, that the open sets be extensional, and that the membership predicate (of points in open sets) be two-valued. The definition of continuous function remains unchanged other than having to be worded carefully to continue to make sense after these generalizations.

The name is due to Po-Hsaing Chu, who originally constructed a verification of autonomous categories as a grad student under the direction of Michael Barr in 1979

Understood statically, a Chu space (A, r, X) over a set K consists of a set A of points, a set X of states, and a function r : A × XK. This makes it an A × X matrix with entries drawn from K, or equivalently a K-valued binary relation between A and X (ordinary binary relations being 2-valued).

Understood dynamically, Chu spaces transform in the manner of topological spaces, with A as the set of points, X as the set of open sets, and r as the membership relation between them, where K is the set of all possible degrees of membership of a point in an open set. The counterpart of a continuous function from (A, r, X) to (B, s, Y) is a pair (f, g) of functions f : AB, g : YX satisfying the adjointness condition s(f(a), y) = r(a, g(y)) for all aA and yY. That is, f maps points forwards at the same time as g maps states backwards. The adjointness condition makes g the inverse image function f−1, while the choice of X for the codomain of g corresponds to the requirement for continuous functions that the inverse image of open sets be open. Such a pair is called a Chu transform or morphism of Chu spaces.

A topological space (X, T) where X is the set of points and T the set of open sets, can be understood as a Chu space (X,∈,T) over {0, 1}. That is, the points of the topological space become those of the Chu space while the open sets become states and the membership relation " ∈ " between points and open sets is made explicit in the Chu space. The condition that the set of open sets be closed under arbitrary (including empty) union and finite (including empty) intersection becomes the corresponding condition on the columns of the matrix. A continuous function fX → X' between two topological spaces becomes an adjoint pair (f,g) in which f is now paired with a realization of the continuity condition constructed as an explicit witness function g exhibiting the requisite open sets in the domain of f.


...
Wikipedia

...