 8.5. CATEGORIES OF RELOIDS

190

Proof.

First,

im(

f

|

↑{

α

}

) =

RLD

l

h

im

i

up(

f

|

↑{

α

}

) =

RLD

l

h

im

i

up(

f

u

(

Src

f

{

α

} × >

F

(Dst

f

)

)) =

RLD

l

im(

F

(

{

α

} × >

T

(Dst

f

)

))

F

up

f

=

RLD

l

im(

F

|

↑{

α

}

)

F

up

f

.

Taking this into account we have:

Src

f

{

α

} ×

RLD

im(

f

|

↑{

α

}

) =

RLD

l

Src

f

{

α

} ×

K

K

im(

f

|

↑{

α

}

)

=

RLD

l

(

Src

f

{

α

} ×

im(

F

|

↑{

α

}

)

F

up

f

)

=

RLD

l

F

|

↑{

α

}

F

up

f

=

RLD

l

F

u

(

Src

f

{

α

} × >

T

(Dst

f

)

)

F

up

f

=

RLD

l

F

F

up

f

u ↑

RLD

(

Src

f

{

α

} × >

T

(Dst

f

)

) =

f

u ↑

RLD

(

Src

f

{

α

} × >

T

(Dst

f

)

) =

f

|

↑{

α

}

.

Lemma

1029

.

λ

B ∈

F

(

B

) :

>

F

×

RLD

B

is an upper adjoint of

λf

RLD

(

A, B

) :

im

f

(for every sets

A

,

B

).

Proof.

We need to prove im

f

v B ⇔

f

v >

F

×

RLD

B

what is obvious.

Corollary

1030

.

Image and domain of reloids preserve joins.

Proof.

By properties of Galois connections and duality.

8.5. Categories of reloids

I will define two categories, the

category of reloids

and the

category of reloid

triples

.

The

category of reloids

is defined as follows:

Objects are small sets.

The set of morphisms from a set

A

to a set

B

is

RLD

(

A, B

).

The composition is the composition of reloids.

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

To show it is really a category is trivial.

The

category of reloid triples

is defined as follows:

Objects are small sets.