 CHAPTER 15

Pointfree funcoids

This chapter is based on [

28

].

This is a routine chapter. There is almost nothing creative here. I just general-

ize theorems about funcoids to the maximum extent for

pointfree funcoids

(defined

below) preserving the proof idea. The main idea behind this chapter is to find

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 different: I just replace the set of filters on a set with an arbitrary poset, this

readily gives the definition of

pointfree funcoid

, almost no need of creativity here.

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

15.1. Definition

Definition

1057

.

Pointfree funcoid

is a quadruple (

A

;

B

;

α

;

β

) where

A

and

B

are posets,

α

B

A

and

β

A

B

such that

x

A

, y

B

: (

y

6

αx

x

6

βy

)

.

Definition

1058

.

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.

Definition

1059

.

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

1060

.

If

A

and

B

have least elements, then

FCD

(

A

;

B

) has least

element.

FiXme

: Move below where order of pointfree funcoids is defined.

Proof.

It is (

A

;

B

;

A

× {⊥

B

}

;

B

× {⊥

A

}

).

Definition

1061

.

h

(

A

;

B

;

α

;

β

)

i

def

=

α

for every pointfree funcoid (

A

;

B

;

α

;

β

).

Definition

1062

.

(

A

;

B

;

α

;

β

)

1

= (

B

;

A

;

β

;

α

) for every pointfree funcoid

(

A

;

B

;

α

;

β

).

Proposition

1063

.

If

f

is a pointfree funcoid then

f

1

is also a pointfree

funcoid.

Proof.

It follows from symmetry in the definition of pointfree funcoid.

Obvious

1064

.

(

f

1

)

1

=

f

for every pointfree funcoid

f

.

Definition

1065

.

The relation [

f

]

P

(Src

f

×

Dst

f

) is defined by the formula

(for every pointfree funcoid

f

and

x

Src

f

,

y

Dst

f

)

x

[

f

]

y

def

=

y

6 h

f

i

x.

199