 14.1. ORDERING OF FILTERS

237

of these directed multigraphs with added composition of morphisms (of directed

multigraphs edges). As such I will call vertices of these multigraphs objects and

edges morphisms.

Definition

1258

.

I will denote

GreFunc

1

the multigraph whose objects are

filters and whose morphisms between objects

A

and

B

are

Set

-morphisms from

Base(

A

) to Base(

B

) such that

B v

FCD

f

A

.

Definition

1259

.

I will denote

GreFunc

2

the multigraph whose objects are

filters and whose morphisms between objects

A

and

B

are

Set

-morphisms from

Base(

A

) to Base(

B

) such that

B

=

FCD

f

A

.

Definition

1260

.

Let

A

be a filter on a set

X

and

B

be a filter on a set

Y

.

A ≥

1

B

iff Hom

GreFunc

1

(

A

,

B

) is not empty.

Definition

1261

.

Let

A

be a filter on a set

X

and

B

be a filter on a set

Y

.

A ≥

2

B

iff Hom

GreFunc

2

(

A

,

B

) is not empty.

Proposition

1262

.

1

.

f

Hom

GreFunc

1

(

A

,

B

) iff

f

is a

Set

-morphism from Base(

A

) to Base(

B

)

such that

C

∈ B ⇐

f

1

C

∈ A

for every

C

P

Base(

B

).

2

.

f

Hom

GreFunc

2

(

A

,

B

) iff

f

is a

Set

-morphism from Base(

A

) to Base(

B

)

such that

C

∈ B ⇔

f

1

C

∈ A

for every

C

P

Base(

B

).

Proof.

1

.

f

Hom

GreFunc

1

(

A

,

B

)

⇔ B v

FCD

f

A ⇔

C

FCD

f

A

:

C

∈ B ⇔ ∀

C

P

Base(

B

) : (

f

1

C

∈ A ⇒

C

∈ B

)

.

2

.

f

Hom

GreFunc

2

(

A

,

B

)

⇔ B

=

FCD

f

A ⇔ ∀

C

: (

C

∈ B ⇔

C

FCD

f

A

)

C

P

Base(

B

) : (

C

∈ B ⇔

C

FCD

f

A

)

C

P

Base(

B

) : (

f

1

C

∈ A ⇔

C

∈ B

)

.

Definition

1263

.

The directed multigraph

FuncBij

is the directed multigraph

got from

GreFunc

2

by restricting to only bijective morphisms.

Definition

1264

.

A filter

A

is

directly isomorphic

to a filter

B

iff there is a

morphism

f

Hom

FuncBij

(

A

,

B

).

Obvious

1265

.

f

Hom

GreFunc

1

(

A

,

B

)

⇔ B v

FCD

f

A

for every

Set

-

morphism from Base(

A

) to Base(

B

).

Obvious

1266

.

f

Hom

GreFunc

2

(

A

,

B

)

⇔ B

=

FCD

f

A

for every

Set

-

morphism from Base(

A

) to Base(

B

).

Corollary

1267

.

A ≥

1

B

iff it exists a

Set

-morphism

f

: Base(

A

)

Base(

B

)

such that

B v

FCD

f

A

.

Corollary

1268

.

A ≥

2

B

iff it exists a

Set

-morphism

f

: Base(

A

)

Base(

B

)

such that

B

=

FCD

f

A

.