background image

Proposition 15.101.

Monovalued pointfree funcoids between sets of lters on boolean lattices

are metamonovalued.

[FIXME: Monovalued is dened below.]

Proof.

h

(

d

G

)

f

i

x

=

h

d

G

ih

f

i

x

=

d

g

2

G

h

g

ih

f

i

x

=

d

g

2

G

h

g

f

i

x

=

d

g

2

G

(

g

f

)

x

for every

ultralter

x

2

atoms

Src

f

. Thus

(

d

G

)

f

=

d

g

2

G

(

g

f

)

.

15.13 Monovalued and injective pointfree funcoids

Denition 15.102.

Let

A

and

B

be posets. Let

f

2

FCD

(

A

;

B

)

.

The pointfree funcoid

f

is:

monovalued

when

f

f

¡

1

v

id

FCD

(

B

)

.

injective

when

f

¡

1

f

v

id

FCD

(

A

)

.

Monovaluedness is dual of injectivity.

Proposition 15.103.

Let

A

and

B

be posets. Let

f

2

FCD

(

A

;

B

)

.

The pointfree funcoid

f

is:

monovalued i

f

f

¡

1

v

id

im

f

FCD

(

B

)

, if im

f

is dened and

B

is a meet-semilattice;

injective i

f

¡

1

f

v

id

dom

f

FCD

(

A

)

, if dom

f

is dened and

A

is a meet-semilattice.

Proof.

It's enough to prove

f

f

¡

1

v

id

FCD

(

B

)

,

f

f

¡

1

v

id

im

f

FCD

(

B

)

.

(

.

Obvious.

)

.

Let

f

f

¡

1

v

id

FCD

(

B

)

. Then

h

f

f

¡

1

i

x

v

x

; and

h

f

f

¡

1

i

x

v

im

f

. Thus

h

f

f

¡

1

i

x

v

x

u

im

f

=

D

id

im

f

FCD

(

B

)

E

x

.

h

(

f

f

¡

1

)

¡

1

i

x

v

x

and

h

(

f

f

¡

1

)

¡

1

i

x

=

h

f

f

¡

1

i

x

v

im

f

. Thus

h

(

f

f

¡

1

)

¡

1

i

x

v

x

u

im

f

=

D

id

im

f

FCD

(

B

)

E

x

.

Thus

f

f

¡

1

v

id

im

f

FCD

(

B

)

.

Theorem 15.104.

Let

A

be an atomistic meet-semilattice with least element,

B

be an atomistic

bounded meet-semilattice. The following statements are equivalent for every

f

2

FCD

(

A

;

B

)

:

1.

f

is monovalued.

2.

8

a

2

atoms

A

:

h

f

i

a

2

atoms

B

[ f

0

B

g

.

3.

8

i; j

2

A

:

h

f

¡

1

i

(

i

u

j

) =

h

f

¡

1

i

i

u h

f

¡

1

i

j

.

Proof.

(

2

)

)

(

3

).

Let

a

2

atoms

A

,

h

f

i

a

=

b

. Then because

b

2

atoms

B

[ f

0

B

g

(

i

u

j

)

u

b

=

/ 0

B

,

i

u

b

=

/ 0

B

^

j

u

b

=

/ 0

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

h

f

¡

1

i

(

i

u

j

) =

/ 0

A

,

a

u h

f

¡

1

i

i

=

/ 0

A

^

a

u h

f

¡

1

i

j

=

/ 0

A

;

a

u h

f

¡

1

i

(

i

u

j

) =

/ 0

A

,

a

u h

f

¡

1

i

i

u h

f

¡

1

i

j

=

/ 0

A

;

h

f

¡

1

i

(

i

u

j

) =

h

f

¡

1

i

i

u h

f

¡

1

i

j:

(

3

)

)

(

1

).

h

f

¡

1

i

a

u h

f

¡

1

i

b

=

h

f

¡

1

i

(

a

u

b

) =

h

f

¡

1

i

0

B

= 0

A

(by proposition

15.13

because

A

is separable by proposition

3.22

for every two distinct

a; b

2

atoms

B

. This is equivalent

to

:

(

h

f

¡

1

i

a

[

f

]

b

)

;

b

u h

f

ih

f

¡

1

i

a

= 0

B

;

b

u h

f

f

¡

1

i

a

= 0

B

;

:

(

a

[

f

f

¡

1

]

b

)

. So

a

[

f

f

¡

1

]

b

)

a

=

b

for every

a; b

2

atoms

B

. This is possible only (corollary

15.56

and the

fact that

B

is atomic) when

f

f

¡

1

v

id

FCD

(

B

)

.

15.13 Monovalued and injective pointfree funcoids

195