21.2. DEFINITION OF STAROIDS

319

Theorem

1628

.

Let

f

,

g

be pointfree funcoids between filters on boolean

lattices. Then for every filters

A

0

F

(Src

f

),

B

0

F

(Src

g

)

D

f

×

(

C

)

g

E

(

A

0

×

FCD

B

0

) =

h

f

iA

0

×

FCD

h

g

iB

0

.

Proof.

For every atom

a

1

×

FCD

b

1

(

a

1

atoms

Dst

f

,

b

1

atoms

Dst

g

) (see

theorem

1572

of the lattice of funcoids we have:

a

1

×

FCD

b

1

6

D

f

×

(

C

)

g

E

(

A

0

×

FCD

B

0

)

A

0

×

FCD

B

0

h

f

×

(

C

)

g

i

a

1

×

FCD

b

1

(

A

0

×

FCD

B

0

)

f

1

6

g

1

(

a

1

×

FCD

b

1

)

h

f

iA

0

×

FCD

B

0

6

a

1

×

FCD

g

1

b

1

h

f

iA

0

6

a

1

g

1

b

1

6 B

0

h

f

iA

0

6

a

1

∧ h

g

iB

0

6

b

1

h

f

iA

0

×

FCD

h

g

iB

0

6

a

1

×

FCD

b

1

.

Thus

f

×

(

C

)

g

(

A

0

×

FCD

B

0

) =

h

f

iA

0

×

FCD

h

g

iB

0

because the lattice

pFCD

(

F

(Dst

f

)

,

F

(Dst

g

)) is atomically separable (corollary

1563

).

Corollary

1629

.

A

0

×

FCD

B

0

f

×

(

C

)

g

A

1

×

FCD

B

1

⇔ A

0

[

f

]

A

1

∧ B

0

[

g

]

B

1

for every

A

0

F

(Src

f

),

A

1

F

(Dst

f

),

B

0

F

(Src

g

),

B

1

F

(Dst

g

) where

Src

f

, Dst

f

, Src

g

, Dst

g

are boolean lattices.

Proof.

A

0

×

FCD

B

0

h

f

×

(

C

)

g

i

A

1

×

FCD

B

1

A

1

×

FCD

B

1

6

D

f

×

(

C

)

g

E

A

0

×

FCD

B

0

A

1

×

FCD

B

1

6 h

f

iA

0

×

FCD

h

g

iB

0

A

1

6 h

f

iA

0

∧ B

1

6 h

g

iB

0

A

0

[

f

]

A

1

∧ B

0

[

g

]

B

1

.

21.2. Definition of staroids

It follows from the above theorem

831

that funcoids are essentially the same as

relations

δ

between sets

A

and

B

, such that

Y

P

B

X

P

A

:

XδY

and

X

P

A

Y

P

B

:

XδY

are

free stars. This inspires the below definition of staroids (switching from two sets

X

and

Y

to a (potentially infinite) family of posets).

Whilst I have (mostly) thoroughly studied basic properties of funcoids,

staroids

(defined below) are yet much a mystery. For example, we do not know whether the

set of staroids on powersets is atomic.

Let

n

be a set. As an example,

n

may be an ordinal,

n

may be a natural

number, considered as a set by the formula

n

=

{

0

, . . . , n

1

}

. Let

A

=

A

i

n

be a

family of posets indexed by the set

n

.

Definition

1630

.

I will call an

anchored relation

a pair

f

= (form

f,

GR

f

) of

a family form(

f

) of relational structures indexed by some index set and a relation

GR(

f

)

P

Q

form(

f

). I call GR(

f

) the

graph

of the anchored relation

f

. I denote

Anch(

A

) the set of anchored relations of the form

A

.