CHAPTER 5

Power of filters

1. Germs of functions

Definition

2036

.

Functions

f, g

Rel

(Ob

X

, B

)

are of the same

X

-germ

for

a filter object

X

iff there exists

X

up

X

such that

f

|

X

=

g

|

X

.

Proposition

2037

.

Being of the same germ is an equivalence relation.

Proof.

Reflexivity. Take arbitrary

X

up

X

.

Symmetry. Obvious.
Transitivity. Let

f

|

X

=

g

|

X

and

g

|

Y

=

h

|

Y

. Then

f

|

X

Y

=

h

|

X

Y

.

Definition

2038

.

A

germ

is an equivalence class of being the same germ.

Obvious

2039

.

Every germ is a filter on

Set

.

Theorem

2040

.

Let

A

,

B

be sets.

The following are mutually inverse bijections between monovalued reloids

f

:

A

B

with dom

f

=

X

and

X

-germs

S

of functions

A

B

for

X ∈

F

A

:

1

.

f

7→

up

Set

f

;

2

.

S

7→

s

|

X

if

s

S

.

The second bijection can also be written as

S

7→

d

RLD

S

|

X

or if card

B

6

= 1 as

S

7→

d

RLD

S

.

Remark

2041

.

s

|

X

is always defined because

S

is nonempty (it is an equiva-

lence class).

Proof.

First prove that up

Set

f

is an

X

-germ. Really,

F

up

Set

f

F

w

f

F

|

X

=

f

⇔ ∃

X

up

X

:

F

|

X

w

f

; thus

F, G

up

Set

f

⇒ ∃

X

up

X

:

F

|

X

w

f

∧ ∃

Y

up

X

:

G

|

Y

w

f

⇒ ∃

X

up

X

:

F

|

X

Y

w

f

∧ ∃

Y

up

X

:

G

|

X

Y

w

f

⇒ ∃

Z

up

X

: (

F

|

Z

w

f

G

|

Z

w

f

)

⇒ ∃

Z

up

X

: (

F

u

G

)

|

Z

w

f

and

F

up

Set

f

∧ ∃

X

up

X

:

F

|

X

=

G

|

X

F

w

f

F

|

X

=

G

|

X

G

|

X

w

f

G

up

Set

f

. We have proved that up

Set

f

is an equivalence class of the suitable

equivalence relation, that is up

Set

f

is an

X

-germ.

That

d

RLD

S

is a monovalued reloid is obvious. Also im

d

RLD

S

=

X

is obvious.

Now prove that our correspondences are mutually inverse.
Let

f

0

:

A

B

be a monovalued reloid and dom

f

=

X

. Let

S

= up

Set

f

0

and

f

1

=

s

|

X

for an

s

S

. We need to prove

f

1

=

f

0

. Really,

f

1

=

F

|

X

for an

F

up

Set

f

0

; thus

f

1

=

f

0

.

Let

S

0

be an

X

-germ of functions

A

B

. Let

f

=

s

|

X

for an

s

S

0

and

S

1

= up

Set

f

. We need to prove

S

1

=

S

0

. Really,

S

1

= up

Set

(

s

|

X

) =

F

Set

F

w

s

|

X

=

F

Set

X

up

X

:

F

|

X

w

s

|

X

=

F

Set

X

up

X

:

F

|

X

=

s

|

X

=

S

0

.

d

RLD

S

|

X

=

d

RLD

s

S

s

|

X

=

s

|

X

for every choice of

s

S

.

23