Theorem 68

a

×

RLD

b

(

RLD

)

in

f

a

×

FCD

b

f

for every funcoid

f

and

atomic f.o.

a

and

b

on the source and destination of

f

correspondingly.

Proof

a

×

FCD

b

f

a

×

RLD

b

(

RLD

)

in

f

is obvious.

a

×

RLD

b

(

RLD

)

in

f

a

×

RLD

b

6≍

(

RLD

)

in

f

a

[(

FCD

) (

RLD

)

in

f

]

b

a

[

f

]

b

a

×

FCD

b

f

.

A conjecture stronger than the last theorem:

Conjecture 18

If

A ×

RLD

B ⊆

(

RLD

)

in

f

then

A ×

FCD

B ⊆

f

for every funcoid

f

and

A ∈

F

(Src

f

)

,

B ∈

F

(Dst

f

)

.

5.3

Galois connections of funcoids and reloids

Theorem 69

(

FCD

) :

RLD

(

A

;

B

)

FCD

(

A

;

B

)

is the lower adjoint of

(

RLD

)

in

:

FCD

(

A

;

B

)

RLD

(

A

;

B

)

for every small sets

A

,

B

.

Proof

Because (

FCD

) and (

RLD

)

in

are trivially monotone, it’s enough to prove

(for every

f

RLD

(

A

;

B

),

g

FCD

(

A

;

B

))

f

(

RLD

)

in

(

FCD

)

f

and(

FCD

)(

RLD

)

in

g

g.

The second formula follows from the fact that (

FCD

)(

RLD

)

in

g

=

g

.

(

RLD

)

in

(

FCD

)

f

=

[ n

a

×

RLD

b

|

a

atoms 1

F

(

A

)

, b

atoms 1

F

(

B

)

, a

×

FCD

b

(

FCD

)

f

o

=

[ n

a

×

RLD

b

|

a

atoms 1

F

(

A

)

, b

atoms 1

F

(

B

)

, a

[(

FCD

)

f

]

b

o

=

[ n

a

×

RLD

b

|

a

atoms 1

F

(

A

)

, b

atoms 1

F

(

B

)

,

(

a

×

RLD

b

)

6≍

f

o

[ n

p

atoms(

a

×

RLD

b

)

|

a

atoms 1

F

(

A

)

, b

atoms 1

F

(

B

)

, p

6≍

f

o

=

[ n

p

atoms 1

RLD

(

A

;

B

)

|

p

6≍

f

o

=

[

{

p

|

p

atoms

f

}

=

f.

Corollary 17

1.

(

FCD

)

S

S

=

S

h

(

FCD

)

i

S

if

S

P

RLD

(

A

;

B

)

.

2.

(

RLD

)

in

T

S

=

T

h

(

RLD

)

in

i

S

if

S

P

FCD

(

A

;

B

)

.

Proposition 39

(

RLD

)

in

(

f

(

A ×

FCD

B

)) = ((

RLD

)

in

f

)

(

A ×

RLD

B

)

for every

funcoid

f

and f.o.

A ∈

F

(Src

f

)

and

B ∈

F

(Dst

f

)

.

58