background image

8.3. GALOIS CONNECTIONS BETWEEN FUNCOIDS AND RELOIDS

153

Proof.

Let

K

GR

g

. Then for every sets

X

P

Src

g

,

Y

P

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

GR(

FCD

)

g

.

Theorem

830

.

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

).

FiXme

: Similar proposition for

funcoids?

Proof.

g

(

A ×

RLD

B

)

f

=

l

RLD

(Src

f

;Dst

g

)

(

G

(

A

×

B

)

F

)

F

GR

f, G

GR

g, A

∈ A

, B

∈ B

=

l

(

RLD

(Src

f

;Dst

g

)

(

F

1

A

× h

G

i

B

)

F

GR

f, G

GR

g, A

∈ A

, B

∈ B

)

=

l

(

Src

f

F

1

A

×

RLD

Dst

g

h

G

i

B

)

F

GR

f, G

GR

g, A

∈ A

, B

∈ B

)

=

(theorem

753

)

l

(

Src

f

F

1

A

F

GR

f, A

∈ A

)

×

RLD

l

Dst

g

h

G

i

B

G

GR

g, B

∈ B

=

l

FCD

(Dst

f

;Src

f

)

F

1

A

F

GR

f, A

∈ A

)

×

RLD

l

FCD

(Src

g

;Dst

g

)

G

B

G

GR

g, B

∈ B

)

=

l

FCD

(Dst

f

;Src

f

)

F

1

A

F

GR

f

)

×

RLD

l

FCD

(Src

g

;Dst

g

)

G

B

G

GR

g

)

=

(by definition of (

FCD

))

(

FCD

)

f

1

A ×

RLD

h

(

FCD

)

g

iB

.

Corollary

831

.

1

. (

A ×

RLD

B

)

f

=

(

FCD

)

f

1

A ×

RLD

B

;

2

.

g

(

A ×

RLD

B

) =

A ×

RLD

h

(

FCD

)

g

iB

.

8.3. Galois connections between funcoids and reloids

Theorem

832

.

(

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

RLD

(

A

;

B

),

g

FCD

(

A

;

B

))

f

v

(

RLD

)

in

(

FCD

)

f

and (

FCD

)(

RLD

)

in

g

v

g.