background image

Proof.

(

val

f

)

i

L

=

f

X

2

Z

i

j

L

[ f

(

i

;

X

)

g 2

GR

f

\

Q

Z

g

=

f

X

2

Z

i

j

L

[ f

(

i

;

X

)

g 2

GR

f

g

=

(

val

f

)

i

L

\

Z

i

.

Proposition 17.65.

Let

(

A

i

;

Z

i

)

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

17.5 Principal staroids

Denition 17.66.

The

staroid generated

by an anchored relation

F

is the staroid

f

=

"

Strd

F

on powersets such that

L

2

GR

f

,

Q

L

/

F

and

(

form

f

)

i

=

P

(

form

F

)

i

for every

L

2

Q

i

2

arity

f

P

(

form

F

)

i

.

Remark 17.67.

Below we will prove that staroid generated by an anchored relation is a staroid

and moreover a completary staroid.

Denition 17.68.

A

principal staroid

is a staroid generated by some anchored relation.

Proposition 17.69.

Every principal staroid is a completary staroid.

Proof.

That

L

2

/

f

if

L

i

= 0

(

form

f

)

i

for some

i

2

arity

f

is obvious. It remains to prove

Y

(

L

0

t

L

1

)

/

F

, 9

c

2 f

0

;

1

g

arity

f

:

Y

i

2

n

L

c

(

i

)

i

/

F :

Really

Q

(

L

0

t

L

1

)

/

F

, 9

x

2

Q

(

L

0

t

L

1

):

x

2

F

, 9

x

2

Q

i

2

arity

f

(

form

f

)

i

8

i

2

arity

f

:

(

x

i

2

L

0

i

[

L

1

i

^

x

2

F

)

, 9

x

2

Q

i

2

arity

f

(

form

f

)

i

8

i

2

arity

f

: ((

x

i

2

L

0

i

_

x

i

2

L

1

i

)

^

x

2

F

)

,

9

x

2

Q

i

2

arity

f

(

form

f

)

i

¡

9

c

2 f

0

;

1

g

arity

f

:

x

2

Q

i

2

arity fn

L

c

(

i

)

i

^

x

2

F

, 9

c

2 f

0

;

1

g

arity

f

:

Q

i

2

arity

f

L

c

(

i

)

i

/

F

.

Denition 17.70.

The

upgraded staroid generated

by an anchored relation

F

is the staroid

"

Strd

F

.

Proposition 17.71.

"

Strd

F

=

"

Strd

F

.

Proof.

Because GR

"

Strd

F

is an upper set.

Conjecture 17.72.

Every upgraded principal staroid is a completary staroid.

Conjecture 17.73.

Filtrators of staroids on powersets are join-closed.

17.6 Multifuncoids

Denition 17.74.

Let

(

A

i

;

Z

i

)

(where

i

2

n

for an index set

n

) be an indexed family of ltrators.

I call a

premultifuncoid sketch

f

of the form

(

A

i

;

Z

i

)

the

n

-indexed family

of functions where

for every

i

2

n

i

:

Y

Z

j

(

dom

A

)

nf

i

g

!

A

i

:

I denote

h

f

i

=

.

Denition 17.75.

A premultifuncoid sketch

on powersets

is a premultifuncoid sketch such that

every

(

A

i

;

Z

i

)

is the primary ltrator of lters on a powerset.

17.6 Multifuncoids

211