background image

21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

344

b

6

Anch(

B

)

StarComp

(

a

)

(

a, f

)

x

Anch(

B

)

\ {⊥}

: (

x

v

b

x

v

StarComp

(

a

)

(

a, f

))

x

Anch(

B

)

\ {⊥}

: (

x

v

b

∧ ∀

B

GR

x

:

B

GR StarComp

(

a

)

(

a, f

))

x

Anch(

B

)

\ {⊥}

:

 

x

v

b

∧ ∀

B

GR

x

A

Y

i

dom

B

atoms

B

i

: (

i

n

:

A

i

[

f

i

]

B

i

A

GR

a

)

!

x

Anch(

B

)

\ {⊥}

: (

x

v

b

∧ ∀

B

GR

x, A

GR

a, i

n

:

A

i

[

f

i

]

B

i

)

x

Anch(

B

) : (

x

v

b

∧ ∀

B

GR

x, A

GR

a, i

n

:

A

i

[

f

i

]

B

i

)

B

GR

b, A

GR

a, i

n

:

A

i

[

f

i

]

B

i

.

Definition

1744

.

I will denote the cross-composition product for the star-

composition StarComp

(

a

)

as

Q

(

a

)

.

Theorem

1745

.

a

h

Q

(

a

)

f

i

b

⇔ ∀

A

GR

a, B

GR

b, i

n

:

A

i

[

f

i

]

B

i

for

anchored relations

a

and

b

, provided that Src

f

i

and Dst

f

i

are atomic posets.

Proof.

From the lemma.

Conjecture

1746

.

b

6

Strd

(

B

)

StarComp(

a, f

)

a

6

Strd

(

A

)

StarComp(

b, f

)

for staroids

a

and

b

on indexed families

A

and

B

of filters on powersets.

Theorem

1747

.

Anchored relations with objects being atomic posets

and above defined compositions form a quasi-invertible precategory with star-

morphisms.

Remark

1748

.

It seems that this precategory with star-morphisms isn’t a

category with star-morphisms.

Proof.

We need to prove:

1

. StarComp

(

a

)

(StarComp

(

a

)

(

m, f

)

, g

) = StarComp

(

a

)

(

m, λi

arity

m

:

g

i

f

i

);

2

.

b

6

StarComp

(

a

)

(

a, f

)

a

6

StarComp

(

a

)

(

b, f

)

(the rest is obvious).

Really, let

a

be a star morphism and

A

i

= (Obj

a

)

i

for every

i

arity

a

;

1

.

L

GR StarComp

(

a

)

(

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

x R

(

f

)

y

⇔ ∀

i

n

:

x

i

[

f

i

]

y

i

.

Obviously

R

(

λi

n

:

g

i

f

i

) =

R

(

g

)

R

(

f

)

.