 Proof.

1. im

(

g

f

) =

h

g

f

i

1

F

(

Src

f

)

=

h

g

ih

f

i

1

F

(

Src

f

)

=

h

g

i

im

f

=

h

g

i

(

im

f

u

dom

g

) =

h

g

i

dom

g

=

h

g

i

1

F

(

Src

g

)

=

im

g

.

2. dom

(

g

f

) =

im

(

f

¡

1

g

¡

1

)

what by proved above is equal to im

f

¡

1

that is dom

f

.

Lemma 6.63.

B 2

F

(

B

): 1

F

FCD

B

is an upper adjoint of

f

2

FCD

(

A

;

B

):

im

f

(for every sets

A

,

B

).

Proof.

We need to prove im

f

v B ,

f

v

1

F

FCD

B

what is obvious.

Corollary 6.64.

Image and domain of funcoids preserve joins.

Proof.

By properties of Galois connections and duality.

6.7 Categories of funcoids

I will dene two categories, the

category of funcoids

and the

category of funcoid triples

.

The

category of funcoids

is dened as follows:

Objects are small sets.

The set of morphisms from a set

A

to a set

B

is

FCD

(

A

;

B

)

.

The composition is the composition of funcoids.

Identity morphism for a set is the identity funcoid for that set.

To show it is really a category is trivial.

The

category of funcoid triples

is dened as follows:

Objects are lters on small sets.

The morphisms from a lter

A

to a lter

B

are triples

(

A

;

B

;

f

)

where

f

2

FCD

(

Base

(

A

);

Base

(

B

))

and dom

f

v A ^

im

f

v B

.

The composition is dened by the formula

(

B

;

C

;

g

)

(

A

;

B

;

f

) = (

A

;

C

;

g

f

)

.

Identity morphism for a lter

A

is id

A

FCD

.

To prove that it is really a category is trivial.

6.8 Specifying funcoids by functions or relations on atomic

lters

Theorem 6.65.

For every funcoid

f

and

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

1.

h

f

iX

=

F

hh

f

ii

atoms

X

;

2.

X

[

f

]

Y , 9

x

2

atoms

X

; y

2

atoms

Y

:

x

[

f

]

y

.

Proof.

1.

Y u h

f

iX

=

/ 0

F

(

Dst

f

)

, X u h

f

¡

1

iY

=

/ 0

F

(

Src

f

)

, 9

x

2

atoms

X

:

x

u h

f

¡

1

iY

=

/ 0

F

(

Src

f

)

, 9

x

2

atoms

X

:

Y u h

f

i

x

=

/ 0

F

(

Dst

f

)

:

@

h

f

iX

=

F

h

@

ihh

f

ii

atoms

X

=

@

F

hh

f

ii

atoms

X

. So

h

f

iX

=

F

hh

f

ii

atoms

X

by proposition

4.202

.

2. If

X

[

f

]

Y

, then

Y u h

f

iX

=

/ 0

F

(

Dst

f

)

, consequently there exists

y

2

atoms

Y

such that

y

u h

f

iX

=

/ 0

F

(

Dst

f

)

,

X

[

f

]

y

. Repeating this second time we get that there exists

x

2

atoms

X

such

that

x

[

f

]

y

. From this it follows

9

x

2

atoms

X

; y

2

atoms

Y

:

x

[

f

]

y:

104

Funcoids