background image

Proof.

We need to prove:

1. StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

i

2

n

:

g

i

f

i

);

2. StarComp

(

m

;

i

2

arity

m

:

id

Obj

m

i

) =

m

;

3.

b

/

StarComp

(

a

;

f

)

,

a

/

StarComp

(

b

;

f

y

)

(the rest is obvious).

Really,

1.

L

2

StarComp

(

a

;

f

)

, 9

y

2

a

8

i

2

n

:

y

i

f

i

L

i

.

Dene the relation

R

(

f

)

by the formula

xR

(

f

)

y

, 8

i

2

n

:

x

i

f

i

y

i

. Obviously

R

(

i

2

n

:

g

i

f

i

) =

R

(

g

)

R

(

f

)

:

L

2

StarComp

(

a

;

f

)

, 9

y

2

a

:

yR

(

f

)

L

.

L

2

StarComp

(

StarComp

(

a

;

f

);

g

)

, 9

p

2

StarComp

(

a

;

f

):

p R

(

g

)

L

, 9

p; y

2

a

:

(

y R

(

f

)

p

^

p R

(

g

)

L

)

, 9

y

2

a

:

y

(

R

(

g

)

R

(

f

))

L

, 9

y

2

a

:

y R

(

i

2

n

:

g

i

f

i

)

L

,

L

2

StarComp

(

a

;

i

2

n

:

g

i

f

i

)

because

p

2

StarComp

(

a

;

f

)

, 9

y

2

a

:

yR

(

f

)

p

.

2. Obvious.
3. It follows from the proposition above.

Obvious 17.143.

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 17.144.

DQ

(

C

)

f

EQ

a

=

Q

i

2

n

h

f

i

i

a

i

for every family

f

=

f

i

2

n

of binary relations

and

a

=

a

i

2

n

where

a

i

is a small set (for each

i

2

n

).

Proof.

L

2

DQ

(

C

)

f

EQ

a

,

L

2

StarComp

(

Q

a

;

f

)

, 9

y

2

Q

a

8

i

2

n

:

y

i

f

i

L

i

, 9

y

2

Q

a

8

i

2

n

:

f

y

i

/

h

f

i

¡

1

if

L

i

g , 8

i

2

n

9

y

2

a

i

:

f

y

/

h

f

i

¡

1

if

L

i

g , 8

i

2

n

:

a

i

/

h

f

i

¡

1

if

L

i

g , 8

i

2

n

:

f

L

i

/

h

f

i

i

a

i

, 8

i

2

n

:

L

i

2 h

f

i

i

a

i

,

L

2

Q

i

2

n

h

f

i

i

a

i

.

17.11.4 Star composition of Rel-morphisms

Dene

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

2

arity

a

:

Dst

f

i

;

arity StarComp

(

a

;

f

) =

arity

a

;

L

2

GR StarComp

(

a

;

f

)

,

L

2

StarComp

(

GR

a

;

GR

f

)

:

(Here I denote GR

(

A

;

B

;

f

) =

f

for every

Rel

-morphism

f

.)

Proposition 17.145.

b

/

StarComp

(

a

;

f

)

, 9

x

2

a; y

2

b

8

j

2

n

:

x

j

f

j

y

j

.

Proof.

From the previous section.

Theorem 17.146.

Relations with above dened compositions form a quasi-invertible category

with star-morphisms.

Proof.

We need to prove:

1. StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

i

2

arity

m

:

g

i

f

i

);

2. StarComp

(

m

;

i

2

arity

m

:

id

Obj

m

i

) =

m

;

3.

b

/

StarComp

(

a

;

f

)

,

a

/

StarComp

(

b

;

f

y

)

(the rest is obvious).

It follows from the previous section.

17.11 Product of an arbitrary number of funcoids

223