background image

15.8. MORE ON COMPOSITION OF POINTFREE FUNCOIDS

212

2

Let denote

x δ y

⇔ ∀

f

R

:

x

[

f

]

y

.

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

f

R, X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X, y

atoms

B

Y

:

x

[

f

]

y

f

R, X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

:

X

[

f

]

Y

f

R

:

a

[

f

]

b

a δ b.

So by the theorem

1114

,

δ

can be continued till [

p

] for some

p

FCD

(

A

;

B

).

For every

q

FCD

(

A

;

B

) such that

f

R

:

q

v

f

we have

x

[

q

]

y

⇒ ∀

f

R

:

x

[

f

]

y

x δ y

x

[

p

]

y

, so

q

v

p

. Consequently

p

=

d

R

.

From this

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

.

1

From the former

y

atoms

B

D

l

R

E

x

y

u

D

l

R

E

x

6

=

B

⇔ ∀

f

R

:

y

u h

f

i

x

6

=

B

y

\

atoms

B

h

f

i

x

f

R

y

atoms

l

h

f

i

x

f

R

for every

y

atoms

B

.

B

is atomically separable by the corollary

405

Thus

h

d

R

i

x

=

d

n

h

f

i

x

f

R

o

.

15.8. More on composition of pointfree funcoids

Proposition

1116

.

[

g

f

] = [

g

]

◦ h

f

i

=

g

1

1

[

f

] for every composable

pointfree funcoids

f

and

g

.

Proof.

For every

x

A

,

y

B

x

[

g

f

]

y

y

6 h

g

f

i

x

y

6 h

g

ih

f

i

x

⇔ h

f

i

x

[

g

]

y

x

([

g

]

◦ h

f

i

)

y.

Thus [

g

f

] = [

g

]

◦ h

f

i

.

[

g

f

] =

(

f

1

g

1

)

1

=

f

1

g

1

1

= (

f

1

g

1

)

1

=

g

1

1

[

f

]

.

Theorem

1117

.

Let

f

and

g

be pointfree funcoids and

A

= Dst

f

= Src

g

is

an atomic poset. Then for every

X ∈

Src

f

and

Z ∈

Dst

g

X

[

g

f

]

Z ⇔ ∃

y

atoms

A

: (

X

[

f

]

y

y

[

g

]

Z

)

.

Proof.

y

atoms

A

: (

X

[

f

]

y

y

[

g

]

Z

)

y

atoms

A

: (

Z 6 h

g

i

y

y

6 h

f

iX

)

y

atoms

A

: (

y

6

g

1

Z ∧

y

6 h

f

iX

)

g

1

Z 6 h

f

iX ⇔

X

[

g

f

]

Z

.

Theorem

1118

.

Let

A

,

B

,

C

be separable starrish join-semilattices and

B

is

atomic. Then:

1

.

f

(

g

t

h

) =

f

g

t

f

h

for

g, h

FCD

(

A

;

B

) and

f

FCD

(

B

;

C

).

2

. (

g

t

h

)

f

=

g

f

t

h

f

for

f

FCD

(

A

;

B

) and

g, h

FCD

(

B

;

C

).