background image

9.3. GALOIS CONNECTIONS BETWEEN FUNCOIDS AND RELOIDS

204

a

×

RLD

b

v

(

RLD

)

in

f

a

×

RLD

b

6

(

RLD

)

in

f

a

[(

FCD

)(

RLD

)

in

f

]

b

a

[

f

]

b

a

×

FCD

b

v

f.

Conjecture

1092

.

If

A ×

RLD

B v

(

RLD

)

in

f

then

A ×

FCD

B v

f

for every

funcoid

f

and

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Theorem

1093

.

up(

FCD

)

g

up

g

for every reloid

g

.

Proof.

Let

K

up

g

. Then for every typed sets

X

T

Src

g

,

Y

T

Dst

g

X

[

K

]

Y

X

FCD

K

Y

X

(

FCD

)

RLD

K

Y

X

[(

FCD

)

g

]

Y.

Thus

FCD

K

w

(

FCD

)

g

that is

K

up(

FCD

)

g

.

Theorem

1094

.

g

(

A ×

RLD

B

)

f

=

(

FCD

)

f

1

A ×

RLD

h

(

FCD

)

g

iB

for every

reloids

f

,

g

and filters

A ∈

F

(Dst

f

),

B ∈

F

(Src

g

).

Proof.

g

(

A ×

RLD

B

)

f

=

RLD

l

G

(

A

×

B

)

F

F

up

f, G

up

g, A

up

A

, B

up

B

=

RLD

l

(

F

1

A

× h

G

i

B

F

up

f, G

up

g, A

up

A

, B

up

B

)

=

RLD

l

(

F

1

A

×

RLD

h

G

i

B

F

up

f, G

up

g, A

up

A

, B

up

B

)

=

(theorem

1013

)

F

l

(

F

1

A

F

up

f, A

up

A

)

×

RLD

F

l

h

G

i

B

G

up

g, B

up

B

=

F

l

(

FCD

F

1

A

F

up

f, A

up

A

)

×

RLD

F

l

(

FCD

G

B

G

up

g, B

up

B

)

=

F

l

FCD

F

1

A

F

up

f

)

×

RLD

F

l

FCD

G

B

G

up

g

)

=

(by definition of (

FCD

))

(

FCD

)

f

1

A ×

RLD

h

(

FCD

)

g

iB

.

Corollary

1095

.

1

. (

A ×

RLD

B

)

f

=

(

FCD

)

f

1

A ×

RLD

B

;

2

.

g

(

A ×

RLD

B

) =

A ×

RLD

h

(

FCD

)

g

iB

.

9.3. Galois connections between funcoids and reloids

Theorem

1096

.

(

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

.