background image

9.3. GALOIS CONNECTIONS BETWEEN FUNCOIDS AND RELOIDS

206

Exercise

1103

.

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

1104

.

FCD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

(

FCD

)

g

⇔↑

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

g

for every reloid

g

.

Proof.

FCD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

(

FCD

)

g

FCD

(Src

g,

Dst

g

)

{

(

x, y

)

} 6

(

FCD

)

g

@

{

x

}

[(

FCD

)

g

]

@

{

y

} ⇔

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

} 6

g

⇔↑

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

g.

Theorem

1105

.

Cor(

FCD

)

g

= (

FCD

) Cor

g

for every reloid

g

.

Proof.

Cor(

FCD

)

g

=

l

FCD

(Src

g,

Dst

g

)

{

(

x, y

)

}

FCD

{

(

x, y

)

} v

(

FCD

)

g

=

l

FCD

(Src

g,

Dst

g

)

{

(

x, y

)

}

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

g

=

l

(

FCD

)

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

}

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

g

=

(

FCD

)

l

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

}

RLD

(Src

g,

Dst

g

)

{

(

x, y

)

} v

g

=

(

FCD

) Cor

g.

Conjecture

1106

.

1

. Cor(

RLD

)

in

g

= (

RLD

)

in

Cor

g

;

2

. Cor(

RLD

)

out

g

= (

RLD

)

out

Cor

g

.

Theorem

1107

.

For every reloid

f

:

1

. Compl(

FCD

)

f

= (

FCD

) Compl

f

;

2

. CoCompl(

FCD

)

f

= (

FCD

) CoCompl

f

.

Proof.

We will prove only the first, because the second is dual.

Compl(

FCD

)

f

=

d

α

Src

f

((

FCD

)

f

)

|

↑{

α

}

=

(proposition

1073

)

=

d

α

Src

f

(

FCD

)(

f

|

↑{

α

}

) = (

FCD

)

d

α

Src

f

f

|

↑{

α

}

= (

FCD

) Compl

f

.

Conjecture

1108

.

1

. Compl(

RLD

)

in

g

= (

RLD

)

in

Compl

g

;

2

. Compl(

RLD

)

out

g

= (

RLD

)

out

Compl

g

.

Note that the above Galois connection between funcoids and reloids is a Galois

surjection.

Proposition

1109

.

(

RLD

)

in

g

= max

n

f

RLD

(

FCD

)

f

v

g

o

= max

n

f

RLD

(

FCD

)

f

=

g

o

.

Proof.

By theorem

131

and proposition

320

.