background image

2. atoms

(

f

t

d

R

) =

atoms

f

[

atoms

d

R

=

atoms

f

[

T

h

atoms

i

R

=

T

h

(

atoms

f

)

[

ih

atoms

i

R

=

T

h

atoms

ih

f

t i

R

=

atoms

d

h

f

t i

R

. (Used the following equality.)

h

(

atoms

f

)

[ ih

atoms

i

R

=

f

(

atoms

f

)

[

A

j

A

2 h

atoms

i

R

g

=

f

(

atoms

f

)

[

A

j 9

C

2

R

:

A

=

atoms

C

g

=

f

(

atoms

f

)

[

(

atoms

C

)

j

C

2

R

g

=

f

atoms

(

f

t

C

)

j

C

2

R

g

=

f

atoms

B

j 9

C

2

R

:

B

=

f

t

C

g

=

f

atoms

B

j

B

2 h

f

t i

R

g

=

h

atoms

ih

f

t i

:

Corollary 15.84.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. Then

FCD

(

A

;

B

)

is a co-brouwerian lattice.

Proposition 15.85.

Let

A

,

B

,

C

be sets of lters over some boolean lattices and

f

2

FCD

(

A

;

B

)

,

g

2

FCD

(

B

;

C

)

. Let

B

be an atomic poset. Then

atoms

(

g

f

) =

f

x

FCD

z

j

x

2

atoms

A

; z

2

atoms

C

;

9

y

2

atoms

B

: (

x

FCD

y

2

atoms

f

^

y

FCD

z

2

atoms

g

)

g

:

Proof.

(

x

FCD

z

)

u

(

g

f

) =

/ 0

FCD

(

A

;

C

)

,

x

[

g

f

]

z

, 9

y

2

atoms

B

: (

x

[

f

]

y

^

y

[

g

]

z

)

, 9

y

2

atoms

B

:

((

x

FCD

y

)

u

f

=

/ 0

FCD

(

A

;

B

)

^

(

y

FCD

z

)

u

g

=

/ 0

FCD

(

B

;

C

)

)

(were used corollary

15.69

and theorem

15.61

).

Theorem 15.86.

Let

f

be a pointfree funcoid between sets of lters on boolean lattices.

1.

X

[

f

]

Y , 9

F

2

atoms

f

:

X

[

F

]

Y

for every

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

;

2.

h

f

iX

=

F

F

2

atoms

f

h

F

iX

for every

X 2

F

(

Src

f

)

.

Proof.

1.

9

F

2

atoms

f

:

X

[

F

]

Y , 9

a

2

atoms

F

(

Src

f

)

; b

2

atoms

F

(

Dst

f

)

: (

a

FCD

b

/

f

^ X

[

a

FCD

b

]

Y

)

, 9

a

2

atoms

F

(

Src

f

)

; b

2

atoms

F

(

Dst

f

)

: (

a

FCD

b

/

f

^

a

FCD

b

/

FCD

Y

)

, 9

F

2

atoms

f

:

(

F

/

f

^

F

/

FCD

Y

)

,

f

/

FCD

Y , X

[

f

]

Y

.

2. Let

Y 2

F

(

Dst

f

)

. Suppose

/

h

f

iX

. Then

X

[

f

]

Y

;

9

F

2

atoms

f

:

X

[

F

]

Y

;

9

F

2

atoms

f

:

/

h

F

iX

;

/

F

F

2

atoms

f

h

F

iX

. So

h

f

iX v

F

F

2

atoms

f

h

F

iX

. The contrary

h

f

iX w

F

F

2

atoms

f

h

F

iX

is obvious.

15.11 Complete pointfree funcoids

Denition 15.87.

Let

A

and

B

be posets. A pointfree funcoid

f

2

FCD

(

A

;

B

)

is

complete

, when

for every

S

2

P

A

whenever both

F

S

and

F

hh

f

ii

S

are dened we have

h

f

i

G

S

=

G

hh

f

ii

S:

Proposition 15.88.

Let

A

,

B

be sets of lters over boolean lattices. A pointfree funcoid

f

2

FCD

(

A

;

B

)

is complete i

h

f

i

a

=

F

hh

f

ii

atoms

a

for every

a

2

A

.

Proof.

Direct implication is obvious. The reverse implication:

Let

S

be a set of lters.

h

f

i

F

S

=

F

hh

f

ii

atoms

F

S

=

F

hh

f

ii

S

h

atoms

i

S

=

F S

hhh

f

iii h

atoms

i

S

=

F

h

F

ihhh

f

iii h

atoms

i

S

=

F

h

F

hh

f

ii 

atoms

i

S

=

F

f

F

hh

f

ii

atoms

a

j

a

2

S

g

=

F

fh

f

i

a

j

a

2

S

g

=

F

hh

f

ii

S

.

192

Pointfree funcoids