8.3. GALOIS CONNECTIONS BETWEEN FUNCOIDS AND RELOIDS

154

The second formula follows from the fact that (

FCD

)(

RLD

)

in

g

=

g

.

(

RLD

)

in

(

FCD

)

f

=

G

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

(

FCD

)

f

=

G

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

[(

FCD

)

f

]

b

=

G

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

RLD

b

6

f

w

G

p

atoms(

a

×

RLD

b

)

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, p

6

f

=

G

(

p

atoms

RLD

(

A

;

B

)

p

6

f

)

=

G

p

p

atoms

f

=

f.

Corollary

833

.

1

. (

FCD

)

F

S

=

F

h

(

FCD

)

i

S

if

S

P

RLD

(

A

;

B

).

2

. (

RLD

)

in

d

S

=

d

h

(

RLD

)

in

i

S

if

S

P

FCD

(

A

;

B

).

Proposition

834

.

(

RLD

)

in

(

f

u

(

A ×

FCD

B

)) = ((

RLD

)

in

f

)

u

(

A ×

RLD

B

) for

every funcoid

f

and

A ∈

F

(Src

f

),

B ∈

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

835

.

(

RLD

)

in

(

f

|

A

) = ((

RLD

)

in

f

)

|

A

.

Conjecture

836

.

(

RLD

)

in

is not a lower adjoint (in general).

Conjecture

837

.

(

RLD

)

out

is neither a lower adjoint nor an upper adjoint (in

general).

Exercise

838

.

Prove that card

FCD

(

A

;

B

) = 2

2

max

{

A,B

}

if

A

or

B

is an infinite

set (provided that

A

and

B

are nonempty).

Lemma

839

.

FCD

{

(

x

;

y

)

} v

(

FCD

)

g

⇔↑

RLD

{

(

x

;

y

)

} v

g

for every reloid

g

.

Proof.

FCD

{

(

x

;

y

)

} v

(

FCD

)

g

FCD

{

(

x

;

y

)

} 6

(

FCD

)

g

⇔ {

x

}

[(

FCD

)

g

]

{

y

} ⇔

RLD

{

(

x

;

y

)

} 6

g

⇔↑

RLD

{

(

x

;

y

)

} v

g.

Theorem

840

.

Cor(

FCD

)

g

= (

FCD

) Cor

g

for every reloid

g

.