background image

Theorem 17.223.

For every lters

a

0

,

a

1

,

b

0

,

b

1

we have

a

0

FCD

b

0

f

(

C

)

g

a

1

FCD

b

1

,

a

0

RLD

b

0

f

(

A

)

g

a

1

RLD

b

1

:

Proof.

a

0

RLD

b

0

f

(

A

)

g

a

1

RLD

b

1

, 8

A

0

2

a

0

; B

0

2

b

0

; A

1

2

a

1

; B

1

2

b

1

:

A

0

B

0

f

(

A

)

g

A

1

B

1

.

A

0

B

0

f

(

A

)

g

A

1

B

1

,

A

0

B

0

f

(

C

)

g

A

1

B

1

,

A

0

[

f

]

A

1

^

B

0

[

g

]

B

1

. (Here by

A

0

B

0

f

(

C

)

g

A

1

B

1

I mean

"

FCD

(

Base

a

;

Base

b

)

(

A

0

B

0

)

f

(

C

)

g

"

FCD

(

Base

a

;

Base

b

)

(

A

1

B

1

)

.)

Thus it is equivalent to

a

0

[

f

]

a

1

^

b

0

[

g

]

b

1

that is

a

0

FCD

b

0

f

(

C

)

g

a

1

FCD

b

1

.

(It was used the theorem

17.151

.)

Can the above theorem be generalized for the innitary case?

17.16 Coordinate-wise continuity

Theorem 17.224.

Let

and

be indexed (by some index set

n

) families of endomorphisms for

a quasi-invertible dagger category with star-morphisms, and

f

i

2

Mor

(

Ob

i

;

Ob

i

)

for every

i

2

n

.

Then:

1.

8

i

2

n

:

f

i

2

C

(

i

;

i

)

)

Q

(

C

)

f

2

C

 Q

(

C

)

;

Q

(

C

)

;

2.

8

i

2

n

:

f

i

2

C

0

(

i

;

i

)

)

Q

(

C

)

f

2

C

0

 Q

(

C

)

;

Q

(

C

)

;

3.

8

i

2

n

:

f

i

2

C

00

(

i

;

i

)

)

Q

(

C

)

f

2

C

00

 Q

(

C

)

;

Q

(

C

)

.

Proof.

Using the corollary

17.140

:

1.

8

i

2

n

:

f

i

2

C

(

i

;

i

)

, 8

i

2

n

:

f

i

i

v

i

f

i

)

Q

i

2

n

(

C

)

(

f

i

i

)

v

Q

i

2

n

(

C

)

(

i

f

i

)

,

 Q

(

C

)

f

 Q

(

C

)

v

 Q

(

C

)

 Q

(

C

)

f

,

Q

(

C

)

f

2

C

 Q

(

C

)

;

Q

(

C

)

.

2.

8

i

2

n

:

f

i

2

C

0

(

i

;

i

)

, 8

i

2

n

:

i

v

f

i

y

i

f

i

)

Q

(

C

)

v

Q

i

2

n

(

C

)

¡

f

i

y

i

f

i

,

Q

(

C

)

v

 Q

i

2

n

(

C

)

f

i

y

 Q

i

2

n

(

C

)

i

 Q

i

2

n

(

C

)

f

i

,

Q

(

C

)

v

 Q

i

2

n

(

C

)

f

i

y

 Q

i

2

n

(

C

)

i

 Q

i

2

n

(

C

)

f

i

,

Q

(

C

)

f

2

C

0

 Q

(

C

)

;

Q

(

C

)

.

3.

8

i

2

n

:

f

i

2

C

00

(

i

;

i

)

, 8

i

2

n

:

f

i

i

f

i

y

v

i

)

Q

i

2

n

(

C

)

¡

f

i

i

f

i

y

v

Q

i

2

n

(

C

)

i

,

Q

i

2

n

(

C

)

f

i

Q

i

2

n

(

C

)

i

Q

i

2

n

(

C

)

f

i

y

v

Q

i

2

n

(

C

)

i

,

Q

i

2

n

(

C

)

f

i

Q

i

2

n

(

C

)

i

 Q

i

2

n

(

C

)

f

i

y

v

Q

i

2

n

(

C

)

i

,

Q

i

2

n

(

C

)

f

i

2

C

00

 Q

(

C

)

;

Q

(

C

)

.

Theorem 17.225.

Let

and

be indexed (by some index set

n

) families of endofuncoids, and

f

i

2

FCD

(

Ob

i

;

Ob

i

)

for every

i

2

n

. Then:

1.

8

i

2

n

:

f

i

2

C

(

i

;

i

)

)

Q

(

A

)

f

2

C

 Q

(

A

)

;

Q

(

A

)

;

2.

8

i

2

n

:

f

i

2

C

0

(

i

;

i

)

)

Q

(

A

)

f

2

C

0

 Q

(

A

)

;

Q

(

A

)

;

3.

8

i

2

n

:

f

i

2

C

00

(

i

;

i

)

)

Q

(

A

)

f

2

C

00

 Q

(

A

)

;

Q

(

A

)

.

Proof.

Similar to the previous theorem.

Theorem 17.226.

Let

and

be indexed (by some index set

n

) families of pointfree endofuncoids

between posets with least elements, and

f

i

2

FCD

(

Ob

i

;

Ob

i

)

for every

i

2

n

. Then:

1.

8

i

2

n

:

f

i

2

C

(

i

;

i

)

)

Q

(

S

)

f

2

C

 Q

(

S

)

;

Q

(

S

)

;

236

Multifuncoids and staroids