 17.5. PRINCIPAL STAROIDS

241

Definition

1257

.

We will denote the set of staroids, prestaroids, and comple-

tary staroids of a form

A

correspondingly as

Strd

(

A

),

pStrd

(

A

), and

cStrd

(

A

).

17.4. Upgrading and downgrading a set regarding a filtrator

Let fix a filtrator (

A

;

Z

).

Definition

1258

.

f

=

f

Z

for every

f

P

A

(

f

).

Definition

1259

.

f

=

n

L

A

up

L

f

o

for every

f

P

Z

(

f

).

Obvious

1260

.

a

f

up

a

f

for every

f

P

Z

and

a

A

.

Proposition

1261

.

f

=

f

if

f

is an upper set for every

f

P

Z

.

Proof.

f

=

f

Z

=

n

L

Z

up

L

f

o

=

n

L

Z

L

f

o

=

f

Z

=

f

.

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:

FiXme

: Define for all anchored relations.

form

f

=

Z

and GR

f

=

GR

f

;

form

f

=

A

and GR

f

=

GR

f.

Proposition

1262

.

(val

f

)

i

L

= (val

f

)

i

L

Z

i

for every

L

Q

Z

|

(arity

f

)

\{

i

}

.

Proof.

(val

f

)

i

L

=

X

Z

i

L

∪{

(

i

;

X

)

}∈

GR

f

Q

Z

=

n

X

Z

i

L

∪{

(

i

;

X

)

}∈

GR

f

o

=

(val

f

)

i

L

Z

i

.

Proposition

1263

.

Let (

A

i

;

Z

i

) be 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

be 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 finitely join-closed.

17.5. Principal staroids

Definition

1264

.

The

staroid generated

by an anchored relation

F

is the

staroid

f

=

Strd

F

on powersets such that

↑ ◦

L

GR

f

Q

L

6

F

and (form

f

)

i

=

P

(form

F

)

i

for every

L

Q

i

arity

f

P

(form

F

)

i

.

Remark

1265

.

Below we will prove that staroid generated by an anchored

relation is a staroid and moreover a completary staroid.

Definition

1266

.

A

principal staroid

is a staroid generated by some anchored

relation.

Proposition

1267

.

Every principal staroid is a completary staroid.

Proof.

That

L /

f

if

L

i

=

(form

f

)

i

for some

i

arity

f

is obvious. It

remains to prove

Y

(

L

0

t

L

1

)

6

F

⇔ ∃

c

∈ {

0

,

1

}

arity

f

:

Y

i

n

L

c

(

i

)

i

6

F.