background image

dom

f

=

S

Src

f

{

a

atoms

Src

f

|

a

Src

f

dom

f

}

=

S

Src

f

{

a

atoms

Src

f

| h

f

i

a

0

Dst

f

}

.

Proposition 49.

dom

f

|

a

FCD

(

Src

f

)

=

a

Src

f

dom

f

for every pointfree funcoid

f

and

a

Src

f

where

Src

f

is a meet-semilattice and Dst

f

has greatest element.

Proof.

dom

f

|

a

FCD

(

Src

f

)

=

im

I

a

FCD

(

Src

f

)

f

1

=

D

I

a

FCD

(

Src

f

)

E

h

f

1

i

1

Dst

f

=

a

Src

f

h

f

1

i

1

Dst

f

=

a

Src

f

dom

f

.

Proposition 50.

For every composable pointfree funcoids

f

and

g

where the posets Src

f

and

Dst

f

=

Src

g

have greatest elements:

1. If im

f

dom

g

then im

(

g

f

) =

im

g

.

2. If im

f

dom

g

then dom

(

g

f

) =

dom

g

.

Proof.

1. im

(

g

f

) =

h

g

f

i

1

Src

f

=

h

g

ih

f

i

1

Src

f

=

h

g

i

im

f

=

h

g

i

(

im

f

Dst

f

dom

g

) =

h

g

i

dom

g

=

h

g

i

1

Src

g

=

im

g

.

2. dom

(

g

f

) =

im

(

f

1

g

1

)

what by the proved is equal to im

f

1

that is dom

f

.

3.7 Category of pointfree funcoids

I will define the category pf

FCD

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

; (=)

|

A

; (=)

|

A

)

.

To prove that it is really a category is trivial.

The

category of funcoid 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

(

f

;

A

;

B

;

A

;

B

)

where

f

FCD

(

A

;

B

)

and dom

f

⊆ A ∧

im

f

⊆ B

.

The composition is defined by the formula

(

g

;

B

;

C

)

(

f

;

A

;

B

) = (

g

f

;

A

;

C

)

.

Identity morphism for an object

(

A

;

A

)

is

I

A

FCD

(

A

)

.

To prove that it is really a category is trivial.

3.8 Specifying funcoids by functions or relations on atomic filter objects

Theorem 51.

Let

A

is 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

hh

f

ii

atoms

A

X

.

Proof.

For every

Y

Z

1

we have

Y

B

h

f

iX ⇔ X

A

h

f

1

i

Y

⇔ ∃

x

atoms

A

X

:

x

A

h

f

1

i

Y

⇔ ∃

x

atoms

A

X

:

Y

B

h

f

i

x.

Thus

h

f

iX

=

S

h

i hh

f

ii

atoms

A

X

=

S

B

hh

f

ii

atoms

A

X

(used the theorem 46 in [3]).

Consequently

h

f

iX

=

S

B

hh

f

ii

atoms

A

X

by the corollary 15 in [3].

Pointfree funcoids

9