background image

In addition to atoms

A

x

, the set of atoms under an element

x

of a poset

A

we will write just

atoms

A

for all atoms of a poset

A

.

3 Pointfree funcoids

3.1 Definition

Definition 1.

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

B

α x

x

A

β y

)

.

Definition 2.

The

source

Src

(

A

;

B

;

α

;

β

) =

A

and

destination

Dst

(

A

;

B

;

α

;

β

) =

B

for every

pointfree funcoid

(

A

;

B

;

α

;

β

)

.

Definition 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 4.

If

A

and

B

have least elements, then

FCD

(

A

;

B

)

has least element.

Proof.

It is

(

A

;

B

;

A

× {

0

B

}

;

B

× {

0

A

}

)

.

Definition 5.

h

(

A

;

B

;

α

;

β

)

i

=

def

α

for a pointfree funcoid

(

A

;

B

;

α

;

β

)

.

Definition 6.

(

A

;

B

;

α

;

β

)

1

= (

B

;

A

;

β

;

α

)

for a pointfree funcoid

(

A

;

B

;

α

;

β

)

.

Proposition 7.

If

f

is a pointfree funcoid then

f

1

is also a pointfree funcoid.

Proof.

Follows from symmetry in the definition of pointfree funcoid.

Obvious 8.

(

f

1

)

1

=

f

for a pointfree funcoid

f

.

Definition 9.

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

Dst

f

h

f

i

x.

Obvious 10.

x

[

f

]

y

y

Dst

f

h

f

i

x

x

Src

f

h

f

1

i

y

for every pointfree funcoid

f

and

x

Src

f

,

y

Dst

f

.

Obvious 11.

[

f

1

]=[

f

]

1

for a pointfree funcoid

f

.

Theorem 12.

Let

A

and

B

are posets. Then:

1. If

A

is separable, for given value of

h

f

i

exists no more than one

f

FCD

(

A

;

B

)

;

2. If

A

and

B

are separable, for given value of

[

f

]

exists no more than one

f

FCD

(

A

;

B

)

.

Proof.

Let

f , g

FCD

(

A

;

B

)

.

1. Let

h

f

i

=

h

g

i

. Then for every

x

A

,

y

B

we have

x

A

h

f

1

i

y

y

B

h

f

i

x

y

B

h

g

i

x

x

A

h

g

1

i

y

and thus by separability of

A

we have

h

f

1

i

y

=

h

g

1

i

y

that is

h

f

1

i

=

h

g

1

i

and so

f

=

g

.

2. Let

[

f

]=[

g

]

. Then for every

x

A

,

y

B

we have

y

B

h

f

i

x

x

[

f

]

y

x

[

g

]

y

y

B

h

g

i

x

and thus by separability of

B

we have

h

f

i

x

=

h

g

i

x

that is

h

f

i

=

h

g

i

. Similarly we have

h

f

1

i

=

h

g

1

i

. Thus

f

=

g

.

Proposition 13.

If Dst

f

is separable, then

h

f

i

0

Src

f

= 0

Dst

f

for every pointfree funcoid

f

.

2

Section 3