background image

CHAPTER 8

Systems of sides

Now we will consider a common generalization of (some of pointfree) funcoids

and (some of) Galois connections. The main purpose of this is general theorem

2274

below.

First consider some properties of Galois connections:

1. More on Galois connections

Here I will denote

h

f

i

the lower adjoint of a Galois connection

f

.

FiXme

:

Switch to this notation in the book?

Let

GAL

be the category of Galois connections.

FiXme

: Need to decide whether

use

GAL

(

A, B

) or

A

B

.

I will denote (

f, g

)

1

= (

g, f

) for a Galois connection (

f, g

).

We will order Galois connections by the formula

f

v

g

⇔ h

f

i v h

g

i ⇔

f

1

w

g

1

.

Obvious

2227

.

This defines a partial order on the set of Galois connections

between any two (fixed) posets.

Proposition

2228

.

If

f

and

g

are Galois connections (between a join-

semilattice

A

and a meet-semilattice

B

), then there exists a Galois connection

f

t

g

determined by the formula

h

f

t

g

i

x

=

h

f

i

x

t h

g

i

x

.

Proof.

It is enough to prove that

(

x

7→ h

f

i

x

t h

g

i

x, y

7→

f

1

y

u

g

1

y

)

is a Galois connection that is that

h

f

i

x

t h

g

i

x

v

y

x

v

f

1

y

u

g

1

y

for all relevant

x

and

y

.

Really,

h

f

i

x

t h

g

i

x

v

y

⇔ h

f

i

x

v

y

∧ h

g

i

x

v

y

x

v

f

1

y

x

v

g

1

y

x

v

f

1

y

u

g

1

y.

FiXme

: Describe infinite join of Galois connections.

Proposition

2229

.

If

A

is a poset with least element, then

h

a

i⊥

=

.

Proof.

h

a

i⊥ v

y

⇔ ⊥ v

a

1

y

1. Thus

h

a

i⊥

is the least element.

Proposition

2230

.

(

A

× {⊥

B

}

,

B

× {>

A

}

) is the least Galois connection from

a poset

A

with greatest element to a poset

B

with least element.

Proof.

Let’s prove that it is a Galois connection. We need to prove

(

A

× {⊥

B

}

)

x

v

y

x

v

(

B

× {>

A

}

)

y.

But this is trivially equivalent to 1

1. Thus it’s a Galois connection.

That it the least is obvious.

41