background image

Obvious 15.10.

x

[

f

]

y

,

y

/

h

f

i

x

,

x

/

h

f

¡

1

i

y

for every pointfree funcoid

f

and

x

2

Src

f

,

y

2

Dst

f

.

Obvious 15.11.

[

f

¡

1

]=[

f

]

¡

1

for every pointfree funcoid

f

.

Theorem 15.12.

Let

A

and

B

be posets. Then:

1. If

A

is separable, for given value of

h

f

i

there exists no more than one

f

2

FCD

(

A

;

B

)

.

2. If

A

and

B

are separable, for given value of

[

f

]

there exists no more than one

f

2

FCD

(

A

;

B

)

.

Proof.

Let

f ; g

2

FCD

(

A

;

B

)

.

1. Let

h

f

i

=

h

g

i

. Then for every

x

2

A

,

y

2

B

we have

x

/

h

f

¡

1

i

y

,

y

/

h

f

i

x

,

y

/

h

g

i

x

,

x

/

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

2

A

,

y

2

B

we have

y

/

h

f

i

x

,

x

[

f

]

y

,

x

[

g

]

y

,

y

/

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

If Src

f

and Dst

f

have least elements, then

h

f

i

0

Src

f

= 0

Dst

f

for every

pointfree funcoid

f

.

[TODO: Previously I required separability of Dst

f

. It turned out to be a

superuous condition. Remove it also in consequences of this proposition.]

Proof.

y

/

h

f

i

0

Src

f

,

0

Src

f

/

h

f

¡

1

i

y

,

0

for every

y

2

Dst

f

. Thus

h

f

i

0

Src

f

 h

f

i

0

Src

f

. So

h

f

i

0

Src

f

= 0

Dst

f

.

Proposition 15.14.

If Dst

f

is a separable meet-semilattice then

h

f

i

is a monotone function

(for a pointfree funcoid

f

).

[FIXME: Added condition to be a meet-semilattice, add it also in all

consequences.]

[TODO: Check whether existence of least element of Dst

f

is required (in theorem

3.14

).]

Proof.

a

v

b

) 8

x

2

Dst

f

: (

a

/

h

f

¡

1

i

x

)

b

/

h

f

¡

1

i

x

)

) 8

x

2

Dst

f

: (

x

/

h

f

i

a

)

x

/

h

f

i

b

)

,

?

h

f

i

a

?

h

f

i

b

) h

f

i

a

v h

f

i

b

(used theorem

3.14

and that it is a separable meet-semilattice).

Theorem 15.15.

Let

f

be a pointfree funcoid from a starrish join-semilattice Src

f

to a separable

starrish join-semilattice Dst

f

. Then

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

for every

i; j

2

Src

f

.

Proof.

?

h

f

i

(

i

t

j

) =

f

y

2

Dst

f

j

y

/

h

f

i

(

i

t

j

)

g

=

f

y

2

Dst

f

j

i

t

j

/

h

f

¡

1

i

y

g

=

f

y

2

Dst

f

j

i

/

h

f

¡

1

i

y

_

j

/

h

f

¡

1

i

y

g

=

f

y

2

Dst

f

j

y

/

h

f

i

i

_

y

/

h

f

i

j

g

=

f

y

2

Dst

f

j

y

/

h

f

i

i

t h

f

i

j

g

=

?

(

h

f

i

i

t h

f

i

j

)

:

Thus

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

by separability.

Proposition 15.16.

Let

f

be a pointfree funcoid. Then:

1.

k

[

f

]

i

t

j

,

k

[

f

]

i

_

k

[

f

]

j

for every

i; j

2

Dst

f

,

k

2

Src

f

if Dst

f

is a starrish join-semilattice.

2.

i

t

j

[

f

]

k

,

i

[

f

]

k

_

j

[

f

]

k

for every

i; j

2

Src

f

,

k

2

Dst

f

if Src

f

is a starrish join-semilattice.

Proof.

1.

k

[

f

]

i

t

j

,

i

t

j

/

h

f

i

k

,

i

/

h

f

i

k

_

j

/

h

f

i

k

,

k

[

f

]

i

_

k

[

f

]

j

.

2. Similar.

178

Pointfree funcoids