background image

15.13. MONOVALUED AND INJECTIVE POINTFREE FUNCOIDS

223

Proof.

For every ultrafilter

x

atoms

Src

f

D

l

G

f

E

x

=

D

l

G

E

h

f

i

x

=

l

h

g

ih

f

i

x

=

l

g

G

h

g

f

i

x

=

*

l

g

G

(

g

f

)

+

x.

Thus (

d

G

)

f

=

d

g

G

(

g

f

).

15.13. Monovalued and injective pointfree funcoids

Definition

1158

.

Let

A

and

B

be posets. Let

f

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

1159

.

Let

A

and

B

be posets. Let

f

FCD

(

A

;

B

).

The pointfree funcoid

f

is:

monovalued iff

f

f

1

v

id

FCD

(

B

)

im

f

, if im

f

is defined and

B

is a meet-

semilattice;

injective iff

f

1

f

v

id

FCD

(

A

)

dom

f

, if dom

f

is defined and

A

is a meet-

semilattice.

Proof.

It’s enough to prove

f

f

1

v

id

FCD

(

B

)

f

f

1

v

id

FCD

(

B

)

im

f

.

. Obvious.

. Let

f

f

1

v

id

FCD

(

B

)

. Then

f

f

1

x

v

x

;

f

f

1

x

v

im

f

. Thus

f

f

1

x

v

x

u

im

f

=

D

id

FCD

(

B

)

im

f

E

x

.

(

f

f

1

)

1

x

v

x

and

(

f

f

1

)

1

x

v

f

f

1

x

v

im

f

. Thus

(

f

f

1

)

1

x

v

x

u

im

f

=

D

id

FCD

(

B

)

im

f

E

x

.

Thus

f

f

1

v

id

FCD

(

B

)

im

f

.

Theorem

1160

.

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

FCD

(

A

;

B

):

1

.

f

is monovalued.

2

.

a

atoms

A

:

h

f

i

a

atoms

B

∪{⊥

B

}

.

3

.

i, j

A

:

f

1

(

i

u

j

) =

f

1

i

u

f

1

j

.

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

1069

because

A

is separable by proposition

181

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