background image

To show it is really a category is trivial.

The

category of funcoid triples

is defined as follows:

Objects are filter objects on small sets.

The morphisms from a f.o.

A

to a f.o.

B

are triples (

f

;

A

;

B

) where

f

FCD

(Base (

A

) ; Base (

B

)) and dom

f

⊆ A ∧

im

f

⊆ B

.

The composition is defined by the formula (

g

;

B

;

C

)

(

f

;

A

;

B

) = (

g

f

;

A

;

C

).

Identity morphism for an f.o.

A

is

I

FCD

A

.

To prove that it is really a category is trivial.

3.8

Specifying funcoids by functions or relations on atomic
filter objects

Theorem 15

For every funcoid

f

and

X ∈

F

(Src

f

)

,

Y ∈

F

(Dst

f

)

1.

h

f

i X

=

S

hh

f

ii

atoms

X

;

2.

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y

.

Proof

1.

Y ∩ h

f

i X 6

= 0

F

(Dst

f

)

⇔ X ∩

f

1

Y 6

= 0

F

(Src

f

)

⇔ ∃

x

atoms

X

:

x

f

1

Y 6

= 0

F

(Src

f

)

⇔ ∃

x

atoms

X

:

Y ∩ h

f

i

x

6

= 0

F

(Dst

f

)

.

h

f

i X

=

S

h

i hh

f

ii

atoms

X

=

S

hh

f

ii

atoms

X

.

2. If

X

[

f

]

Y

, then

Y ∩ h

f

i X 6

= 0

F

(Dst

f

)

, consequently exists

y

atoms

Y

such that

y

∩ h

f

i X 6

= 0

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 follows

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y.

The reverse is obvious.

Theorem 16

Let

A

and

B

be small sets.

1. A function

α

F

(

B

)

atoms 1

F

(

A

)

such that (for every

a

atoms 1

F

(

A

)

)

αa

\ D[

◦ h

α

i ◦

atoms

◦ ↑

A

E

up

a

(6)

can be continued to the function

h

f

i

for a unique

f

FCD

(

A

;

B

)

;

h

f

i X

=

[

h

α

i

atoms

X

(7)

for every

X ∈

F

(

A

)

.

21