 7.4. ANOTHER WAY TO REPRESENT FUNCOIDS AS BINARY RELATIONS

152

Proof.

X

[

f

]

l

S

l

S

u h

f

iX 6

=

⊥ ⇔

l

hh

f

iX ui

S

6

=

⊥ ⇔

(by properties of generalized filter bases)

∃Y ∈ hh

f

iX ui

S

:

Y 6

=

⊥ ⇔ ∃Y ∈

S

:

h

f

iX u Y 6

=

⊥ ⇔ ∃Y ∈

S

:

X

[

f

]

Y

.

Definition

841

.

A function

f

between two posets is said to

preserve filtered

meets

, when

f

d

S

=

d

h

f

i

S

whenever

d

S

is defined for a filter base

S

on the

first of the two posets.

Theorem

842

.

(discovered by

Todd Trimble

) A function

ϕ

:

F

(

A

)

F

(

B

)

preserves finite joins (including nullary joins) and filtered meets iff there exists a

funcoid

f

such that

h

f

i

=

ϕ

.

Proof.

Backward implication follows from above.

Let

ψ

=

ϕ

|

T

A

. Then

ψ

preserves bottom element and binary joins. Thus there

exists a funcoid

f

such that

h

f

i

=

ψ

.

It remains to prove that

h

f

i

=

ϕ

.

Really,

h

f

iX

=

d

h

f

i

up

X

=

d

h

ψ

i

up

X

=

d

h

ϕ

i

up

X

=

ϕ

d

up

X

=

ϕ

X

for every

X ∈

F

(

A

).

Corollary

843

.

Funcoids

f

from

A

to

B

bijectively correspond by the formula

h

f

i

=

ϕ

to functions

ϕ

:

F

(

A

)

F

(

B

) preserving finite joins and filtered meets.

7.4. Another way to represent funcoids as binary relations

This is based on a

Todd Trimble

’s idea.

Definition

844

.

The binary relation

ξ

~

P

(

F

(Src

ξ

)

×

F

(Dst

ξ

)) for a

funcoid

ξ

is defined by the formula

A

ξ

~

B ⇔ B w h

ξ

iA

.

Definition

845

.

The binary relation

ξ

P

(

T

Src

ξ

×

T

Dst

ξ

) for a funcoid

ξ

is defined by the formula

A ξ

B

B

w h

ξ

i

A

B

up

h

ξ

i

A.

Proposition

846

.

Funcoid

ξ

can be restored from

1

. the value of

ξ

~

;

2

. the value of

ξ

.

Proof.

1

. The value of

h

ξ

i

can be restored from

ξ

~

.

2

. The value of

h

ξ

i

can be restored from

ξ

.

Theorem

847

.

Let

ν

and

ξ

be composable funcoids. Then:

1

.

ξ

~

ν

~

= (

ξ

ν

)

~

;

2

.

ξ

ν

= (

ξ

ν

)

.

Proof.

1

.

A

(

ξ

~

ν

~

)

C ⇔ ∃B

:

A

ν

~

B ∧ B

ξ

~

C

∃B ∈

F

(Dst

ν

) : (

B w h

ν

iA ∧ C w h

ξ

iB

)

C w h

ξ

ih

ν

iA ⇔ C w h

ξ

ν

iA ⇔ A

(

ξ

ν

)

~

C

.