background image

15.7. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS209

2

dom(

g

f

) = im(

f

1

g

1

) what by the proved is equal to im

f

1

that is

dom

f

.

15.6. Category of pointfree funcoids

I will define the category

pFCD

of pointfree funcoids:

The class of objects are small posets.

The set of morphisms from

A

to

B

is

FCD

(

A

;

B

).

The composition is the composition of pointfree funcoids.

Identity morphism for an object

A

is (

A

;

A

; id

A

; id

A

).

To prove that it is really a category is trivial.

The

category of pointfree funcoid triples

FiXme

: They are quintuples not triples.

is defined as follows:

Objects are pairs (

A

;

A

) where

A

is a small poset and

A ∈

A

.

The morphisms from an object (

A

;

A

) to an object (

B

;

B

) are tuples

(

A

;

B

;

A

;

B

;

f

) where

f

FCD

(

A

;

B

) and dom

f

v A ∧

im

f

v B

.

FiXme

:

Domain and image are not always defined. Even if it’s defined, the com-

position law may not hold. We can require instead

f

v A ×

FCD

B

, but

this is defined only for posets with least elements.

The composition is defined by the formula (

B

;

C

;

g

)

(

A

;

B

;

f

) = (

A

;

C

;

g

f

).

Identity morphism for an object (

A

;

A

) is id

FCD

(

A

)

A

.

FiXme

: Defined only

for meet-semilattices. We can also define a wider precategory without

identity.

To prove that it is really a category is trivial.

15.7. Specifying funcoids by functions or relations on atomic filters

Theorem

1110

.

Let

A

be an atomic poset and (

B

;

Z

1

) is a primary filtrator

over a boolean lattice. Then for every

f

FCD

(

A

;

B

) and

X ∈

A

we have

h

f

iX

=

B

G

hh

f

ii

atoms

A

X

.

Proof.

For every

Y

Z

1

we have

Y

6

B

h

f

iX ⇔ X 6

A

f

1

Y

x

atoms

A

X

:

x

6

A

f

1

Y

⇔ ∃

x

atoms

A

X

:

Y

6

B

h

f

i

x.

Thus

h

f

iX

=

S

h

i

hh

f

ii

atoms

A

X

=

F

B

hh

f

ii

atoms

A

X

(used theorem

399

).

Consequently

h

f

iX

=

F

B

hh

f

ii

atoms

A

X

by the corollary

395

.

Proposition

1111

.

Let

f

be a pointfree funcoid. Then for every

X ∈

Src

f

and

Y ∈

Dst

f

1

.

X

[

f

]

Y ⇔ ∃

x

atoms

X

:

x

[

f

]

Y

if Src

f

is an atomic poset.

2

.

X

[

f

]

Y ⇔ ∃

y

atoms

Y

:

X

[

f

]

y

if Dst

f

is an atomic poset.

Proof.

I will prove only the second as the first is similar.

If

X

[

f

]

Y

, then

Y 6 h

f

iX

, consequently exists

y

atoms

Y

such that

y

6

h

f

iX

,

X

[

f

]

y

. The reverse is obvious.

Corollary

1112

.

If

f

is a pointfree funcoid with both source and destination

being atomic posets, then for every

X ∈

Src

f

and

Y ∈

Dst

f

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y.