background image

7.10. FUNCOIDAL PRODUCT OF FILTERS

166

Proof.

(

A

0

×

FCD

B

0

)

u

(

A

1

×

FCD

B

1

) =

d

{A ×

FCD

B

0

,

A

1

×

FCD

B

1

}

what is by

the last theorem equal to (

A

0

u A

1

)

×

FCD

(

B

0

u B

1

).

Theorem

893

.

If

A

,

B

are sets and

A ∈

F

(

A

) then

FCD

is a complete

homomorphism from the lattice

F

(

B

) to the lattice

FCD

(

A, B

), if also

A 6

=

F

(

A

)

then it is an order embedding.

Proof.

Let

S

PF

(

B

),

X

T

A

,

x

atoms

F

(

A

)

.

D

l

FCD

S

E

X

=

l

B∈

S

A ×

FCD

B

X

=

(

d

S

if

X

A

F

(

B

)

if

X /

A

=

D

A ×

FCD

l

S

E

X

;

D

l

FCD

S

E

x

=

l

B∈

S

A ×

FCD

B

x

=

(

d

S

if

x

6 A

F

(

B

)

if

x

 A

.

Thus

d

FCD

S

=

A ×

FCD

d

S

and

d

FCD

S

=

A ×

FCD

d

S

.

If

A 6

=

then obviously

A ×

FCD

X v A ×

FCD

Y ⇔ X v Y

.

The following proposition states that cutting a rectangle of atomic width from

a funcoid always produces a rectangular (representable as a funcoidal product of

filters) funcoid (of atomic width).

Proposition

894

.

If

f

is a funcoid and

a

is an atomic filter on Src

f

then

f

|

a

=

a

×

FCD

h

f

i

a.

Proof.

Let

X ∈

F

(Src

f

).

X 6

a

⇒ h

f

|

a

iX

=

h

f

i

a,

a

⇒ h

f

|

a

iX

=

F

(Dst

f

)

.

Lemma

895

.

λ

B ∈

F

(

B

) :

>

F

×

FCD

B

is an upper adjoint of

λf

FCD

(

A, B

) :

im

f

(for every sets

A

,

B

).

Proof.

We need to prove im

f

v B ⇔

f

v > ×

FCD

B

what is obvious.

Corollary

896

.

Image and domain of funcoids preserve joins.

Proof.

By properties of Galois connections and duality.

Proposition

897

.

f

v A ×

FCD

B ⇔

dom

f

v A ∧

im

f

v B

for every funcoid

f

and filters

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Proof.

f

v A ×

FCD

B ⇒

dom

f

v A

because dom(

A ×

FCD

B

)

v A

.

Let now dom

f

v A ∧

im

f

v B

. Then

h

f

iX 6

=

⊥ ⇒ X 6 A

that is

f

v

A ×

FCD

>

. Similarly

f

v > ×

FCD

B

. Thus

f

v A ×

FCD

B

.