background image

CHAPTER 19

Pointfree funcoids

This chapter is based on [

29

].

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.

19.1. Definition

Definition

1486

.

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

1487

.

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

1488

.

I will denote

pFCD

(

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

.

h

(

A

,

B

, α, β

)

i

def

=

α

for every pointfree funcoid (

A

,

B

, α, β

).

Definition

1489

.

(

A

,

B

, α, β

)

1

= (

B

,

A

, β, α

) for every pointfree funcoid

(

A

,

B

, α, β

).

Proposition

1490

.

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

1491

.

(

f

1

)

1

=

f

for every pointfree funcoid

f

.

Definition

1492

.

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.

Obvious

1493

.

x

[

f

]

y

y

6 h

f

i

x

x

6

f

1

y

for every pointfree funcoid

f

and

x

Src

f

,

y

Dst

f

.

Obvious

1494

.

f

1

=[

f

]

1

for every pointfree funcoid

f

.

Theorem

1495

.

Let

A

and

B

be posets. Then:

283