 14.1. ORDERING OF FILTERS

238

Proposition

1269

.

For a bijective

Set

-morphism

f

: Base(

A

)

Base(

B

) the

following are equivalent:

1

.

B

=

n

C

P

Base(

B

)

h

f

1

i

C

∈A

o

.

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

Hom

GreFunc

2

(

A

,

B

).

8

.

f

Hom

FuncBij

(

A

,

B

).

Proof.

1

2

.

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

∈ B ⇔

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

1270

.

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

Hom

GreFunc

2

(

A

,

B

).

8

. There is a bijective morphism

f

Hom

FuncBij

(

A

,

B

).

Proposition

1271

.

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

.