background image

CHAPTER 4

Extending Galois connections between funcoids

and reloids

Definition

2203

.

1

. Φ

f

=

λb

B

:

d

n

x

A

f x

v

b

o

;

2

. Φ

f

=

λb

A

:

d

n

x

B

f x

w

b

o

.

Proposition

2204

.

1

. If

f

has upper adjoint then Φ

f

is the upper adjoint of

f

.

2

. If

f

has lower adjoint then Φ

f

is the lower adjoint of

f

.

Proof.

By theorem 131.

Lemma

2205

.

Φ

(

RLD

)

out

= (

FCD

).

Proof.

(

RLD

)

out

)

f

=

d

n

g

FCD

(

RLD

)

out

g

w

f

o

=

d

FCD

n

g

Rel

(

RLD

)

out

g

w

f

o

=

d

FCD

n

g

Rel

g

w

f

o

= (

FCD

)

f

.

Lemma

2206

.

Φ

(

RLD

)

out

6

= (

FCD

).

Proof.

(

RLD

)

out

)

f

=

d

n

g

FCD

(

RLD

)

out

g

v

f

o

(

RLD

)

out

)

⊥ 6

=

.

Lemma

2207

.

Φ

(

FCD

) = (

RLD

)

out

.

Proof.

(

FCD

))

f

=

d

n

g

RLD

(

FCD

)

g

w

f

o

=

d

RLD

n

g

Rel

(

FCD

)

g

w

f

o

=

d

RLD

n

g

Rel

g

w

f

o

=

(

RLD

)

out

f

.

Lemma

2208

.

Φ

(

RLD

)

in

= (

FCD

).

Proof.

(

RLD

)

in

)

f

=

d

n

g

FCD

(

RLD

)

in

g

v

f

o

=

d

n

g

FCD

g

v

(

FCD

)

f

o

= (

FCD

)

f

.

Theorem

2209

.

The picture at figure

1

describes values of functions Φ

and Φ

.

All nodes of this diagram are distinct.

Proof.

Follows from the above lemmas.

Figure 1

(

FCD

)

(

RLD

)

in

(

RLD

)

out

other

Φ

Φ

Φ

Φ

33