background image

9.6. PROPERTIES PRESERVED BY RELATIONSHIPS

211

Proof.

It’s proved above, that all morphisms (except the “unnamed” arrow,

which is the inverse morphism by definition) depicted on the diagram are bijections

and the depicted “opposite” morphisms are mutually inverse.

That arrows preserve order is obvious.

It remains to apply lemma

193

(taking into account that

θ

can be decomposed

into

G

7→

d

n

{

α

RLD

G

(

α

)

α

A

o

1

and

G

7→

d

n

{

α

FCD

G

(

α

)

α

A

o

).

Theorem

1124

.

Composition of complete reloids is complete.

Proof.

Let

f

,

g

be complete reloids. Then (

FCD

)(

g

f

) = (

FCD

)

g

(

FCD

)

f

.

Thus (because (

FCD

)(

g

f

) is a complete funcoid) we have

g

f

= (

RLD

)

out

((

FCD

)

g

(

FCD

)

f

), but (

FCD

)

g

(

FCD

)

f

is a complete funcoid, thus

g

f

is a complete

reloid.

Theorem

1125

.

1

. (

RLD

)

out

g

(

RLD

)

out

f

= (

RLD

)

out

(

g

f

) for composable complete funcoids

f

and

g

.

2

. (

RLD

)

out

g

(

RLD

)

out

f

= (

RLD

)

out

(

g

f

) for composable co-complete fun-

coids

f

and

g

.

Proof.

Let

f

,

g

be composable complete funcoids.

(

FCD

)((

RLD

)

out

g

(

RLD

)

out

f

) = (

FCD

)(

RLD

)

out

g

(

FCD

)(

RLD

)

out

f

=

g

f

.

Thus (taking into account that (

RLD

)

out

g

(

RLD

)

out

f

is complete) we have

(

RLD

)

out

g

(

RLD

)

out

f

= (

RLD

)

out

(

g

f

).

For co-complete funcoids it’s dual.

Proposition

1126

.

If

f

is a (co-)complete funcoid then up

f

is a filter.

Proof.

It is enough to consider the case if

f

is complete.

We need to prove that

F, G

up

f

:

F

u

G

up

f

.

For every

F

Rel

(Src

f,

Dst

f

) we have

F

up

f

F

w

f

⇔ h

F

i

{

x

} w h

f

i

{

x

}

.

Thus

F, G

up

f

⇒ h

F

i

{

x

} w h

f

i

{

x

}∧h

G

i

{

x

} w h

f

i

{

x

} ⇒ h

F

u

G

i

{

x

}

=

h

F

i

{

x

} u h

G

i

{

x

} w h

f

i

{

x

} ⇒

F

u

G

up

f

.

That up

f

is nonempty and up-directed is obvious.

Corollary

1127

.

1

. If

f

is a (co-)complete funcoid then up

f

= up(

RLD

)

out

f

.

2

. If

f

is a (co-)complete reloid then up

f

= up(

FCD

)

f

.

Proof.

By order isomorphism, it is enough to prove the first.

Because up

f

is a filter, by properties of generalized filter bases we have

F

up(

RLD

)

out

f

⇔ ∃

g

up

f

:

F

w

g

F

up

f

.

9.6. Properties preserved by relationships

Proposition

1128

.

(

FCD

)

f

is reflexive iff

f

is reflexive (for every endoreloid

f

).

Proof.

f

is reflexive

1

Rel

Ob

f

v

f

⇔ ∀

F

up

f

: 1

Rel

Ob

f

v

F

1

Rel

Ob

f

v

d

FCD

up

f

1

Rel

Ob

f

v

(

FCD

)

f

(

FCD

)

f

is reflexive.

Proposition

1129

.

(

RLD

)

out

f

is reflexive iff

f

is reflexive (for every endofun-

coid

f

).

Proof.

f

is reflexive

1

Rel

Ob

f

v

f

(corollary

922

)

⇔ ∀

F

up

f

: 1

Rel

Ob

f

v

F

1

Rel

Ob

f

v

d

RLD

up

f

1

Rel

Ob

f

v

(

RLD

)

out

f

(

RLD

)

out

f

is reflexive.