background image

3. completary staroids.

Proof.

f

is a finitary pre-staroid

f

is a finitary completary staroid.

f

is a finitary completary staroid

f

is a finitary staroid.

f

is a finitary staroid

f

is a finitary pre-staroid.

Definition 59.

We will denote the set of staroids, pre-staroids, and completary staroids of a form

A

correspondingly as

Strd

(

A

)

,

pStrd

(

A

)

, and

cStrd

(

A

)

.

6 Upgrading and downgrading a set regarding a filtrator

Let fix a filtrator

(

A

;

Z

)

.

Definition 60.

f

=

f

Z

for every

f

P

A

(

downgrading

f

).

Definition 61.

f

=

{

L

A

|

up

L

f

}

for every

f

P

Z

(

upgrading

f

).

Obvious 62.

a

f

up

a

f

for every

f

P

Z

and

a

A

.

Proposition 63.

 ⇈

f

=

f

if

f

is an upper set.

Proof.

f

=

f

Z

=

{

L

Z

|

up

L

f

}

=

{

L

Z

|

up

L

f

}

=

f

P

Z

=

f

.

6.1 Upgrading and downgrading staroids

Let fix a family

(

A

;

Z

)

of filtrators.

For a graph

f

of a staroid define

f

and

f

taking the filtrator of

(

Q

A

;

Q

Z

)

.

For a staroid

f

define:

form

f

=

Z

and GR

f

=

GR

f

;

form

f

=

A

and

GR

f

=

GR

f .

Proposition 64.

(

val

f

))

i

L

= (

val

f

)

i

L

Z

i

for every

L

Q

Z

|

(

arity

f

)

\{

i

}

.

Proof.

(

val

f

))

i

L

=

{

X

(

form

f

)

i

|

L

∪ {

(

i

;

X

)

} ∈

GR

f

Q

Z

}

=

{

X

Z

i

|

L

∪ {

(

i

;

X

)

} ∈

GR

f

}

= (

val

f

)

i

L

Z

i

.

Proposition 65.

Let

(

A

i

;

Z

i

)

are finitely join-closed filtrators with both the base and the core

being join-semilattices. If

f

is a staroid of the form

A

, then

f

is a staroid of the form

Z

.

Proof.

Let

f

is a a staroid.

We need to prove that

(

val

f

)

i

L

is a free star. It follows from the last proposition and the

fact that it is join-closed.

Proposition 66.

Q

Strd

a

=

Q

Strd

a

if each

a

i

A

i

(for

i

n

where

n

is some index set) where

A

i

is a separable poset with least element.

Proof.

Q

Strd

a

=

L

Q

A

|

L

Q

Strd

a

 

=

{

L

Q

A

| ∀

K

L

:

K

a

}

=

{

L

Q

A

|

L

a

}

=

Q

Strd

a

(taken into account that

Q

A

is a separable poset).

6.2 Displacement

Definition 67.

Let

f

is an indexed family of pointfree funcoids. The

displacement

of the pre-

staroid

p

A

=

pStrd

(

λi

dom

f

:

FCD

(

Src

f

i

;

Src

g

i

))

8

Section 6