 13.2. ORDERING OF FILTERS

183

2

1

By corollary

1015

below, there exists a

Set

-morphism

F

: Base(

A

)

Base(

B

) such that

f

= (

RLD

f

)

|

A

. Thus

FCD

F

A

= im(

FCD

F

)

|

A

= im(

FCD

)(

RLD

F

)

|

A

= im(

FCD

)

f

= im

f

=

B

.

Thus

A ≥

2

B

is testified by the morphism

F

.

2

3

By duality.

Theorem

980

.

The following are categories (with reloid composition):

1

.

MonRld

v

,

w

;

2

.

MonRld

v

,

=

;

3

.

MonRld

=

,

=

;

4

.

CoMonRld

v

,

w

;

5

.

CoMonRld

v

,

=

;

6

.

CoMonRld

=

,

=

.

Proof.

We will prove only the first three. The rest follow from duality.

FiXme

:

Check duality.

We need to prove only that composition of morphisms is a morphism,

because associativity and existence of identity morphism are evident. We have:

1

Let

f

Mor

MonRld

v

,

w

(

A

;

B

),

g

Mor

MonRld

v

,

w

(

B

;

C

). Then dom

f

v A

,

im

f

w B

, dom

g

v B

, im

g

w C

. So dom(

g

f

)

v A

, im(

g

f

)

w C

that is

g

f

Mor

MonRld

v

,

w

(

A

;

C

).

2

Let

f

Mor

MonRld

v

,

=

(

A

;

B

),

g

Mor

MonRld

v

,

=

(

B

;

C

). Then dom

f

v A

,

im

f

=

B

, dom

g

v B

, im

g

=

C

. So dom(

g

f

)

v A

, im(

g

f

) =

C

that is

g

f

Mor

MonRld

v

,

=

(

A

;

C

).

3

Let

f

Mor

MonRld

=

,

=

(

A

;

B

),

g

Mor

MonRld

=

,

=

(

B

;

C

). Then dom

f

=

A

,

im

f

=

B

, dom

g

=

B

, im

g

=

C

. So dom(

g

f

) =

A

, im(

g

f

) =

C

that is

g

f

Mor

MonRld

=

,

=

(

A

;

C

).

Definition

981

.

Let

BijRld

be the groupoid of all bijections of the category

of reloid triples. Its objects are filters and its morphisms from a filter

A

to filter

B

are monovalued injective reloids

f

such that dom

f

=

A

and im

f

=

B

.

Theorem

982

.

Filters

A

and

B

are isomorphic iff Mor

BijRld

(

A

;

B

)

6

=

.

Proof.

. Let

A

and

B

be isomorphic. Then there are sets

A

∈ A

,

B

∈ B

and a bijective

Set

-morphism

F

:

A

B

such that

h

F

i

:

P

A

∩ A →

P

B

∩ B

is a

bijection.