 Proof.

g

(

RLD

B

)

f

=

d

"

RLD

(

Src

f

;

Dst

g

)

(

G

(

A

B

)

F

)

j

F

2

GR

f ; G

2

GR

g;

A

2 A

; B

2 B

=

d

"

RLD

(

Src

f

;

Dst

g

)

(

h

F

¡

1

i

A

h

G

i

B

)

j

F

2

GR

f ; G

2

GR

g; A

2 A

;

B

2 B

=

d

f"

Src

f

h

F

¡

1

i

A

RLD

"

Dst

g

h

G

i

B

j

F

2

GR

f ; G

2

GR

g; A

2 A

; B

2 Bg

=

(theorem

7.23

)

=

d

f"

Src

f

h

F

¡

1

i

A

j

F

2

GR

f ; A

2 Ag

RLD

d

f"

Dst

g

h

G

i

B

j

G

2

GR

g; B

2 Bg

=

d

"

FCD

(

Dst

f

;

Src

f

)

F

¡

1

"

Dst

f

A

j

F

2

GR

f ; A

2 A

RLD

d

"

FCD

(

Src

g

;

Dst

g

)

G

"

Src

g

B

j

G

2

GR

g; B

2 B

=

d

"

FCD

(

Dst

f

;

Src

f

)

F

¡

1

A j

F

2

GR

f

RLD

d

"

FCD

(

Src

g

;

Dst

g

)

G

B j

G

2

GR

g

=

(by denition of

(

FCD

)

)

=

h

(

FCD

)

f

¡

1

iA

RLD

h

(

FCD

)

g

iB

.

Corollary 8.32.

1.

(

RLD

B

)

f

=

h

(

FCD

)

f

¡

1

iA

RLD

B

;

2.

g

(

RLD

B

) =

RLD

h

(

FCD

)

g

iB

.

8.3 Galois connections between funcoids and reloids

Theorem 8.33.

(

FCD

):

RLD

(

A

;

B

)

!

FCD

(

A

;

B

)

is the lower adjoint of

(

RLD

)

in

:

FCD

(

A

;

B

)

!

RLD

(

A

;

B

)

for every sets

A

,

B

.

Proof.

Because

(

FCD

)

and

(

RLD

)

in

are trivially monotone, it's enough to prove (for every

f

2

RLD

(

A

;

B

)

,

g

2

FCD

(

A

;

B

)

)

f

v

(

RLD

)

in

(

FCD

)

f

and

(

FCD

)(

RLD

)

in

g

v

g:

The second formula follows from the fact that

(

FCD

)(

RLD

)

in

g

=

g

.

(

RLD

)

in

(

FCD

)

f

=

a

RLD

b

j

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; a

FCD

b

v

(

FCD

)

f

=

a

RLD

b

j

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; a

[(

FCD

)

f

]

b

=

a

RLD

b

j

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; a

RLD

b

/

f

w

p

2

atoms

(

a

RLD

b

)

j

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; p

/

f

=

p

2

atoms

RLD

(

A

;

B

)

j

p

/

f

=

G

f

p

j

p

2

atoms

f

g

=

f :

Corollary 8.34.

1.

(

FCD

)

F

S

=

F

h

(

FCD

)

i

S

if

S

2

P

RLD

(

A

;

B

)

.

2.

(

RLD

)

in

d

S

=

d

h

(

RLD

)

in

i

S

if

S

2

P

FCD

(

A

;

B

)

.

Proposition 8.35.

(

RLD

)

in

(

f

u

(

FCD

B

)) = ((

RLD

)

in

f

)

u

(

RLD

B

)

for every funcoid

f

and

A 2

F

(

Src

f

)

,

B 2

F

(

Dst

f

)

.

Proof.

(

RLD

)

in

(

f

u

(

FCD

B

)) = ((

RLD

)

in

f

)

u

(

RLD

)

in

(

FCD

B

) = ((

RLD

)

in

f

)

u

(

RLD

B

)

.

Corollary 8.36.

(

RLD

)

in

(

f

j

A

) = ((

RLD

)

in

f

)

j

A

.

Conjecture 8.37.

(

RLD

)

in

is not a lower adjoint (in general).

Conjecture 8.38.

(

RLD

)

out

is neither a lower adjoint nor an upper adjoint (in general).

Exercise 8.2.

Prove that card

FCD

(

A

;

B

) = 2

2

max

f

A;B

g

if

A

or

B

is an innite set (provided that

A

and

B

are

nonempty).

Lemma 8.39.

"

FCD

f

(

x

;

y

)

g v

(

FCD

)

g

, "

RLD

f

(

x

;

y

)

g v

g

for every reloid

g

.

136

Relationships between funcoids and reloids