9 Infinite product of elements and filters

Definition 90.

Let

A

i

is a family of elements of a family

A

i

of posets. The

staroidal product

Q

Strd

(

A

)

A

i

is defined by the formula (for every

L

Q

A

)

form

Y

Strd

(

A

)

A

=

A

and

L

GR

Y

Strd

(

A

)

A

⇔ ∀

i

dom

A

:

A

i

L

i

.

Theorem 91.

Staroidal product is a completary staroid (if our posets are distributive lattices).

Proof.

We need to prove

i

dom

A

:

A

i

(

L

0

i

L

1

i

)

⇔ ∃

c

∈ {

0

,

1

}

n

i

dom

A

:

A

i

L

c

(

i

)

i.

Really,

i

dom

A

:

A

i

(

L

0

i

L

1

i

)

⇔ ∀

i

dom

A

: (

A

i

L

0

i

A

i

L

1

i

)

⇔ ∃

c

∈ {

0

,

1

}

dom

A

i

dom

A

:

A

i

L

c

(

i

)

i

.

Definition 92.

Let

A

is an indexed family of posets with least elements. Then

funcoidal product

is defined by the formulas:

form

Y

FCD

(

A

)

A

=

A

and

GR

Y

FCD

(

A

)

A

!

k

L

=

A

k

if

i

(

dom

A

)

\ {

k

}

:

A

i

L

i

0

otherwise

.

Proposition 93.

Q

Strd

(

A

)

A

=

h

Q

FCD

(

A

)

A

i

.

Proof.

L

GR

Q

Strd

(

A

)

A

⇔ ∀

i

dom

A

:

A

i

L

i

⇔ ∀

i

(

dom

A

)

\ {

k

}

:

A

i

L

i

L

k

A

k

A

k

Q

FCD

(

A

)

A

k

L

L

GR

h

Q

FCD

(

A

)

A

i

.

Corollary 94.

Funcoidal product is a completary multifuncoid.

Proof.

It is enough to prove that funcoidal product is a pre-multifuncoid. Really,

L

i

GR

Y

FCD

(

A

)

A

!

i

L

|

(

dom

A

)

\{

i

}

⇔∀

i

dom

A

:

A

i

L

i

L

j

GR

Y

FCD

(

A

)

A

!

j

L

|

(

dom

A

)

\{

j

}

.

Theorem 95.

If our filtrator

(

Q

A

;

Q

Z

)

is with separable core and

A

Q

Z

, then

Q

Strd

(

Z

)

A

=

Q

Strd

(

A

)

A

.

Proof.

GR

Q

Strd

(

Z

)

A

=

n

L

A

|

L

Q

Strd

(

Z

)

A

o

=

{

L

A

| ∀

K

L, i

dom

A

:

A

i

K

i

}

=

{

L

A

| ∀

i

dom

A

, K

L

i

:

A

i

K

}

=

{

L

A

| ∀

i

dom

A

:

A

i

L

i

}

=

GR

Q

Strd

(

A

)

A

.

Proposition 96.

Let

(

Q

A

;

Q

Z

)

is a meet-closed filtrator. Then

Q

Strd

(

A

)

A

=

Q

Strd

(

Z

)

A

.

Proof.

GR

Q

Strd

(

A

)

A

=

GR

Q

Strd

(

A

)

A

=

{

L

Q

A

| ∀

i

dom

A

:

A

i

L

i

}

=

{

L

Q

A

| ∀

i

dom

A

:

A

i

L

i

} ∩

Q

Z

=

{

L

Q

Z

| ∀

i

dom

A

:

A

i

L

i

}

=

GR

Q

Strd

(

Z

)

A

.

Theorem 97.

Let

F

is a family of sets of filters on distributive lattices with least elements. Let

a

Q

F

,

S

P

Q

F

is a generalized filter base,

d

S

=

a

. Then

Y

Strd

(

F

)

a

=

l

(

Y

Strd

(

F

)

A

|

A

S

)

.

Proof.

That

Q

Strd

(

F

)

a

is a lower bound for

n

Q

Strd

(

F

)

A

|

A

S

o

is obvious.

12

Section 9