nLab coalgebra of the real interval




This article is about structure on a closed interval of real numbers, generally taken to be I=[0,1]I = [0, 1], that is derivable from a coalgebraic perspective. This topic was introduced by Peter Freyd in a posting about the paper by Dusko Pavlovic and Vaughan Pratt.

Coalgebraic description of II

For the moment we work classically, over the category of sets. A bipointed set is a set equipped with two elements, that is a cospan of the form

1 1 x 0 x 1 X \array{ 1 & & & & 1 \\ & ^\mathllap{x_0} \searrow & & \swarrow^\mathrlap{x_1} & \\ & & X & & }

where x 0x_0 and x 1x_1 might coincide. There is a monoidal product on Cospan(1,1)Cospan(1, 1) given by cospan composition (formed by taking pushouts); this monoidal product is denoted \vee. (Explicitly, (X,x 0,x 1)(Y,y 0,y 1)(X,x_0,x_1) \vee (Y,y_0,y_1) is ((XY)/(x 1y 0),x 0,y 1)((X \uplus Y)/(x_1 \sim y_0), x_0, y_1).) The monoidal unit is a 11-element set with its unique bipointed structure. The category of such cospans or bipointed sets is denoted CosCos.

Inside CosCos is the full subcategory of two-pointed sets, where x 0x_0 and x 1x_1 are distinct. Let TwopTwop be the category of two-pointed sets. The monoidal product \vee restricts to a functor

:Twop×TwopTwop\vee \colon Twop \times Twop \to Twop

and one can define the square

sq=(TwopΔTwop×TwopTwop)sq = (Twop \stackrel{\Delta}{\to} Twop \times Twop \stackrel{\vee}{\to} Twop)

A sqsq-coalgebra is a two-pointed set XX together with a map ξ:XXX\xi: X \to X \vee X. An example is given by I=[0,1]I = [0, 1], where III \vee I is identified with the interval [0,2][0, 2] and the coalgebra structure IIII \to I \vee I is identified with multiplication by 22, [0,1][0,2][0, 1] \to [0, 2]. This map will be denoted α\alpha.

Theorem (Freyd)

(I,α)(I, \alpha) is terminal in the category of sqsq-coalgebras.

Corecursively defined operations on II

We now define a number of operations on II. For 0x10 \leq x \leq 1, define xmin(2x,1){x \uparrow} \coloneqq \min(2 x, 1) and xmax(2x1,0){x \downarrow} \coloneqq \max(2 x - 1, 0). These give unary operations on II which can also be defined as maps in CosCos using the coalgebra structure α\alpha:

I()I=(IαIII!I1I)I \stackrel{{(-) \uparrow}}{\to} I = (I \stackrel{\alpha}{\to} I \vee I \stackrel{I \vee !}{\to} I \vee 1 \cong I)
I()I=(IαII!I1II)I \stackrel{{(-) \downarrow}}{\to} I = (I \stackrel{\alpha}{\to} I \vee I \stackrel{! \vee I}{\to} 1 \vee I \cong I)

We similarly define unary operations (){(-)\uparrow}, (){(-) \downarrow} for any sqsq-coalgebra (X,ξ)(X, \xi). For any coalgebra XX and xXx \in X, either x=x 0{x \downarrow} = x_0 or x=x 1{x \uparrow} = x_1. Moreover, if i 0:XXXi_0 \colon X \to X \vee X and i 1:XXXi_1 \colon X \to X \vee X are the evident pushout inclusions, we have ξ(x)=i 0(x)\xi(x) = i_0({x \uparrow}) if x=x 0{x \downarrow} = x_0, and ξ(x)=i 1(x)\xi(x) = i_1({x \downarrow}) if x=x 1{x \uparrow} = x_1. This means that coalgebra structures can be recovered from algebraic structures consisting of two constants x 0,x 1x_0, x_1 and two unary operations \uparrow, \downarrow, although we must consider a coherent but non-algebraic axiom

x=x 1orx=x 0\vdash {x \uparrow} = x_1 or {x \downarrow} = x_0

Order-theoretic operations

Next, we define meet and join operations on II, making it a lattice, by exploiting corecursion. A slick corecursive definition of the order \leq is that xyx \leq y

  • if x=0{x \downarrow} = 0 and xy{x \uparrow} \leq {y \uparrow}, or

  • if y=1{y \uparrow} = 1 and xy{x \downarrow} \leq {y \downarrow}.

If one prefers to work with operations, one could define the meet operation :I×II\wedge \colon I \times I \to I by putting a suitable coalgebra structure on I×II \times I and using terminality of the coalgebra II to define \wedge as a coalgebra map. A coalgebra structure

ξ:I×I(I×I)(I×I)\xi \colon I \times I \to (I \times I) \vee (I \times I)

which works is

  • ξ(x,y)=i 0(x,y)\xi(x, y) = i_0({x \uparrow}, {y \uparrow}) if x=0{x \downarrow} = 0 or y=0{y \downarrow} = 0;

  • ξ(x,y)=i 1(x,y)\xi(x, y) = i_1({x \downarrow}, {y \downarrow}) if x=1=y{x \uparrow} = 1 = {y \uparrow}.

Midpoint operations

The general midpoint operation is not as easy to construct as one might think, but to start with we do have operations which take the midpoint between a given point and an endpoint. Namely, the left midpoint operation is the unary operation defined by

l=(Ii 0IIα 1I)l = (I \stackrel{i_0}{\to} I \vee I \stackrel{\alpha^{-1}}{\to} I)

and the right midpoint operation is defined by

r=(Ii 1IIα 1I).r = (I \stackrel{i_1}{\to} I \vee I \stackrel{\alpha^{-1}}{\to} I).

Constructive aspects

There are two versions of this construction, classically equivalent, in constructive mathematics, one of which produces the unit interval of MacNeille real numbers, the other of which produces the unit interval of located Dedekind real numbers. Both start with CosCos (which is straightforward) but define TwopTwop differently, and the monoidal product \vee is subtler.

For the MacNeille real numbers, define Twop MTwop_M in the most obvious way,

¬x 0=x 1. \neg\; x_0 = x_1 .

For the Dedekind real numbers, define Two DTwo_D by requiring

x,¬x=x 0¬x=x 1. \forall x,\; \neg\; x = x_0 \;\vee\; \neg\; x = x_1 .

(The two statements are equivalent assuming the classical de Morgan law ¬(pq)¬p¬q\neg(p \wedge q) \Rightarrow \neg{p} \vee \neg{q}, but the latter is stronger in intuitionistic logic.)

In CosCos, let XYX \vee Y be a subset of X×YX \times Y, with (x,y)XY(x,y) \in X \vee Y iff

(¬x=x 1y=y 0)(¬y=y 0x=x 1). (\neg\; x = x_1 \;\Rightarrow\; y = y_0) \;\wedge\; (\neg\; y = y_0 \;\Rightarrow\; x = x_1) .

(A pushout can be constructed using x=x 1y=y 0x = x_1 \;\vee\; y = y_0 instead; this is stronger in intuitionistic logic but equivalent assuming excluded middle. If equality happens to be stable in XX and YY, then only the classical de Morgan law is needed to make this a pushout.)

As in the classical case, this makes Twop MTwop_M and Twop DTwop_D into “semigroupal” categories (monoidal categories but without the monoidal unit), since the unit object (which exists in CosCos as the singleton) does not exist in Twop MTwop_M or in Twop DTwop_D, but we can still define sq Msq_M and sq Dsq_D and consider their coalgebras. As stated above, [0,1] M[0,1]_M is the final coalgebra of sq Msq_M, and [0,1]=[0,1] D[0,1] = [0,1]_D is the final coalgebra of sq Dsq_D; both are equipped with 00 and 11.

Another approach to the Dedekind real interval looks simpler from the perspective of constructive analysis. Start with Set #Set_\#, the category of T 0T_0 point–point apartness spaces and strongly extensional functions between them. (A point–point apartness space is a set equipped with an apartness relation, that is a binary relation #\# satisfying properties dual to those of an equivalence relation; it is T 0T_0 iff the apartness relation is tight; and a function between such spaces is strongly extensional iff it reflects ##.) On Cos #Cos_\#, let XYX \vee Y be the subset of X×YX \times Y satisfying

(x#x 1y=y 0)(y#y 0x=x 1). (x \# x_1 \;\Rightarrow\; y = y_0) \;\wedge\; (y \# y_0 \;\Rightarrow\; x = x_1) .

Define Twop #Twop_\# by

x#x 0x#x 1. x \# x_0 \;\vee\; x \# x_1 .

Now defining sq #sq_\# on Twop #Twop_\#, its final coalgebra is again the Dedekind unit interval (equipped with its endpoints).

Computational aspects

… explain how the classical version corresponds to computation with (unsigned) binary digits … the constructive (Dedekind) version corresponds to computation with signed binary digits …


The constructive version is also due to Freyd:

  • Peter Freyd, Reality Check, post to the categories list, July 31, 2000 (web)

Freyd published 8 years later:

  • Peter Freyd, Algebraic Real Analysis, TAC 20 no.10 (2008) pp. 215–306. (web)

There is also a complete development in the Elephant:

Last revised on February 7, 2024 at 14:25:48. See the history of this page for a list of all contributions to it.