background image

13.2. ORDERING OF FILTERS

178

2

.

f

Mor

GreFunc

2

(

A

;

B

)

⇔ B

=

f

∗ A ⇔ ∀

C

: (

C

∈ B ⇔

C

f

∗ A

)

C

P

Base(

B

) : (

C

∈ B ⇔

C

f

∗ A

)

C

P

Base(

B

) : (

f

1

C

∈ A ⇔

C

∈ B

)

.

Definition

954

.

The directed multigraph

FuncBij

is the directed multigraph

got from

GreFunc

2

by restricting to only bijective morphisms.

Definition

955

.

A filter

A

is

directly isomorphic

to a filter

B

iff there is a

morphism

f

Mor

FuncBij

(

A

;

B

).

Proposition

956

.

f

∗ A

=

FCD

A

for every

Set

-morphism

f

: Base(

A

)

Base(

B

).

FiXme

: Make it the primary definition instead of the trick with

.

Proof.

For every set

C

P

Base(

B

) we have

C

f

∗ A ⇔

f

1

C

∈ A ⇒

K

∈ A

:

f

1

C

=

K

K

∈ A

:

h

f

i

f

1

C

=

h

f

i

K

K

∈ A

:

C

⊇ h

f

i

K

K

∈ A

:

C

FCD

f

K

C

FCD

f

A

.

So

C

f

∗ A ⇒

C

FCD

f

A

.

Let now

C

FCD

f

A

. Then

Base(

A

)

f

1

C

w

FCD

f

1

FCD

f

A w A

and thus

f

1

C

∈ A

.

Corollary

957

.

f

Mor

GreFunc

1

(

A

;

B

)

⇔ B v

FCD

f

A

for every

Set

-

morphism from Base(

A

) to Base(

B

).

Corollary

958

.

f

Mor

GreFunc

2

(

A

;

B

)

⇔ B

=

FCD

f

A

for every

Set

-

morphism from Base(

A

) to Base(

B

).

Corollary

959

.

A ≥

1

B

iff it exists a

Set

-morphism

f

: Base(

A

)

Base(

B

)

such that

B v

FCD

f

A

.

Corollary

960

.

A ≥

2

B

iff it exists a

Set

-morphism

f

: Base(

A

)

Base(

B

)

such that

B

=

FCD

f

A

.

Proposition

961

.

For a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) the

following are equivalent:

1

.

B

=

f

∗ A

.

2

.

C

Base(

B

) : (

C

∈ B ⇔

f

1

C

∈ A

).

3

.

C

Base(

A

) : (

C

∈ h

f

i

B ⇔

C

∈ A

).

4

.

FCD

f

|

A

is a bijection from

A

to

B

.

5

.

FCD

f

|

A

is a function onto

B

.

6

.

B

=

FCD

f

A

.

7

.

f

Mor

GreFunc

2

(

A

;

B

).

8

.

f

Mor

FuncBij

(

A

;

B

).

Proof.