 6.8. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS 111

To show it is really a category is trivial.

The

category of funcoid triples

is defined as follows:

Objects are filters on small sets.

The morphisms from a filter

A

to a filter

B

are triples (

A

;

B

;

f

) where

f

FCD

(Base(

A

); Base(

B

)) and dom

f

v A ∧

im

f

v B

.

The composition is defined by the formula (

B

;

C

;

g

)

(

A

;

B

;

f

) = (

A

;

C

;

g

f

).

Identity morphism for a filter

A

is id

FCD

A

.

To prove that it is really a category is trivial.

6.8. Specifying funcoids by functions or relations on atomic filters

Theorem

632

.

For every funcoid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

)

1

.

h

f

iX

=

F

hh

f

ii

atoms

X

;

2

.

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y

.

Proof.

1

.

Y u h

f

iX 6

=

F

(Dst

f

)

X u

f

1

Y 6

=

F

(Src

f

)

x

atoms

X

:

x

u

f

1

Y 6

=

F

(Src

f

)

x

atoms

X

:

Y u h

f

i

x

6

=

F

(Dst

f

)

.

h

f

iX

=

F

h

i

hh

f

ii

atoms

X

=

F

hh

f

ii

atoms

X

.

So

h

f

iX

=

F

hh

f

ii

atoms

X

by proposition

469

.

2

If

X

[

f

]

Y

, then

Y u h

f

iX 6

=

F

(Dst

f

)

, consequently there exists

y

atoms

Y

such that

y

u h

f

iX 6

=

F

(Dst

f

)

,

X

[

f

]

y

. Repeating this second time we

get that there exists

x

atoms

X

such that

x

[

f

]

y

. From this it follows

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y.

The reverse is obvious.

Corollary

633

.

Let

f

be a funcoid.

The value of

f

can be restored knowing

h

f

i|

atoms

F

(Src

f

)

.

The value of

f

can be restored knowing [

f

]

|

atoms

F

(Src

f

)

×

atoms

F

(Dst

f

)

.

Theorem

634

.

Let

A

and

B

be sets.

1

. A function

α

F

(

B

)

atoms

F

(

A

)

such that (for every

a

atoms

F

(

A

)

)

αa

v

l

DG

◦h

α

i

atoms

◦ ↑

A

E

a

(8)

can be continued to the function

h

f

i

for a unique

f

FCD

(

A

;

B

);

h

f

iX

=

G

h

α

i

atoms

X

(9)

for every

X ∈

F

(

A

).

2

. A relation

δ

P

(atoms

F

(

A

)

×

atoms

F

(

B

)

) such that (for every

a

atoms

F

(

A

)

,

b

atoms

F

(

B

)

)

X

a, Y

b

x

atoms

A

X, y

atoms

A

X

:

x δ y

a δ b

(10)

can be continued to the relation [

f

] for a unique

f

FCD

(

A

;

B

);

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

X

:

x δ y

(11)

for every

X ∈

F

(

A

),

Y ∈

F

(

B

).