background image

2. Let denote

x  y

, 8

f

2

R

:

x

[

f

]

y

.

8

X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

9

x

2

atoms

A

X ; y

2

atoms

B

Y

:

x  y

)

8

f

2

R; X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

9

x

2

atoms

A

X ; y

2

atoms

B

Y

:

x

[

f

]

y

)

8

f

2

R; X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

:

X

[

f

]

Y

)

8

f

2

R

:

a

[

f

]

b

,

a  b:

So, by the theorem

15.58

,

can be continued till

[

p

]

for some

p

2

FCD

(

A

;

B

)

.

For every

q

2

FCD

(

A

;

B

)

such that

8

f

2

R

:

q

v

f

we have

x

[

q

]

y

) 8

f

2

R

:

x

[

f

]

y

,

x  y

,

x

[

p

]

y

,

so

q

v

p

. Consequently

p

=

d

R

.

From this

x

[

d

R

]

y

, 8

f

2

R

:

x

[

f

]

y

.

1. From the former

y

2

atoms

B

h

d

R

i

x

,

y

u h

d

R

i

x

=

/ 0

B

, 8

f

2

R

:

y

u h

f

i

x

=

/ 0

B

,

y

2

T

h

atoms

B

ifh

f

i

x

j

f

2

R

g ,

y

2

atoms

d

fh

f

i

x

j

f

2

R

g

for every

y

2

atoms

B

.

B

is atomically separable by the corollary

4.138

Thus

l

R

x

=

l

fh

f

i

x

j

f

2

R

g

:

15.8 More on composition of pointfree funcoids

Proposition 15.60.

[

g

f

]=[

g

]

h

f

i

=

h

g

¡

1

i

¡

1

[

f

]

for every composable pointfree funcoids

f

and

g

.

Proof.

x

[

g

f

]

y

,

y

/

h

g

f

i

x

,

y

/

h

g

ih

f

i

x

, h

f

i

x

[

g

]

y

,

x

([

g

]

h

f

i

)

y

for every

x

2

A

,

y

2

B

.

Thus

[

g

f

]=[

g

]

h

f

i

.

[

g

f

]=[(

f

¡

1

g

¡

1

)

¡

1

]=[

f

¡

1

g

¡

1

]

¡

1

=([

f

¡

1

]

h

g

¡

1

i

)

¡

1

=

h

g

¡

1

i

¡

1

[

f

]

.

Theorem 15.61.

Let

f

and

g

be pointfree funcoids and

A

=

Dst

f

=

Src

g

is an atomic poset.

Then for every

X 2

Src

f

and

Z 2

Dst

g

X

[

g

f

]

Z , 9

y

2

atoms

A

: (

X

[

f

]

y

^

y

[

g

]

Z

)

:

Proof.

9

y

2

atoms

A

: (

X

[

f

]

y

^

y

[

g

]

Z

)

, 9

y

2

atoms

A

: (

/

h

g

i

y

^

y

/

h

f

iX

)

, 9

y

2

atoms

A

: (

y

/

h

g

¡

1

iZ ^

y

/

h

f

iX

)

, h

g

¡

1

iZ 

/

h

f

iX

, X

[

g

f

]

Z

:

Theorem 15.62.

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

2

FCD

(

A

;

B

)

and

f

2

FCD

(

B

;

C

)

.

2.

(

g

t

h

)

f

=

g

f

t

h

f

for

f

2

FCD

(

A

;

B

)

and

g; h

2

FCD

(

B

;

C

)

.

Proof.

I will prove only the rst equality because the other is analogous.

We can apply theorem

15.35

.

For every

X 2

A

,

Y 2

C

X

[

f

(

g

t

h

)]

Z , 9

y

2

atoms

B

: (

X

[

g

t

h

]

y

^

y

[

f

]

Z

)

, 9

y

2

atoms

B

: ((

X

[

g

]

y

_ X

[

h

]

y

)

^

y

[

f

]

Z

)

, 9

y

2

atoms

B

: ((

X

[

g

]

y

^

y

[

f

]

Z

)

_

(

X

[

h

]

y

^

y

[

f

]

Z

))

, 9

y

2

atoms

B

: (

X

[

g

]

y

^

y

[

f

]

Z

)

_ 9

y

2

atoms

B

: (

X

[

h

]

y

^

y

[

f

]

Z

)

, X

[

f

g

]

Z _ X

[

f

h

]

Z

, X

[

f

g

t

f

h

]

Z

:

15.8 More on composition of pointfree funcoids

187