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 Freyd.

Coalgebraic description of II

For the moment we work classically, over the category SetSet. A bipointed set 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. The monoidal unit is a 1-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. (N.B. When we go beyond the classical case, we need a more refined analysis involving notions of apartness, separation, etc.) 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).


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

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

Revised on July 16, 2014 01:28:34 by Thomas Holder (