background image

15.2 Composition of pointfree funcoids

Denition 15.17.

Composition

of pointfree funcoids is dened by the formula

(

B

;

C

;

2

;

2

)

(

A

;

B

;

1

;

1

) = (

A

;

C

;

2

1

;

1

2

)

:

Denition 15.18.

I will call funcoids

f

and

g

composable

when Dst

f

=

Src

g

.

Proposition 15.19.

If

f

,

g

are composable pointfree funcoids then

g

f

is pointfree funcoid.

Proof.

Let

f

= (

A

;

B

;

1

;

1

)

,

g

= (

B

;

C

;

2

;

2

)

. For every

x; y

2

A

we have

y

/ (

2

1

)

x

,

y

/

2

1

x

,

1

x

/

2

y

,

x

/

1

2

y

,

x

/ (

1

2

)

y:

So

(

A

;

C

;

2

1

;

1

2

)

is a pointfree funcoid.

Obvious 15.20.

h

g

f

i

=

h

g

i  h

f

i

for every composable pointfree funcoids

f

and

g

.

Theorem 15.21.

(

g

f

)

¡

1

=

f

¡

1

g

¡

1

for every composable pointfree funcoids

f

and

g

.

Proof.

h

(

g

f

)

¡

1

i

=

h

f

¡

1

i  h

g

¡

1

i

=

h

f

¡

1

g

¡

1

i

;

h

((

g

f

)

¡

1

)

¡

1

i

=

h

g

f

i

=

h

(

f

¡

1

g

¡

1

)

¡

1

i

:

Proposition 15.22.

(

h

g

)

f

=

h

(

g

f

)

for every composable pointfree funcoids

f

,

g

,

h

.

Proof.

h

(

h

g

)

f

i

=

h

h

g

i  h

f

i

=

h

h

i  h

g

i  h

f

i

=

h

h

i  h

g

f

i

=

h

h

(

g

f

)

i

.

h

((

h

g

)

f

)

¡

1

i

=

h

f

¡

1

(

h

g

)

¡

1

i

=

h

f

¡

1

g

¡

1

h

¡

1

i

=

h

(

g

f

)

¡

1

h

¡

1

i

=

h

(

h

(

g

f

))

¡

1

i

.

15.3 Pointfree funcoid as continuation

Proposition 15.23.

Let

f

be a pointfree funcoid. Then for every

x

2

Src

f

,

y

2

Dst

f

we have

1. If

(

Src

f

;

Z

)

is a ltrator with separable core then

x

[

f

]

y

, 8

X

2

up

(

Src

f

;

Z

)

x

:

X

[

f

]

y

.

2. If

(

Dst

f

;

Z

)

is a ltrator with separable core then

x

[

f

]

y

, 8

Y

2

up

(

Dst

f

;

Z

)

y

:

x

[

f

]

Y

.

Proof.

We will prove only the second because the rst is similar.

x

[

f

]

y

,

y

/

Dst

f

h

f

i

x

, 8

Y

2

up

(

Dst

f

;

Z

)

y

:

Y

/

Dst

f

h

f

i

x

, 8

Y

2

up

(

Dst

f

;

Z

)

y

:

x

[

f

]

Y

.

Corollary 15.24.

Let

f

be a pointfree funcoid and

(

Src

f

;

Z

0

)

,

(

Dst

f

;

Z

1

)

are ltrators with

separable core. Then

x

[

f

]

y

, 8

X

2

up

(

Src

f

;

Z

0

)

x; Y

2

up

(

Dst

f

;

Z

1

)

y

:

X

[

f

]

Y :

Proof.

Apply the proposition twice.

Theorem 15.25.

Let

f

be a pointfree funcoid. Let

(

Src

f

;

Z

0

)

be a nitely meet-closed ltrator

with separable core which is a meet-semilattice and

8

x

2

Src

f

:

up

(

Src

f

;

Z

0

)

x

=

/

;

and

(

Dst

f

;

Z

1

)

is

a primary ltrator over a boolean lattice.

h

f

i

x

=

l

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x:

Proof.

By the previous proposition for every

y

2

Dst

f

:

y

/

Dst

f

h

f

i

x

,

x

[

f

]

y

, 8

X

2

up

(

Src

f

;

Z

0

)

x

:

X

[

f

]

y

, 8

X

2

up

(

Src

f

;

Z

0

)

x

:

y

/

Dst

f

h

f

i

X:

15.3 Pointfree funcoid as continuation

179