background image

CHAPTER 21

Multifuncoids and staroids

21.1. Product of two funcoids

21.1.1. Definition.

Definition

1622

.

I will call a

quasi-invertible category

a partially ordered

dagger category such that it holds

g

f

6

h

g

6

h

f

(32)

for every morphisms

f

Hom(

A, B

),

g

Hom(

B, C

),

h

Hom(

A, C

), where

A

,

B

,

C

are objects of this category.

Inverting this formula, we get

f

g

6

h

g

6

f

h

. After replacement of

variables, this gives:

f

g

6

h

g

6

f

h

.

Exercise

1623

.

Prove that every ordered groupoid is quasi-invertible category

if we define the dagger as the inverse morphism.

As it follows from above, the categories

Rel

of binary relations (proposi-

tion

283

),

FCD

of funcoids (theorem

882

and

RLD

of reloids (theorem

1009

are

quasi-invertible (taking

f

=

f

1

). Moreover the category of pointfree funcoids

between lattices of filters on boolean lattices is quasi-invertible (theorem

1554

).

Definition

1624

.

The

cross-composition product

of morphisms

f

and

g

of a quasi-invertible category is the pointfree funcoid Hom(Src

f,

Src

g

)

Hom(Dst

f,

Dst

g

) defined by the formulas (for every

a

Hom(Src

f,

Src

g

) and

b

Hom(Dst

f,

Dst

g

)):

D

f

×

(

C

)

g

E

a

=

g

a

f

and

D

(

f

×

(

C

)

g

)

1

E

b

=

g

b

f.

We need to prove that it is really a pointfree funcoid that is that

b

6

D

f

×

(

C

)

g

E

a

a

6

D

(

f

×

(

C

)

g

)

1

E

b.

This formula means

b

6

g

a

f

a

6

g

b

f

and can be easily proved applying

formula (

32

twice.

Proposition

1625

.

a

f

×

(

C

)

g

b

a

f

6

g

b

.

Proof.

From the definition.

Proposition

1626

.

a

f

×

(

C

)

g

b

f

a

×

(

C

)

b

g

.

Proof.

f

a

×

(

C

)

b

g

f

a

6

b

g

a

f

6

g

b

a

f

×

(

C

)

g

b

.

Theorem

1627

.

(

f

×

(

C

)

g

)

1

=

f

×

(

C

)

g

.

Proof.

For every morphisms

a

Hom(Src

f,

Src

g

) and

b

Hom(Dst

f,

Dst

g

)

we have:

(

f

×

(

C

)

g

)

1

b

=

g

b

f

=

f

×

(

C

)

g

b

.

((

f

×

(

C

)

g

)

1

)

1

a

=

f

×

(

C

)

g

a

=

g

a

f

=

(

f

×

(

C

)

g

)

1

a

.

318