background image

Theorem 142.

a

h

Q

(

C

)

f

i

b

⇔ ∀

A

a, B

b, i

n

:

A

i

[

f

i

]

B

i

for anchored relations

a

and

b

.

Proof.

From the lemma.

Proposition 143.

b

pStrd

(

A

)

StarComp

(

a

;

f

)

b

pStrd

(

B

)

StarComp

(

a

;

f

)

for staroids

a

and

b

.

Proof.

Because StarComp

(

a

;

f

)

is a staroid.

Theorem 144.

Anchored relations with above defined compositions form a quasi-invertible cat-

egory with star-morphisms.

Proof.

We need to prove:

1. StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

λi

arity

m

:

g

i

f

i

);

2. StarComp

(

m

;

λi

arity

m

:

id

Obj

m

i

) =

m

;

3.

b

StarComp

(

a

;

f

)

a

StarComp

(

b

;

f

)

(the rest is obvious).

Really,

1.

L

GR StarComp

(

a

;

f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

i

n

:

y

i

[

f

i

]

L

i

.

Define the relation

R

(

f

)

by the formula

xR

(

f

)

y

⇔ ∀

i

n

:

x

i

[

f

i

]

y

i

. Obviously

R

(

λi

n

:

g

i

f

i

) =

R

(

g

)

R

(

f

)

.

L

GR StarComp

(

a

;

f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

:

yR

(

f

)

L

.

L

GR StarComp

(

StarComp

(

a

;

f

);

g

)

⇔ ∃

p

GR StarComp

(

a

;

f

)

Q

i

n

atoms

A

i

:

pR

(

g

)

L

⇔ ∃

p, y

GR

a

Q

i

n

atoms

A

i

: (

yR

(

f

)

p

pR

(

g

)

L

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

:

y

(

R

(

g

)

R

(

f

))

L

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

:

y R

(

λi

n

:

g

i

f

i

)

L

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

i

n

:

y

i

[

g

i

f

i

]

L

i

L

GR StarComp

(

a

;

λi

n

:

g

i

f

i

)

because

p

GR StarComp

(

a

;

f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

:

yR

(

f

)

p

.

2. Obvious.

3. It follows from the lemma above.

Theorem 145.

D

Q

(

C

)

f

E

Q

Strd

a

=

Q

i

n

Strd

h

f

i

i

a

i

for every families

f

=

f

i

n

of pointfree funcoids

and

a

=

a

i

n

where

a

i

Src

f

i

, if Src

f

i

(for every

i

n

) is an atomic lattice.

Proof.

L

D

Q

(

C

)

f

E

Q

Strd

a

L

StarComp

Q

Strd

a

;

f

⇔ ∃

y

Q

i

dom

A

atoms

A

i

i

n

:

(

y

i

[

f

i

]

L

i

y

i

a

i

)

⇔ ∀

i

n

y

atoms

A

i

: (

y

[

f

i

]

L

i

y

a

i

)

⇔ ∀

i

n

:

a

i

[

f

i

]

L

i

⇔ ∀

i

n

:

L

i

h

f

i

i

a

i

L

Q

i

n

Strd

h

f

i

i

a

i

.

Theorem 146.

For every filters

a

0

,

a

1

,

b

0

,

b

1

we have

a

0

×

FCD

b

0

f

×

(

C

)

g

a

1

×

FCD

b

1

a

0

×

RLD

b

0

f

×

(

DP

)

g

a

1

×

RLD

b

1

.

Proof.

a

0

×

RLD

b

0

f

×

(

DP

)

g

a

1

×

RLD

b

1

⇔ ∀

A

0

a

0

, B

0

b

0

, A

1

a

1

, B

1

b

1

:

A

0

×

B

0

f

×

(

DP

)

g

A

1

×

B

1

.

A

0

×

B

0

f

×

(

DP

)

g

A

1

×

B

1

A

0

×

B

0

f

×

(

C

)

g

A

1

×

B

1

A

0

[

f

]

A

1

B

0

[

g

]

B

1

.

Thus it is equivalent to

a

0

[

f

]

a

1

b

0

[

g

]

b

1

that is

a

0

×

FCD

b

0

f

×

(

C

)

g

a

1

×

FCD

b

1

.

(It was used the theorem 142.)

Can the above theorem be generalized for the infinitary case?

Proposition 147.

GR StarComp

(

a

;

λi

n

:

f

i

g

i

) =

GR StarComp

(

a

;

f

)

pFCD

GR StarComp

(

a

;

g

)

if

f

,

g

are pointfree funcoids and every Src

f

i

=

Src

g

i

and Dst

f

i

=

Dst

g

i

are distributive lattices

with least elements, and

a

is a multifuncoid of the form

λi

n

:

Src

f

i

.

Product of an arbitrary number of funcoids

23