background image

9.3. GALOIS CONNECTIONS BETWEEN FUNCOIDS AND RELOIDS

205

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

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

=

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

(

FCD

)

f

=

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

[(

FCD

)

f

]

b

=

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

RLD

b

6

f

w

l

p

atoms(

a

×

RLD

b

)

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, p

6

f

=

l

(

p

atoms

RLD

(

A,B

)

p

6

f

)

=

l

p

p

atoms

f

=

f.

Corollary

1097

.

1

. (

FCD

)

d

S

=

d

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

).

Theorem

1098

.

(

RLD

)

in

(

f

t

g

) = (

RLD

)

in

f

t

(

RLD

)

in

g

for every funcoids

f, g

FCD

(

A, B

).

Proof.

(

RLD

)

in

(

f

t

g

) =

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

f

t

g

=

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

f

a

×

FCD

b

v

g

=

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

f

t

l

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

g

=

(

RLD

)

in

f

t

(

RLD

)

in

g.

Proposition

1099

.

(

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

1100

.

(

RLD

)

in

(

f

|

A

) = ((

RLD

)

in

f

)

|

A

.

Conjecture

1101

.

(

RLD

)

in

is not a lower adjoint (in general).

Conjecture

1102

.

(

RLD

)

out

is neither a lower adjoint nor an upper adjoint

(in general).