background image

17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

258

2

Obvious.

3

It follows from the proposition above.

Obvious

1340

.

StarComp(

a

b

;

f

) = StarComp(

a

;

f

)

StarComp(

b

;

f

) for

n

-ary relations

a

,

b

and an

n

-indexed family

f

of binary relations.

Theorem

1341

.

D

Q

(

C

)

f

E

Q

a

=

Q

i

n

h

f

i

i

a

i

for every family

f

=

f

i

n

of

binary relations and

a

=

a

i

n

where

a

i

is a small set (for each

i

n

).

Proof.

L

*

(

C

)

Y

f

+

Y

a

L

StarComp

Y

a

;

f

y

Y

a

i

n

:

y

i

f

i

L

i

y

Y

a

i

n

:

{

y

i

} 6

f

1

i

{

L

i

} ⇔

i

n

y

a

i

:

{

y

} 6

f

1

i

{

L

i

} ⇔

i

n

:

a

i

6

f

1

i

{

L

i

} ⇔

i

n

:

{

L

i

} 6 h

f

i

i

a

i

i

n

:

L

i

∈ h

f

i

i

a

i

L

Y

i

n

h

f

i

i

a

i

.

17.11.4. Star composition of Rel-morphisms.

Define

star composition

for

an

n

-ary anchored relation

a

and an

n

-indexed family

f

of

Rel

-morphisms as an

n

-ary anchored relation complying with the formulas:

Obj

StarComp(

a

;

f

)

=

λi

arity

a

: Dst

f

i

;

arity StarComp(

a

;

f

) = arity

a

;

L

GR StarComp(

a

;

f

)

L

StarComp(GR

a

; GR

f

)

.

(Here I denote

GR

(

A

;

B

;

f

) =

f

for every

Rel

-morphism

f

.)

Proposition

1342

.

b

6

StarComp(

a

;

f

)

⇔ ∃

x

a, y

b

j

n

:

x

j

f

j

y

j

.

Proof.

From the previous section.

Theorem

1343

.

Relations with above defined compositions form a quasi-

invertible 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

: id

Obj

m

i

) =

m

;

3

.

b

6

StarComp(

a

;

f

)

a

6

StarComp(

b

;

f

)

(the rest is obvious).

It follows from the previous section.

Proposition

1344

.

StarComp(

a

t

b

;

f

) = StarComp(

a

;

f

)

t

StarComp(

b

;

f

)

for an

n

-ary anchored relations

a

,

b

and an

n

-indexed family

f

of

Rel

-morphisms.

Proof.

It follows from the previous section.