background image

7.14. COMPLETION OF FUNCOIDS

174

7.13. Funcoids corresponding to pretopologies

Let ∆ be a pretopology on a set

U

and cl the preclosure corresponding to it

(see theorem

774

).

Both induce a funcoid, I will show that these two funcoids are reverse of each

other:

Theorem

931

.

Let

f

be a complete funcoid defined by the formula

h

f

i

@

{

x

}

=

∆(

x

) for every

x

U

, let

g

be a co-complete funcoid defined by the formula

h

g

i

X

=

U

cl(GR

X

) for every

X

T

U

. Then

g

=

f

1

.

Remark

932

.

It is obvious that funcoids

f

and

g

exist.

Proof.

For

X, Y

T

U

we have

X

[

g

]

Y

Y

6 h

g

i ↑

X

Y

6

cl(GR

X

)

y

Y

: ∆(

y

)

6↑

X

y

Y

:

h

f

i

U

{

y

} 6↑

X

(proposition

607

and properties of complete funcoids)

h

f

i

Y

6↑

X

Y

[

f

]

X.

So

g

=

f

1

.

7.14. Completion of funcoids

Theorem

933

.

Cor

f

= Cor

0

f

for an element

f

of a filtrator of funcoids.

Proof.

By theorem

542

and corollary

922

.

Definition

934

.

Completion

of a funcoid

f

FCD

(

A, B

) is the complete

funcoid Compl

f

FCD

(

A, B

) defined by the formula

h

Compl

f

i

@

{

α

}

=

h

f

i

@

{

α

}

for

α

Src

f

.

Definition

935

.

Co-completion

of a funcoid

f

is defined by the formula

CoCompl

f

= (Compl

f

1

)

1

.

Obvious

936

.

Compl

f

v

f

and CoCompl

f

v

f

.

Proposition

937

.

The filtrator (

FCD

(

A, B

)

,

ComplFCD

(

A, B

)) is filtered.

Proof.

Because the filtrator of funcoids is filtered.

Theorem

938

.

Compl

f

= Cor

ComplFCD

(

A,B

)

f

= Cor

0

ComplFCD

(

A,B

)

f

for every

funcoid

f

FCD

(

A, B

).

Proof.

Cor

ComplFCD

(

A,B

)

f

= Cor

0

ComplFCD

(

A,B

)

f

using theorem

542

since the

filtrator (

FCD

(

A, B

)

,

ComplFCD

(

A, B

)) is filtered.

Let

g

up

ComplFCD

(

A,B

)

f

. Then

g

ComplFCD

(

A, B

) and

g

w

f

. Thus

g

= Compl

g

w

Compl

f

.

Thus

g

up

ComplFCD

(

A,B

)

f

:

g

w

Compl

f

.

Let

g

up

ComplFCD

(

A,B

)

f

:

h

v

g

for some

h

ComplFCD

(

A, B

).

Then

h

v

d

up

ComplFCD

(

A,B

)

f

=

f

and consequently

h

= Compl

h

v

Compl

f

.

Thus

Compl

f

=

ComplFCD

(

A,B

)

l

up

ComplFCD

(

A,B

)

f

= Cor

ComplFCD

(

A,B

)

f.