 19.13. MONOVALUED AND INJECTIVE POINTFREE FUNCOIDS

307

Proof.

2

3

Let

a

atoms

A

,

h

f

i

a

=

b

. Then because

b

atoms

B

∪{⊥

B

}

(

i

u

j

)

u

b

6

=

B

i

u

b

6

=

B

j

u

b

6

=

B

;

a

[

f

]

i

u

j

a

[

f

]

i

a

[

f

]

j

;

i

u

j

f

1

a

i

f

1

a

j

f

1

a

;

a

u

A

f

1

(

i

u

j

)

6

=

A

a

u

f

1

i

6

=

A

a

u

f

1

j

6

=

A

;

a

u

A

f

1

(

i

u

j

)

6

=

A

a

u

f

1

i

u

f

1

j

6

=

A

;

f

1

(

i

u

j

) =

f

1

i

u

f

1

j.

3

1

.

f

1

a

u

f

1

b

=

f

1

(

a

u

b

) =

f

1

B

=

A

(by proposition

1499

)

for every two distinct

a, b

atoms

B

. This is equivalent to

¬

(

f

1

a

[

f

]

b

);

b

u h

f

i

f

1

a

=

B

;

b

u

f

f

1

a

=

B

;

¬

(

a

f

f

1

b

). So

a

f

f

1

b

a

=

b

for every

a, b

atoms

B

. This is possible only

(corollary

1547

and the fact that

B

is atomic) when

f

f

1

v

1

pFCD

B

.

¬

2

⇒ ¬

1

Suppose

h

f

i

a /

atoms

B

∪{⊥

B

}

for some

a

atoms

A

. Then there exist

two atoms

p

6

=

q

such that

h

f

i

a

w

p

∧ h

f

i

a

w

q

. Consequently

p

u h

f

i

a

6

=

B

;

a

u

f

1

p

6

=

A

;

a

v

f

1

p

;

f

f

1

p

=

h

f

i

f

1

p

w h

f

i

a

w

q

(by proposition

1500

because

B

is separable by proposition

234

and thus

strongly separable by theorem

225

);

f

f

1

p

6v

p

and

f

f

1

p

6

=

B

.

So it cannot be

f

f

1

v

1

pFCD

B

.

Theorem

1594

.

The following is equivalent for primary filtrators (

A

,

Z

0

) and

(

B

,

Z

1

) over boolean lattices and pointfree funcoids

f

:

A

B

:

1

.

f

is monovalued.

2

.

f

is metamonovalued.

3

.

f

is weakly metamonovalued.

Proof.

2

3

Obvious.

1

2

.

D

l

G

f

E

x

=

D

l

G

E

h

f

i

x

=

l

g

G

h

g

ih

f

i

x

=

l

g

G

h

g

f

i

x

=

*

l

g

G

(

g

f

)

+

x

for every atomic filter object

x

atoms

A

. Thus (

d

G

)

f

=

d

g

G

(

g

f

).

3

1

Take

g

=

a

×

FCD

y

and

h

=

b

×

FCD

y

for arbitrary atomic filter objects

a

6

=

b

and

y

. We have

g

u

h

=

; thus (

g

f

)

u

(

h

f

) = (

g

u

h

)

f

=

and

thus impossible

x

[

f

]

a

x

[

f

]

b

as otherwise

x

[

g

f

]

y

and

x

[

h

f

]

y

so

x

[(

g

f

)

u

(

h

f

)]

y

. Thus

f

is monovalued.

Theorem

1595

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. A pointfree funcoid

f

pFCD

(

A

,

B

) is monovalued iff

I, J

Z

1

:

f

1

(

I

u

Z

1

J

) =

f

1

I

u

f

1

J.

Proof.

A

and

B

are complete lattices (corollary

518

).

(

B

,

Z

1

) is a filtrator with separable core by theorem

537

.

(

B

,

Z

1

) is binarily meet-closed by corollary

536

.

A

and

B

are starrish by corollary

531

.

(

A

,

Z

0

) is with separable core by theorem

537

.