background image

Proof.

Using the fact that

f

pStrd

(

form

f

)

Q

Strd

a

=

StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

is a

completary staroid (theorem 140).

Theorem 154.

Q

Strd

a

pStrd

Q

Strd

b

Q

Strd

a

cStrd

Q

Strd

b

b

Q

Strd

a

a

Q

Strd

b

a

b

for every indexed families

a

and

b

of filters on boolean algebras.

Proof.

By corollary 66 we have

Q

Strd

b

=

f

for some

f

. Thus as our filtrator is with separable

core we can apply the theorem 152 and its corollary. So

Q

Strd

a

cStrd

Q

Strd

b

a

Q

Strd

b

and

Q

Strd

a

cStrd

Q

Strd

b

a

Q

Strd

b

. Similarly

Q

Strd

a

cStrd

Q

Strd

b

b

Q

Strd

a

. This by the

definition of staroidal product is equivalent to

a

b

. We are done.

13 Multireloids

Definition 155.

I will call a

multireloid

of the form

A

=

A

i

n

, where every each

A

i

is a set, a pair

(

f

;

A

)

where

f

is a filter on the set

Q

A

.

Definition 156.

I will denote Obj

(

f

;

A

) =

A

and GR

(

f

;

A

) =

f

for every multireloid

(

f

;

A

)

.

I will denote

RLD

(

A

)

the set of multireloids of the form

A

.

The multireloid

RLD

(

A

)

F

for a binary relation

F

is defined by the formulas:

Obj

RLD

(

A

)

F

=

A

and GR

RLD

(

A

)

F

=

Q

A

GR

F .

Let

a

is a multireloid of the form

A

and dom

A

=

n

.

Let every

f

i

is a reloid with Src

f

i

=

A

i

.

The star-composition of

a

with

f

is a multireloid of the form

λi

dom

A

:

Src

f

i

defined by the

formulas:

arity StarComp

(

a

;

f

) =

n

;

GR StarComp

(

a

;

f

) =

l

(

RLD

(

A

)

StarComp

(

A

;

F

)

| ∀

A

a, F

Y

i

n

f

i

)

;

Obj

m

StarComp

(

a

;

f

) =

λi

n

:

Dst

f

i

.

Theorem 157.

Multireloids with above defined compositions form a quasi-invertible category

with star-morphisms.

Proof.

We need to prove:

1. StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

λi

arity

m

:

g

i

f

i

);

2. StarComp

(

m

;

λi

arity

m

:

id

Obj

m

i

) =

m

;

3.

b

StarComp

(

a

;

f

)

a

StarComp

(

b

;

f

)

(the rest is obvious).

Really,

1. StarComp

(

StarComp

(

A

;

f

);

g

) =

d

RLD

(

A

)

StarComp

(

B

;

G

)

| ∀

B

StarComp

(

A

;

f

)

,

G

Q

i

n

g

i

 

=

d

RLD

(

A

)

StarComp

(

StarComp

(

A

;

F

);

G

)

| ∀

A

a, F

Q

i

n

f

i

,

G

Q

i

n

g

i

 

=

d

RLD

(

A

)

StarComp

(

A

;

G

F

)

| ∀

A

a, F

Q

i

n

f

i

, G

Q

i

n

g

i

 

=

d

RLD

(

A

)

StarComp

(

A

;

H

)

| ∀

A

a, H

Q

i

n

λi

n

:

g

i

f

i

 

=

StarComp

(

a

;

λi

n

:

g

i

f

i

)

(used properties of generalized filter bases)

[TODO: More detailed proof.]

2. StarComp

(

m

;

λi

arity

m

:

id

Obj

m

i

) =

d

RLD

(

A

)

StarComp

(

A

;

id

X

)

| ∀

A

m, X

S

i

n

P

Obj

m

i

 

=

d

RLD

(

A

)

A

| ∀

A

a

 

=

m

.

3. Using properties of generalized filter bases,

Multireloids

25