background image

3.9. SOME PROPERTIES OF FRAMES

56

Definition

325

.

Let

A

be a JSWLE. A

co-nucleus

is a function

F

:

A

A

such that for every

p, q

A

we have:

1

.

F

(

p

)

v

p

;

2

.

F

(

F

(

p

)) =

F

(

p

);

3

.

F

(

p

t

q

) =

F

(

p

)

t

F

(

q

).

Proposition

326

.

Every co-nucleus is a monotone function.

Proof.

It follows from

F

(

p

t

q

) =

F

(

p

)

t

F

(

q

).

Lemma

327

.

d

Fix(

F

)

S

=

d

S

for every

S

P

Fix(

F

) for every co-nucleus

F

on a complete lattice.

Proof.

Obviously

d

S

w

x

for every

x

S

.

Suppose

z

w

x

for every

x

S

for a

z

Fix(

F

). Then

z

w

d

S

.

F

(

d

S

)

w

F

(

x

) for every

x

S

. Thus

F

(

d

S

)

w

d

x

S

F

(

x

) =

d

S

. But

F

(

d

S

)

v

d

S

. Thus

F

(

d

S

) =

d

S

that is

d

S

Fix(

F

).

So

d

Fix(

F

)

S

=

d

S

by the definition of join.

Corollary

328

.

d

Fix(

F

)

S

is defined for every

S

P

Fix(

F

).

Lemma

329

.

d

Fix(

F

)

S

=

F

(

d

S

) for every

S

P

Fix(

F

) for every co-

nucleus

F

on a complete lattice.

Proof.

Obviously

F

(

d

S

)

v

x

for every

x

S

.

Suppose

z

v

x

for every

x

S

for a

z

Fix(

F

). Then

z

v

d

S

and thus

z

v

F

(

d

S

).

So

d

Fix(

F

)

S

=

F

(

d

S

) by the definition of meet.

Corollary

330

.

d

Fix(

F

)

S

is defined for every

S

P

Fix(

F

).

Obvious

331

.

Fix(

F

) with induced order is a complete lattice.

Lemma

332

.

If

F

is a co-nucleus on a co-frame

A

, then the poset Fix(

F

) of

fixed points of

F

, with order inherited from

A

, is also a co-frame.

Proof.

Let

b

Fix(

F

),

S

P

Fix(

F

). Then

b

t

Fix(

F

)

Fix(

F

)

l

S

=

b

t

Fix(

F

)

F

l

S

=

F

(

b

)

t

F

l

S

=

F

b

t

l

S

=

F

l

h

b

ti

S

=

Fix(

F

)

l

h

b

ti

S

=

Fix(

F

)

l

h

b

t

Fix(

F

)

i

S.

Definition

333

.

Denote Up(

A

) the set of upper sets on

A

ordered

reverse

to

set theoretic inclusion.

Definition

334

.

Denote

a

=

n

x

A

x

w

a

o

Up(

A

).