 3. GENERAL COPRODUCT IN PARTIALLY ORDERED DAGGER CATEGORY

11

Proof.

We need to prove

π

i

C

Q

(

L

)

F, F

i

but that was proved above.

Lemma

1989

.

f

Hom

cont(

C

)

Y,

Q

(

L

)

F

is continuous iff all

π

i

f

are con-

tinuous.

Proof.

. Let

f

Hom

cont(

C

)

Y,

Q

(

L

)

F

. Then

f

Y

v

Q

(

L

)

F

f

;

π

i

f

Y

v

π

i

Q

(

L

)

F

f

;

π

i

f

Y

v

Q

(

L

)

F

π

i

f

. Thus

π

i

f

is continuous.

. Let all

π

i

f

be continuous. Then

π

cont(

C

)

i

f

Hom

cont(

C

)

(

Y, F

i

);

π

cont(

C

)

i

f

Y

v

F

i

π

cont(

C

)

i

f

. We need to prove

Y

v

f

Q

(

L

)

F

f

that is

Y

v

f

l

i

n

((

π

i

)

F

i

π

i

)

f

for what is enough (because

f

is metamonovalued)

Y

v

l

i

n

(

f

(

π

i

)

F

i

π

i

f

)

what follows from

Y

v

d

i

n

(

f

(

π

i

)

π

i

f

Y

) what is obvious.

Theorem

1990

.

Q

(

L

)

together with

N

is a (partial) product in the category

cont(

C

).

Proof.

Obvious.

Check

http://math.stackexchange.com/questions/102632/

how-to-check-whether-it-is-a-direct-product/102677#102677

2. On duality

We will consider duality where both the category

C

and orders on Mor-sets are

replaced with their dual. I will denote

A

dual

←−→

B

when two formulas

A

and

B

are

dual with this duality.

Proposition

1991

.

f

C(

µ, ν

)

dual

←−→

f

C(

ν

, µ

).

Proof.

f

C(

µ, ν

)

f

µ

v

ν

f

dual

←−→

µ

f

w

f

ν

1

f

C(

ν

, µ

).

f

is entirely defined

f

f

w

1

Src

f

dual

←−→

f

f

v

1

Src

f

f

is injective

f

is monovalued.

f

is monovalued

f

f

v

1

Dst

f

dual

←−→

f

f

w

1

Dst

f

f

is surjective

f

is entirely defined.

3. General coproduct in partially ordered dagger category

The below is the dual of the above, proofs are omitted as they are dual.
Let

ι

i

FiXme

: What is

ι

?

are entirely defined monovalued morphisms to an

object

Z

.

Let

ι

i

dual

←−→

π

i

that is

ι

i

= (

π

i

)

. We have the above equivalent to

π

i

being

monovalued and entirely defined.