background image

7.12. COMPLETE FUNCOIDS

173

Proof.

First, it’s easy to see that

A

{

α

} ×

FCD

b

are elements of

ComplFCD

(

A, B

). Also

FCD

(

A,B

)

is an element of

ComplFCD

(

A, B

).

A

{

α

} ×

FCD

b

are atoms of

ComplFCD

(

A, B

) because they are atoms of

FCD

(

A, B

).

It remains to prove that if

f

is an atom of

ComplFCD

(

A, B

) then

f

=

A

{

α

} ×

FCD

b

for some

α

A

and an ultrafilter

b

on

B

.

Suppose

f

FCD

(

A, B

) is a non-empty complete funcoid. Then there exists

α

A

such that

h

f

i

@

{

α

} 6

=

F

(

B

)

. Thus

A

{

α

}

×

FCD

b

v

f

for some ultrafilter

b

on

B

. If

f

is an atom then

f

=

A

{

α

}

×

FCD

b

.

Theorem

928

.

G

7→

d

α

A

(

A

{

α

} ×

FCD

G

(

α

)) is an order isomorphism from

the set of functions

G

F

(

B

)

A

to the set

ComplFCD

(

A, B

).

The inverse isomorphism is described by the formula

G

(

α

) =

h

f

i

@

{

α

}

where

f

is a complete funcoid.

Proof.

d

α

A

(

A

{

α

} ×

FCD

G

(

α

)) is complete because

G

(

α

) =

d

atoms

G

(

α

)

and thus

l

α

A

(

A

{

α

} ×

FCD

G

(

α

)) =

l

A

{

α

} ×

FCD

b

α

A, b

atoms

G

(

α

)

is complete. So

G

7→

d

α

A

(

A

{

α

} ×

FCD

G

(

α

)) is a function from

G

F

(

B

)

A

to

ComplFCD

(

A, B

).

Let

f

be complete. Then take

G

(

α

) =

l

(

b

atoms

F

(Dst

f

)

A

{

α

} ×

FCD

b

v

f

)

and we have

f

=

d

α

A

(

A

{

α

} ×

FCD

G

(

α

)) obviously. So

G

7→

d

α

A

(

A

{

α

} ×

FCD

G

(

α

)) is surjection onto

ComplFCD

(

A, B

).

Let now prove that it is an injection:

Let

f

=

l

α

A

(

A

{

α

} ×

FCD

F

(

α

)) =

l

α

A

(

A

{

α

} ×

FCD

G

(

α

))

for some

F, G

F

(Dst

f

)

Src

f

. We need to prove

F

=

G

. Let

β

Src

f

.

h

f

i

@

{

β

}

=

l

α

A

A

{

α

} ×

FCD

F

(

α

)

@

{

β

}

=

F

(

β

)

.

Similarly

h

f

i

@

{

β

}

=

G

(

β

). So

F

(

β

) =

G

(

β

).

We have proved that it is a bijection. To show that it is monotone is trivial.

Denote

f

=

d

α

A

(

A

{

α

} ×

FCD

G

(

α

)). Then

h

f

i

@

{

α

0

}

= (because

A

{

α

0

}

is principal) =

l

α

A

A

{

α

} ×

FCD

G

(

α

)

@

{

α

0

}

=

A

{

α

0

} ×

FCD

G

(

α

0

)

@

{

α

0

}

=

G

(

α

0

)

.

Corollary

929

.

G

7→

d

α

A

(

G

(

α

)

×

FCD

A

{

α

}

) is an order isomorphism from

the set of functions

G

F

(

B

)

A

to the set

CoComplFCD

(

A, B

).

The inverse isomorphism is described by the formula

G

(

α

) =

f

1

@

{

α

}

where

f

is a co-complete funcoid.

Corollary

930

.

ComplFCD

(

A, B

) and

CoComplFCD

(

A, B

) are co-frames.