background image

3. CONCRETE EXAMPLES OF SIDES

44

3.2. Funcoids and pointfree funcoids.

Proposition

2258

.

The category of pointfree funcoids between starrish join-

semilattices with usual

h

f

i

defines a system of presides.

Proof.

Theorem 1627.

Proposition

2259

.

The category of pointfree funcoids between bounded star-

rish join-semilattices with usual

h

f

i

defines a system of bounded presides.

Proof.

Take the proof of theorem 1624 into account.

Proposition

2260

.

The category of pointfree funcoids from a starrish join-

semilattices to a separable starrish join-semilattices defines a distributive system of
presides.

Proof.

Theorem 1599.

Proposition

2261

.

The category of pointfree funcoids between starrish lat-

tices with usual

h

f

i

and usual id

c

defines a system of presides with correct identities.

Proof.

That it is with identities is obvious.

That it is with correct identities is obvious.

Obvious

2262

.

The category of pointfree funcoids between bounded starrish

lattices with usual

h

f

i

and usual id

c

defines a system of sides with correct identities.

Proposition

2263

.

The category of funcoids with usual

h

f

i

and usual id

c

defines a system of sides with correct identities.

Proof.

Because it can be considered a full subsystem of the category of point-

free funcoids between bounded starrish lattices with usual

h

f

i

.

3.3. Galois connections.

Proposition

2264

.

The category of Galois connections between (small) lat-

tices with least elements together with usual

h

f

i

defines a distributive system of

presides.

Proof.

Propositions

2228

and

2229

for a system of presides.

It is distributive because lower adjoints preserve all joins.

Proposition

2265

.

The category of Galois connections between (small)

bounded lattices together with usual

h

f

i

defines a bounded system of presides.

Proof.

Theorem

2232

.

Proposition

2266

.

The category of Galois connections between (small) Heyt-

ing lattices together with usual

h

f

i

defines a system of sides with correct identities.

Proof.

Theorem

2233

ensures that they a system of sides with identities. The

identities are correct due to faithfulness.

3.4. Reloids.

Proposition

2267

.

Reloids with the functor

f

7→ h

(

FCD

)

f

i

and usual id

c

form

a system of sides with correct identities.

Proof.

It

is

really

a

functor

because

h

(

FCD

)

g

i ◦ h

(

FCD

)

f

i

=

h

(

FCD

)

g

(

FCD

)

f

i

=

h

(

FCD

)(

g

f

)

i

for every composable reloids

f

and

g

.

h

a

i⊥

=

h

(

FCD

)

a

i⊥

=

;

h

a

t

b

i

X

=

h

(

FCD

)(

a

t

b

)

i

X

=

h

(

FCD

)

a

t

(

FCD

)

b

)

i

X

=

h

(

FCD

)

a

i

X

t h

(

FCD

)

b

i

X

=

h

a

i

X

t h

b

i

X

;