background image

19.13. MONOVALUED AND INJECTIVE POINTFREE FUNCOIDS

306

Obvious

1586

.

Co-completion is always co-complete.

Proposition

1587

.

For above defined always CoCompl

f

v

f

.

Proof.

By proposition

539

.

19.13. Monovalued and injective pointfree funcoids

Definition

1588

.

Let

A

and

B

be posets. Let

f

pFCD

(

A

,

B

).

The pointfree funcoid

f

is:

monovalued

when

f

f

1

v

1

pFCD

B

.

injective

when

f

1

f

v

1

pFCD

A

.

Monovaluedness is dual of injectivity.

Proposition

1589

.

Let

A

and

B

be posets. Let

f

pFCD

(

A

,

B

).

The pointfree funcoid

f

is:

monovalued iff

f

f

1

v

id

pFCD

(

B

)

im

f

, if

A

has greatest element and

B

is a

strongly separable meet-semilattice;

injective iff

f

1

f

v

id

pFCD

(

A

)

dom

f

, if

B

has greatest element and

A

is a

strongly separable meet-semilattice.

Proof.

It’s enough to prove

f

f

1

v

1

pFCD

B

f

f

1

v

id

pFCD

(

B

)

im

f

. im

f

is defined because

A

has greatest element. id

pFCD

(

B

)

im

f

is defined because

B

is a

meet-semilattice.

. Obvious.

. Let

f

f

1

v

1

pFCD

B

. Then

f

f

1

x

v

x

;

f

f

1

x

v

im

f

(proposi-

tion

1497

). Thus

f

f

1

x

v

x

u

im

f

=

D

id

pFCD

(

B

)

im

f

E

x

.

(

f

f

1

)

1

x

v

x

and

(

f

f

1

)

1

x

=

f

f

1

x

v

im

f

. Thus

(

f

f

1

)

1

x

v

x

u

im

f

=

D

id

pFCD

(

B

)

im

f

E

x

.

Thus

f

f

1

v

id

pFCD

(

B

)

im

f

.

Theorem

1590

.

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

pFCD

(

A

,

B

):

1

.

f

is monovalued.

2

.

a

atoms

A

:

h

f

i

a

atoms

B

∪{⊥

B

}

.

3

.

i, j

B

:

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

1496

)

for every two distinct

a, b

atoms

B

. This is equivalent to

¬

(

f

1

a

[

f

]