background image

3.2 Definition

Definition 4.

I will call a

quasi-invertible category

a partially ordered dagger category such that

it holds

g

f

h

g

h

f

(1)

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

h

g

f

h

. After replacement of variables, this

gives:

f

g

h

g

f

h

As it follows from [1], the category of funcoids and the category of reloids are quasi-invertible

(taking

f

=

f

1

). Moreover by [3] the category of pointfree funcoids between lattices of filters on

boolean lattices are quasi-invertible.

Definition 5.

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

)

):

f

×

(

C

)

g

a

=

g

a

f

and

f

×

(

C

)

g

1

b

=

g

b

f .

The cross-composition product is a pointfree funcoid from Hom

(

Src

f

;

Src

g

)

to Hom

(

Dst

f

;

Dst

g

)

.

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

b

f

×

(

C

)

g

a

a

f

×

(

C

)

g

1

b.

This formula means

b

g

a

f

a

g

b

f

and can be easily proved applying the formula (1)

two times.

Proposition 6.

a

f

×

(

C

)

g

b

a

f

g

b

.

Proof.

From the lemma.

Proposition 7.

a

f

×

(

C

)

g

b

f

a

×

(

C

)

b

g

.

Proof.

f

a

×

(

C

)

b

g

f

a

b

g

a

f

g

b

a

f

×

(

C

)

g

b

.

Theorem 8.

f

×

(

C

)

g

=

f

×

(

C

)

g

.

Proof.

For every funcoids

a

Hom

(

Src

f

;

Src

g

)

and

b

Hom

(

Dst

f

;

Dst

g

)

we have:

f

×

(

C

)

g

b

=

g

b

f

=

g

b

f

=

f

×

(

C

)

g

b

.

f

×

(

C

)

g

a

=

f

×

(

C

)

g

a

=

g

a

f

=

f

×

(

C

)

g

a

.

Theorem 9.

Let

f

,

g

are morphisms of a quasi-invertible category where Dst

f

and Dst

g

are f.o.

on boolean lattices. Then for every f.o.

A

0

F

(

Src

f

)

,

B

0

F

(

Src

g

)

f

×

(

C

)

g

(

A

0

×

FCD

B

0

) =

h

f

iA

0

×

FCD

h

g

iB

0

.

Proof.

For every atom

a

1

×

FCD

b

1

(

a

1

atoms

Dst

f

,

b

1

atoms

Dst

g

) of the lattice of funcoids we have:

a

1

×

FCD

b

1

f

×

(

C

)

g

(

A

0

×

FCD

B

0

)

⇔ A

0

×

FCD

B

0

f

×

(

C

)

g

a

1

×

FCD

b

1

(

A

0

×

FCD

B

0

)

f

g

(

a

1

×

FCD

b

1

)

⇔ h

f

iA

0

×

FCD

B

0

a

1

×

FCD

h

g

i

b

1

⇔ h

f

iA

0

a

1

∧ h

g

i

b

1

B

0

⇔ h

f

iA

0

a

1

h

g

iB

0

b

1

⇔ h

f

iA

0

×

FCD

h

g

iB

0

a

1

×

FCD

b

1

. Thus

f

×

(

C

)

g

(

A

0

×

FCD

B

0

) =

h

f

iA

0

×

FCD

h

g

iB

0

because the lattice

FCD

(

F

(

Dst

f

);

F

(

Dst

g

))

is atomically separable (corollary 64 in [3]).

Proposition 10.

A

0

×

FCD

B

0

f

×

(

C

)

g

A

1

×

FCD

B

1

⇔ A

0

[

f

]

A

1

∧ B

0

[

g

]

B

1

for every

A

0

F

(

Src

f

)

,

A

1

F

(

Dst

f

)

,

B

0

F

(

Src

g

)

,

B

1

F

(

Dst

g

)

.

Proof.

A

0

×

FCD

B

0

f

×

(

C

)

g

A

1

×

FCD

B

1

⇔ A

1

×

FCD

B

1

f

×

(

C

)

g

(

A

0

×

FCD

B

0

)

A

1

×

FCD

B

1

h

f

iA

0

×

FCD

h

g

iB

0

⇔ A

1

h

f

iA

0

∧ B

1

h

g

iB

0

⇔ A

0

[

f

]

A

1

∧ B

0

[

g

]

B

1

.

2

Section 3