background image

Proof.

y

h

f

i

0

Src

f

0

Src

f

h

f

1

i

y

0

y

0

Dst

f

. Thus by separability,

h

f

i

0

Src

f

= 0

Dst

f

.

Proposition 14.

If Dst

f

is a separable meet semilattice with least element then

h

f

i

is a monotone

function (for a pointfree funcoid

f

).

Proof.

a

b

⇒ ∀

x

Dst

f

: (

a

h

f

1

i

x

b

h

f

1

i

x

)

⇒ ∀

x

A

: (

x

h

f

i

a

x

h

f

i

b

)

⇒ h

f

i

a

⊆ h

f

i

b

(used the theorem 19 in [3]).

Theorem 15.

Let

f

is a pointfree funcoid from a distributive lattice Src

f

with least element to

a separable distributive lattice Dst

f

with least element. Then

h

f

i

(

i

Src

f

j

) =

h

f

i

i

Dst

f

h

f

i

j

for

every

i, j

Src

f

.

[TODO: In the book this theorem is strenghtened for starrish semilattices instead

of distributive lattices.]

Proof.

h

f

i

(

i

Src

f

j

) =

{

y

A

|

y

Dst

f

h

f

i

(

i

Src

f

j

)

0

Dst

f

}

=

{

y

A

|

(

i

Src

f

j

)

Src

f

h

f

1

i

y

0

Src

f

}

=

{

y

A

|

(

i

Src

f

h

f

1

i

y

)

Src

f

(

j

Src

f

h

f

1

i

y

)

0

Src

f

}

=

{

y

A

|

i

Src

f

h

f

1

i

y

0

Src

f

j

Src

f

h

f

1

i

y

0

Src

f

}

=

{

y

A

|

y

Dst

f

h

f

i

i

0

Dst

f

y

Dst

f

h

f

i

j

0

Dst

f

}

=

{

y

A

|

(

y

Dst

f

h

f

i

i

)

Dst

f

(

y

Dst

f

h

f

i

j

)

0

Dst

f

}

=

{

y

A

|

y

Dst

f

(

h

f

i

i

Dst

f

h

f

i

j

)

0

Dst

f

}

=

(

h

f

i

i

Dst

f

h

f

i

j

)

.

Thus

h

f

i

(

i

Src

f

j

) =

h

f

i

i

Src

f

h

f

i

j

by separability.

Proposition 16.

Let

f

is a pointfree funcoid. Then:

[TODO: This theorem is also strenghtened

in the book.]

1.

k

[

f

]

i

j

k

[

f

]

i

k

[

f

]

k

for every

i, j

Dst

f

,

k

Src

f

if Dst

f

is a distributive lattice

with least element.

2.

i

j

[

f

]

k

i

[

f

]

k

j

[

f

]

k

for every

i, j

Src

f

,

k

Dst

f

if Src

f

is a distributive lattice

with least element.

Proof.

1.

k

[

f

]

i

Dst

f

j

(

i

j

)

Dst

f

h

f

i

k

0

Dst

f

(

i

Dst

f

h

f

i

k

)

(

j

Dst

f

h

f

i

k

)

0

Dst

f

i

Dst

f

h

f

i

k

0

Dst

f

j

Dst

f

h

f

i

k

0

Dst

f

k

[

f

]

i

k

[

f

]

j

.

2. Similar.

3.2 Composition of pointfree funcoids

Definition 17.

Composition

of pointfree funcoids is defined by the formula

(

B

;

C

;

α

2

;

β

2

)

(

A

;

B

;

α

1

;

β

1

) = (

A

;

C

;

α

2

α

1

;

β

1

β

2

)

.

Definition 18.

I will call funcoids

f

and

g

composable

when Dst

f

=

Src

g

.

Proposition 19.

If

f

,

g

are pointfree funcoids and Dst

f

=

Src

g

then

g

f

is pointfree funcoid.

Proof.

Let

f

= (

A

;

B

;

α

1

;

β

1

)

,

g

= (

B

;

C

;

α

2

;

β

2

)

. For every

x, y

A

we have

y

C

(

α

2

α

1

)

x

y

C

α

2

α

1

x

α

1

x

B

β

2

y

x

A

β

1

β

2

y

x

A

(

β

1

β

2

)

y.

So

(

A

;

C

;

α

2

α

1

;

β

1

β

2

)

is a pointfree funcoid.

Obvious 20.

h

g

f

i

=

h

g

i ◦ h

f

i

for every composable pointfree funcoids

f

and

g

.

Pointfree funcoids

3