6.3 Funcoid as continuation

Let

f

be a funcoid.

Denition 6.21.

h

f

i

is the function

P

(

Src

f

)

!

F

(

Dst

f

)

dened by the formula

h

f

i

X

=

h

f

i"

Src

f

X:

Denition 6.22.

[

f

]

is the relation between

P

(

Src

f

)

and

P

(

Dst

f

)

dened by the formula

X

[

f

]

Y

, "

Src

f

X

[

f

]

"

Dst

Y :

Obvious 6.23.

1.

h

f

i

=

h

f

i  "

Src

f

;

2.

[

f

]

=(

"

Dst

)

¡

1

[

f

]

"

Src

f

.

Obvious 6.24.

h

g

ih

f

i

X

=

h

g

f

i

X

for every

X

2

P

(

Src

f

)

.

Theorem 6.25.

For every funcoid

f

and

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

1.

h

f

iX

=

d

hh

f

i

iX

;

2.

X

[

f

]

Y , 8

X

2 X

; Y

2 Y

:

X

[

f

]

Y

.

Proof.

2.

X

[

f

]

Y , Y u h

f

iX

=

/ 0

F

(

Dst

f

)

, 8

Y

2 Y

:

"

Dst

f

Y

u h

f

iX

=

/ 0

F

(

Dst

f

)

, 8

Y

2 Y

:

X

[

f

]

"

Dst

f

Y

.

Analogously

X

[

f

]

Y , 8

X

2 X

:

"

Src

f

X

[

f

]

Y

. Combining these two equivalences we get

X

[

f

]

Y , 8

X

2 X

; Y

2 Y

:

"

Src

f

X

[

f

]

"

Dst

f

Y

, 8

X

2 X

; Y

2 Y

:

X

[

f

]

Y :

1.

Y u h

f

iX

=

/ 0

F

(

Dst

f

)

, X

[

f

]

Y , 8

X

2 X

:

"

Src

f

X

[

f

]

Y , 8

X

2 X

:

Y u h

f

i

X

=

/ 0

F

(

Dst

f

)

.

Let's denote

W

=

fY u h

f

i

X

j

X

2 X g

. We will prove that

W

is a generalized lter base. To

prove this it is enough to show that

V

=

fh

f

i

X

j

X

2 X g

is a generalized lter base.

Let

P

;

Q 2

V

. Then

P

=

h

f

i

A

,

Q

=

h

f

i

B

where

A; B

2 X

;

A

\

B

2 X

and

R v P u Q

for

R

=

h

f

i

(

A

\

B

)

2

V

. So

V

is a generalized lter base and thus

W

is a generalized lter base.

0

F

(

Dst

f

)

2

/

W

,

d

W

=

/ 0

F

(

Dst

f

)

by properties of generalized lter bases. That is

8

X

2 X

:

Y u h

f

i

X

=

/ 0

F

(

Dst

f

)

, Y u

l

hh

f

i

iX

=

/ 0

F

(

Dst

f

)

:

Comparing with the above,

Y u h

f

iX

=

/ 0

F

(

Dst

f

)

, Y u

d

hh

f

i

iX

=

/ 0

F

(

Dst

f

)

. So

h

f

iX

=

d

hh

f

i

iX

because the lattice of lters is separable.

Corollary 6.26.

Let

f

be a funcoid.

1. The value of

f

can be restored knowing

h

f

i

.

2. The value of

f

can be restored knowing

[

f

]

.

Proposition 6.27.

For every

f

2

FCD

(

A

;

B

)

we have (for every

I ; J

2

P

A

)

h

f

i

;

= 0

F

(

B

)

;

h

f

i

(

I

[

J

) =

h

f

i

I

t h

f

i

J

and

:

(

I

[

f

]

;

)

;

I

[

J

[

f

]

K

,

I

[

f

]

K

_

J

[

f

]

K

(for every

I ; J

2

P

A

,

K

2

P

B

)

;

:

(

;

[

f

]

I

)

;

K

[

f

]

I

[

J

,

K

[

f

]

I

_

K

[

f

]

J

(for every

I ; J

2

P

B

,

K

2

P

A

)

:

Proof.

h

f

i

;

=

h

f

i"

A

;

=

h

f

i

0

F

(

A

)

= 0

F

(

B

)

;

h

f

i

(

I

[

J

) =

h

f

i"

A

(

I

[

J

) =

h

f

i"

A

I

t h

f

i"

A

J

=

h

f

i

I

t h

f

i

J

.

I

[

f

]

; ,

0

F

(

B

)

/

h

f

i"

A

I

,

0

;

I

[

J

[

f

]

K

, "

A

(

I

[

J

) [

f

]

"

B

K

, "

B

K

/

h

f

i"

A

(

I

[

J

)

,

"

B

K

/

h

f

i

(

I

[

J

)

, "

B

K

/

h

f

i

I

t h

f

i

J

, "

B

K

/

h

f

i

I

_ "

B

K

/

h

f

i

J

,

I

[

f

]

K

_

J

[

f

]

K

.

The rest follows from symmetry.

98

Funcoids