background image

We need to prove it is really a pointfree funcoid.

Proof.

b

/

h

f

i

a

,

b

/

f

a

,

a

/

f

y

b

,

a

/

h

(

f

)

¡

1

i

b

.

Remark 17.136.

h

f

i

= (

f

¡

)

is the Mor-functor

17.1

Mor

(

f ;

¡

)

and we can apply Yoneda lemma

to it. (See any category theory book for denitions of these terms.)

Obvious 17.137.

h

(

g

f

)

i

a

=

g

f

a

for composable morphisms

f

and

g

or a quasi-invertible

category.

17.11.2 General cross-composition product

Denition 17.138.

Let x a quasi-invertible category with with star-morphisms. If

f

is an

indexed family of morphisms from its base category, then the pointfree funcoid

Q

(

C

)

f

(

cross-

composition product

of

f

) from StarMor

(

i

2

dom

f

:

Src

f

i

)

to StarMor

(

i

2

dom

f

:

Dst

f

i

)

is dened

by the formulas (for all star-morphisms

a

and

b

of these forms):

*

Y

(

C

)

f

+

a

=

StarComp

(

a

;

f

)

and

Y

(

C

)

f

!

¡

1

+

b

=

StarComp

(

b

;

f

y

)

:

It is really a pointfree funcoid by the denition of quasi-invertible category with star-morphisms.

Theorem 17.139.

 Q

(

C

)

g

 Q

(

C

)

f

=

Q

i

2

n

(

C

)

(

g

i

f

i

)

for every

n

-indexed families

f

and

g

of composable morphisms of a quasi-invertible category with star-morphisms.

Proof.

DQ

i

2

n

(

C

)

(

g

i

f

i

)

E

a

=

StarComp

(

a

;

i

2

n

:

g

i

f

i

) =

StarComp

(

StarComp

(

a

;

f

);

g

)

and

D Q

(

C

)

g

 Q

(

C

)

f

E

a

=

DQ

(

C

)

g

ED Q

(

C

)

f

E

a

=

StarComp

(

StarComp

(

a

;

f

);

g

)

.

The rest follows from symmetry.

Corollary 17.140.

 Q

(

C

)

f

k

¡

1

:::

 Q

(

C

)

f

0

=

Q

i

2

n

(

C

)

(

f

k

¡

1

:::

f

0

)

for every

n

-indexed

families

f

0

; :::; f

n

¡

1

of composable morphisms of a quasi-invertible category with star-morphisms.

Proof.

By math induction.

17.11.3 Star composition of binary relations

First dene

star composition

for an

n

-ary relation

a

and an

n

-indexed family

f

of binary relations

as an

n

-ary relation complying with the formulas:

Obj

StarComp

(

a

;

f

)

=

fg

n

;

L

2

StarComp

(

a

;

f

)

, 9

y

2

a

8

i

2

n

:

y

i

f

i

L

i

where

is a unique object of the group of small binary relations considered as a category.

Proposition 17.141.

b

/

StarComp

(

a

;

f

)

, 9

x

2

a; y

2

b

8

j

2

n

:

x

j

f

j

y

j

.

Proof.

b

/

StarComp

(

a

;

f

)

, 9

y

: (

y

2

b

^

y

2

StarComp

(

a

;

f

))

, 9

y

: (

y

2

b

^ 9

x

2

a

8

j

2

n

:

x

j

f

j

y

j

)

, 9

x

2

a; y

2

b

8

j

2

n

:

x

j

f

j

y

j

.

Theorem 17.142.

The group of small binary relations considered as a category together with

the set of of all

n

-ary relations (for every small

n

) and the above dened star-composition form a

quasi-invertible category with star-morphisms.

17.1

Also called Hom-functor.

222

Multifuncoids and staroids