background image

CHAPTER 17

Multifuncoids and staroids

17.1. Product of two funcoids

17.1.1. Lemmas.

FiXme

: Previous theorems/propositions shall not be re-

peated as lemmas.

Lemma

1196

.

Let

A

,

B

,

C

be sets,

f

FCD

(

A

;

B

),

g

FCD

(

B

;

C

),

h

FCD

(

A

;

C

). Then

g

f

6

h

g

6

h

f

1

.

Proof.

Proposition

637

.

Lemma

1197

.

Let

A

,

B

,

C

be sets,

f

RLD

(

A

;

B

),

g

RLD

(

B

;

C

),

h

RLD

(

A

;

C

). Then

g

f

6

h

g

6

h

f

1

.

Proof.

Theorem

746

.

17.1.2. Definition.

Definition

1198

.

I will call a

quasi-invertible category

a partially ordered

dagger category such that it holds

g

f

6

h

g

6

h

f

(24)

for every morphisms

f

Mor(

A

;

B

),

g

Mor(

B

;

C

),

h

Mor(

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

.

As it follows from above, the category of funcoids and the category of reloids are

quasi-invertible (taking

f

=

f

1

). Moreover the category of pointfree funcoids be-

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

1119

).

FiXme

:

Say that

Rel

is quasi-invertible.

Exercise

1199

.

Prove that every ordered groupoid is quasi-invertible category

if we define the dagger as the inverse morphism.

Definition

1200

.

The

cross-composition product

of morphisms

f

and

g

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

f

; Src

g

)

Mor(Dst

f

; Dst

g

) defined by the formulas (for every

a

Mor(Src

f

; Src

g

) and

b

Mor(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

the formula (

24

two times.

231