 Chapter 15
Pointfree funcoids

This chapter is based on [

28

].

This is a routine chapter. There is almost nothing creative here. I just generalize theorems

about funcoids to the maximum extent for

pointfree funcoids

(dened below) preserving the proof

idea. The main idea behind this chapter is to nd weakest theorem conditions enough for the same
theorem statement as for above theorems for funcoids.

For these who know pointfree topology: Pointfree topology notions of frames and locales is a

non-trivial generalization of topological spaces. Pointfree funcoids are dierent: I just replace the
set of lters on a set with an arbitrary poset, this readily gives the denition of

pointfree funcoid

,

almost no need of creativity here.

Pointfree funcoids are used in the below denitions of products of funcoids.

15.1 Denition

Denition 15.1.

Pointfree funcoid

(

A

;

B

;

;

)

where

A

and

B

are posets,

2

B

A

and

2

A

B

such that

8

x

2

A

; y

2

B

: (

y

/

x

,

x

/

y

)

:

Denition 15.2.

The

source

Src

(

A

;

B

;

;

) =

A

and

destination

Dst

(

A

;

B

;

;

) =

B

for every

pointfree funcoid

(

A

;

B

;

;

)

.

To every funcoid

(

A

;

B

;

;

)

corresponds pointfree funcoid

(

P

A

;

P

B

;

;

)

. Thus pointfree

funcoids are a generalization of funcoids.

Denition 15.3.

I will denote

FCD

(

A

;

B

)

the set of pointfree funcoids from

A

to

B

(that is with

source

A

and destination

B

), for every posets

A

and

B

.

Proposition 15.4.

If

A

and

B

have least elements, then

FCD

(

A

;

B

)

has least element.

[TODO:

Move below where order of pointfree funcoids is dened.]

Proof.

It is

(

A

;

B

;

A

f

0

B

g

;

B

f

0

A

g

)

.

Denition 15.5.

h

(

A

;

B

;

;

)

i

=

def

for every pointfree funcoid

(

A

;

B

;

;

)

.

Denition 15.6.

(

A

;

B

;

;

)

¡

1

= (

B

;

A

;

;

)

for every pointfree funcoid

(

A

;

B

;

;

)

.

Proposition 15.7.

If

f

is a pointfree funcoid then

f

¡

1

is also a pointfree funcoid.

Proof.

It follows from symmetry in the denition of pointfree funcoid.

Obvious 15.8.

(

f

¡

1

)

¡

1

=

f

for every pointfree funcoid

f

.

Denition 15.9.

The relation

[

f

]

2

P

(

Src

f

Dst

f

)

is dened by the formula (for every pointfree

funcoid

f

and

x

2

Src

f

,

y

2

Dst

f

)

x

[

f

]

y

=

def

y

/

h

f

i

x:

177