background image

19.11. COMPLETE POINTFREE FUNCOIDS

303

Proposition

1577

.

Let

A

,

B

,

C

be atomic bounded separable meet-

semilattices, and

f

pFCD

(

A

,

B

),

g

pFCD

(

B

,

C

). Then

atoms(

g

f

) =

x

×

FCD

z

x

atoms

A

, z

atoms

C

,

y

atoms

B

: (

x

×

FCD

y

atoms

f

y

×

FCD

z

atoms

g

)

.

Proof.

(

x

×

FCD

z

)

u

(

g

f

)

6

=

pFCD

(

A

,

C

)

x

[

g

f

]

z

y

atoms

B

: (

x

[

f

]

y

y

[

g

]

z

)

y

atoms

B

: ((

x

×

FCD

y

)

u

f

6

=

pFCD

(

A

,

B

)

(

y

×

FCD

z

)

u

g

6

=

pFCD

(

B

,

C

)

)

(were used corollary

1561

and theorem

1552

).

Theorem

1578

.

Let

f

be a pointfree funcoid between atomic bounded sepa-

rable meet-semilattices

A

and

B

.

1

.

X

[

f

]

Y ⇔ ∃

F

atoms

f

:

X

[

F

]

Y

for every

X ∈

A

,

Y ∈

B

;

2

.

h

f

iX

=

d

F

atoms

f

h

F

iX

for every

X ∈

A

provided that

B

is a complete

lattice.

Proof.

1

.

F

atoms

f

:

X

[

F

]

Y ⇔

a

atoms

A

, b

atoms

B

: (

a

×

FCD

b

6

f

∧ X

a

×

FCD

b

Y

)

a

atoms

A

, b

atoms

B

: (

a

×

FCD

b

6

f

a

×

FCD

b

6 X ×

FCD

Y

)

F

atoms

f

: (

F

6

f

F

6 X ×

FCD

Y

)

(by theorem

1573

)

f

6 X ×

FCD

Y ⇔

X

[

f

]

Y

.

2

Let

Y ∈

B

. Suppose

Y 6 h

f

iX

. Then

X

[

f

]

Y

;

F

atoms

f

:

X

[

F

]

Y

;

F

atoms

f

:

Y 6 h

F

iX

; and (taking into account that

B

is strongly separable

by theorem

225

)

Y 6

d

F

atoms

f

h

F

iX

. So

h

f

iX v

d

F

atoms

f

h

F

iX

by strong

separability. The contrary

h

f

iX w

d

F

atoms

f

h

F

iX

is obvious.

19.11. Complete pointfree funcoids

Definition

1579

.

Let

A

and

B

be posets. A pointfree funcoid

f

pFCD

(

A

,

B

)

is

complete

, when for every

S

P

A

whenever both

d

S

and

d

hh

f

ii

S

are defined

we have

h

f

i

l

S

=

l

hh

f

ii

S.

Definition

1580

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be filtrators. I will call a

co-complete

pointfree funcoid

a pointfree funcoid

f

pFCD

(

A

,

B

) such that

h

f

i

X

Z

1

for every

X

Z

0

.