 13.2. ORDERING OF FILTERS

179

1

2

.

B

=

f

∗ A ⇔ B

=

C

P

Base(

B

)

h

f

1

i

C

∈ A

C

P

Base(

B

) : (

C

∈ B ⇔

f

1

C

∈ A

)

.

2

3

Because

f

is a bijection.

2

5

For every

C

∈ B

we have

f

1

C

∈ A

and thus

FCD

f

|

A

FCD

f

1

C

=

h

f

i

f

1

C

=

C

. Thus

FCD

f

|

A

is onto

B

.

4

5

Obvious.

5

4

We need to prove only that

FCD

f

|

A

is an injection. But this follows

from the fact that

f

is a bijection.

4

3

We have

C

Base(

A

) : ((

FCD

f

|

A

)

C

C

∈ A

) and consequently

C

Base(

A

) : (

h

f

i

C

∈ B ⇔

C

∈ A

).

6

1

From the last corollary.

1

7

Obvious.

7

8

Obvious.

Corollary

962

.

The following are equivalent for every filters

A

and

B

:

1

.

A

is directly isomorphic to

B

.

2

. There is a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) such that for

every

C

P

Base(

B

)

C

∈ B ⇔

f

1

C

∈ A

.

3

. There is a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) such that for

every

C

P

Base(

B

)

h

f

i

C

∈ B ⇔

C

∈ A

.

4

. There is a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) such that

FCD

f

|

A

is a bijection from

A

to

B

.

5

. There is a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) such that

FCD

f

|

A

is a function onto

B

.

6

. There is a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) such that

B

=

FCD

f

A

.

7

. There is a bijective morphism

f

Mor

GreFunc

2

(

A

;

B

).

Proposition

963

.

GreFunc

1

and

GreFunc

2

with function composition are

categories.

Proof.

Let

f

:

A → B

and

g

:

B → C

be morphisms of

GreFunc

1

. Then

B v

FCD

f

A

and

C v

FCD

g

B

. So

FCD

(

g

f

)

A

=

FCD

g

FCD

f

A w

FCD

g

B w C

.

Thus

g

f

is a morphism of

GreFunc

1

. Associativity law is evident. id

Base(

A

)

is

the identity morphism of

GreFunc

1

for every filter

A

.

Let

f

:

A → B

and

g

:

B → C

be morphisms of

GreFunc

2

. Then

B

=

FCD

f

A

and

C

=

FCD

g

B

. So

FCD

(

g

f

)

A

=

FCD

g

FCD

f

A

=

FCD

g

B

=

C

.

Thus

g

f

is a morphism of

GreFunc

2

. Associativity law is evident. id

Base(

A

)

is

the identity morphism of

GreFunc

2

for every filter

A

.

Corollary

964

.

1

and

2

are preorders.

Theorem

965

.

FuncBij

is a groupoid.