background image

2.1. ORDER THEORY

29

Corollary

156

.

For a co-brouwerian lattice

a

t

d

S

=

d

h

a

ti

S

whenever

d

S

exists (for

a

being a lattice element and

S

being a set of lattice elements).

Definition

157

.

Let

a, b

A

where

A

is a complete lattice.

Quasidifference

a

\

b

is defined by the formula:

a

\

b

=

l

z

A

a

v

b

t

z

.

Remark

158

.

A more detailed theory of quasidifference (as well as quasicom-

plement and dual quasicomplement) will be considered below.

Lemma

159

.

(

a

\

b

)

t

b

=

a

t

b

for elements

a

,

b

of a meet infinite distributive

complete lattice.

Proof.

(

a

\

b

)

t

b

=

l

z

A

a

v

b

t

z

t

b

=

l

z

t

b

z

A

, a

v

b

t

z

=

l

t

A

t

w

b, a

v

t

=

a

t

b.

Theorem

160

.

The following are equivalent for a complete lattice

A

:

1

.

A

is a co-frame.

2

.

A

is meet infinite distributive.

3

.

A

is a co-brouwerian lattice.

4

.

A

is a co-Heyting lattice.

5

.

a

t −

has lower adjoint for every

a

A

.

Proof.

1

3

Because it is complete.

3

4

Obvious (taking into account completeness of

A

).

5

2

Let

− \

a

be the lower adjoint of

a

t −

. Let

S

P

A

. For every

y

S

we have

y

w

(

a

t

y

)

\

a

by properties of Galois connections; consequently

y

w

d

h

a

ti

S

\

a

;

d

S

w

d

h

a

ti

S

\

a

. So

a

t

l

S

w

l

h

a

ti

S

\

a

t

a

w

l

h

a

ti

S.

But

a

t

d

S

v

d

h

a

ti

S

is obvious.

2

3

Let

a

\

b

=

d

n

z

A

a

v

b

t

z

o

. To prove that

A

is a co-brouwerian lattice it is

enough to prove

a

v

b

t

(

a

\

b

). But it follows from the lemma.

3

5

.

a

\

b

= min

n

z

A

a

v

b

t

z

o

. So

a

t −

is the upper adjoint of

− \

a

.

2

5

Because

a

t −

preserves all meets.

Corollary

161

.

Co-brouwerian lattices are distributive.

The following theorem is essentially borrowed from [

19

]:

Theorem

162

.

A lattice

A

with least element

is co-brouwerian with pseu-

dodifference

\

iff

\

is a binary operation on

A

satisfying the following identities:

1

.

a

\

a

=

;