 6.13. COMPLETION OF FUNCOIDS

128

Proof.

1

For every

X

h

CoCompl(

g

f

)

i

X

=

Cor

h

g

f

i

X

=

Cor

h

g

ih

f

i

X

=

h

CoCompl

g

ih

f

i

X

=

h

(CoCompl

g

)

f

i

X.

2

(CoCompl(

g

f

))

1

=

f

1

(CoCompl

g

)

1

; Compl(

g

f

)

1

=

f

1

Compl

g

1

; Compl(

f

1

g

1

) =

f

1

Compl

g

1

. After variable replacement we

get Compl(

f

g

) =

f

Compl

g

(after the replacement

f

is a complete funcoid).

Corollary

705

.

CoCompl((Compl

g

)

f

) = Compl(

g

(CoCompl

f

)) = (Compl

g

)

(CoCompl

f

)

.

Proof.

By the theorem:

Compl(

g

(CoCompl

f

)) = (Compl

g

)

(CoCompl

f

);

CoCompl((Compl

f

)

g

) = (Compl

f

)

(CoCompl

g

)

.

After variable replacement CoCompl((Compl

g

)

f

) = (Compl

g

)

(CoCompl

f

).

Proposition

706

.

For every composable funcoids

f

and

g

1

. Compl(

g

(Compl

f

)) = Compl(

g

f

);

2

. CoCompl((CoCompl

g

)

f

) = CoCompl(

g

f

).

Proof.

1

.

h

g

(Compl

f

)

i

{

x

}

=

h

g

ih

Compl

f

i

{

x

}

=

h

g

ih

f

i

{

x

}

=

h

g

f

i

{

x

}

.

Thus Compl(

g

(Compl

f

)) = Compl(

g

f

).

2

(Compl(

g

(Compl

f

))

1

= (Compl(

g

f

))

1

; CoCompl(

g

(Compl

f

))

1

=

CoCompl(

g

f

)

1

; CoCompl((Compl

f

)

1

g

1

) = CoCompl(

f

1

g

1

);

CoCompl((CoCompl

f

1

)

g

1

) = CoCompl(

f

1

g

1

). After variable replace-

ment CoCompl((CoCompl

g

)

f

) = CoCompl(

g

f

).

6.13.1.1.

Open maps.

Definition

707

.

An

open map

from a topological space to a topological space

is a function which maps open sets into open sets.

An obvious generalization of this is

open map

f

from an endofuncoid

µ

to an

endofuncoid

ν

, which is by definition a function (or rather a principal, entirely

defined, monovalued funcoid) from Ob

µ

to Ob

ν

such that

x

Ob

µ, V

∈ h

µ

i

{

x

}

:

h

f

i

V

w h

ν

ih

f

i

{

x

}

.

This formula is equivalent (exercise!) to

x

Ob

µ

:

h

f

ih

µ

i

{

x

} w h

ν

ih

f

i

{

x

}

.

It can be abstracted/simplified further (now for an

arbitrary

funcoid f from

Ob

µ

to Ob

ν

):

Compl(

f

µ

)

w

Compl(

ν

f

)

.

Definition

708

.

An

open funcoid

from an endofuncoid

µ

to an endofuncoid

ν

is a funcoid

f

from Ob

µ

to Ob

ν

such that Compl(

f

µ

)

w

Compl(

ν

f

).