background image

21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

342

Conjecture

1737

.

b

6

Anch(

A

)

StarComp(

a, f

)

⇔ ∀

A

GR

a, B

GR

b, i

n

:

A

i

[

f

i

]

B

i

for anchored relations

a

and

b

on powersets.

It’s consequence:

Conjecture

1738

.

b

6

Anch(

A

)

StarComp(

a, f

)

a

6

Anch(

A

)

StarComp(

b, f

)

for anchored relations

a

and

b

on powersets.

Conjecture

1739

.

b

6

Strd

(

A

)

StarComp(

a, f

)

a

6

Strd

(

A

)

StarComp(

b, f

)

for pre-staroids

a

and

b

on powersets.

Proposition

1740

.

Anchored relations with objects being posets with above

defined star-morphisms is a category 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

: 1

Obj

m

i

) =

m

.

(the rest is obvious). Really,

L

GR StarComp(StarComp(

m, f

)

, g

)

(

λi

arity

m

:

g

1

i

L

i

)

GR StarComp(

m, f

)

(

λi

n

:

f

1

i

(

λj

n

:

g

1

j

L

j

)

i

)

GR

m

(

λi

arity

m

:

h

f

1

i

i

g

1

i

L

i

)

GR

m

(

λi

arity

m

:

h

(

g

i

f

i

)

1

i

L

i

)

GR

m

L

GR StarComp(

m, λi

arity

m

:

g

i

f

i

);

and

L

GR StarComp(

m, λi

arity

m

: 1

Obj

m

i

)

(

λi

n

:

1

Obj

m

i

L

i

)

GR

m

(

λi

arity

m

:

1

Obj

m

i

L

i

)

GR

m

(

λi

arity

m

:

L

i

)

GR

m

L

GR

m.

Conjecture

1741

.

StarComp(

a

t

b, f

) = StarComp(

a, f

)

t

StarComp(

b, f

)

for anchored relations

a

,

b

of a form

A

, where every

A

i

is a distributive lattice, and

an indexed family

f

of pointfree funcoids with Src

f

i

=

A

i

.

21.10.6. Cross-composition product of funcoids through atoms.

Let

a

be a an anchored relation of the form

A

and dom

A

=

n

.

Let every

f

i

(for all

i

n

) be a pointfree funcoid with Src

f

i

=

A

i

.

The

atomary star-composition

of

a

with

f

is an anchored relation of the form

λi

dom

A

: Dst

f

i

defined by the formula

L

GR StarComp

(

a

)

(

a, f

)

⇔ ∃

y

GR

a

Y

i

n

atoms

A

i

i

n

:

y

i

[

f

i

]

L

i

.

Theorem

1742

.

Let Dst

f

i

be a starrish join-semilattice for every

i

n

.

1

. If

a

is a prestaroid then StarComp

(

a

)

(

a, f

) is a staroid.

2

. If

a

is a completary staroid and then StarComp

(

a

)

(

a, f

) is a completary

staroid.

Proof.