21.19. IDENTITY STAROIDS AND MULTIFUNCOIDS

375

Remark

1900

.

v

on the diagram means inequality which can become strict

for some

A

and

n

.

21.19.7. Identity staroids represented as meets and joins.

Proposition

1901

.

id

Strd

a

[

n

]

=

d

Anch

A

up

a

id

A

[

n

]

=

d

Strd

A

up

a

id

A

[

n

]

for every filter

a

on a powerset.

Proof.

Since id

Strd

a

[

n

]

is a staroid (proposition

1872

), it’s enough to prove that

id

Strd

a

[

n

]

is the greatest lower bound of

n

Strd

id

A

[

n

]

A

up

a

o

.

That id

Strd

a

[

n

]

v↑

Strd

id

A

[

n

]

for every

A

up

a

is obvious.

Let

f

v↑

Strd

id

A

[

n

]

for every

A

up

a

.

L

GR

f

⇒ ∀

A

up

a

:

L

GR

Strd

id

A

[

n

]

A

up

a

:

Y

L

6

id

A

[

n

]

⇔ ∀

A

up

a

:

Z

l

i

n

L

i

6

A

A

up

a

:

A

l

i

n

L

i

6

A

A

l

i

n

L

i

6

a

L

GR id

Strd

a

[

n

]

.

Thus

f

v

id

Strd

a

[

n

]

.

Proposition

1902

.

ID

Strd

A

[

n

]

=

d

a

atoms

A

ID

Strd

a

[

n

]

=

d

a

atoms

A

a

n

Strd

where the

join may be taken on every of the following posets: anchored relations, staroids,

completary staroids, provided that

A

is a filter on a set.

Proof.

ID

Strd

A

[

n

]

is a completary staroid (proposition

1873

). Thus, it’s enough

to prove that ID

Strd

A

[

n

]

is the lowest upper bound of

ID

Strd

a

[

n

]

a

atoms

A

(also use the fact

that ID

Strd

a

[

n

]

=

a

n

Strd

).

ID

Strd

A

[

n

]

w

ID

Strd

a

[

n

]

for every

a

atoms

A

is obvious.

Let

f

w

ID

Strd

a

[

n

]

for every

a

atoms

A

. Then

L

GR ID

Strd

a

[

n

]

:

L

GR

f

that is

L

form

f

:

MEET

L

i

i

n

∪ {

a

}

L

GR

f

.

But

a

atoms

A

: MEET

L

i

i

n

∪ {

a

}

⇔ ∃

a

atoms

A

:

A

l

i

n

L

i

6

a

A

l

i

n

L

i

6 A ⇔

L

GR ID

Strd

A

[

n

]

.

So

L

GR ID

Strd

A

[

n

]

L

GR

f

. Thus

f

w

ID

Strd

A

[

n

]

.

Proposition

1903

.

id

Strd

A

[

n

]

=

d

a

atoms

A

id

Strd

a

[

n

]

where the meet may be taken

on every of the following posets: anchored relations, staroids, provided that

A

is a

filter on a set.

Proof.

Since id

Strd

A

[

n

]

is a staroid (proposition

1872

), it’s enough to prove the

result for join on anchored relations.

id

Strd

A

[

n

]

w

id

Strd

a

[

n

]

for every

a

atoms

A

is obvious.