1. GENERAL PRODUCT IN PARTIALLY ORDERED DAGGER CATEGORY

9

Remark

1973

.

In some important examples the function

π

is entire, that is

dom

π

is the set of all small indexed families of objects of

C

. However there are also

some important examples where it is partial.

Definition

1974

.

Infimum product

Q

F

(such that

π

is defined at

λj

n

:

Src

F

j

and

λj

n

: Dst

F

j

) is defined by the formula

(

L

)

Y

F

=

l

i

dom

F

((

π

λj

n

:Dst

F

j

i

)

F

i

π

λj

n

:Src

F

j

i

)

.

This formula can be (over)simplified to:

(

L

)

Y

F

=

l

i

dom

F

((

π

Dst

F

i

)

F

i

π

Src

F

i

)

.

Remark

1975

.

(

π

λj

n

:Dst

F

j

i

)

F

i

π

λj

n

:Src

F

j

i

Hom

Q

(

Q

)

j

n

Src

F

j

,

Q

(

Q

)

j

n

Dst

F

j

are properly defined and have the same sources

and destination (whenever

i

dom

F

is), thus the meet in the formulas is properly

defined.

Remark

1976

.

Thus

F

0

×

(

L

)

F

1

= ((

π

(Dst

F

0

,

Dst

F

1

)

0

)

F

0

π

(Src

F

0

,

Src

F

1

)

0

)

u

((

π

(Dst

F

0

,

Dst

F

1

)

1

)

F

1

π

(Src

F

0

,

Src

F

1

)

1

)

that is product is defined by a pure algebraic formula.

Proposition

1977

.

Q

(

L

)

F

= max

(

Φ

Hom

Q

(

Q

)

j

n

Src

F

j

,

Q

(

Q

)

j

n

Dst

F

j

i

n

v

(

π

λj

n

:Dst

Fj

i

)

F

i

π

λj

n

:Src

Fj

i

)

.

Proof.

By definition of meet on a complete lattice.

Corollary

1978

.

Q

(

L

)

F

=

d

(

Φ

Hom

Q

(

Q

)

j

n

Src

F

j

,

Q

(

Q

)

j

n

Dst

F

j

i

n

v

(

π

λj

n

:Dst

Fj

i

)

F

i

π

λj

n

:Src

Fj

i

)

.

Theorem

1979

.

Let

π

X

i

be metamonovalued morphisms.

If

S

P

(Hom(

A

0

, B

0

)

×

Hom(

A

1

, B

1

)) for some sets

A

0

,

B

0

,

A

1

,

B

1

then

l

a

×

(

L

)

b

(

a, b

)

S

=

l

dom

S

×

(

L

)

l

im

S.

Proof.

l

a

×

b

(

a, b

)

S

=

l

(

((

π

(Dst

a,

Dst

b

)

0

)

a

π

(Src

a,

Src

b

)

0

)

u

((

π

(Dst

a,

Dst

b

)

1

)

b

π

(Src

a,

Src

b

)

1

)

(

a, b

)

S

)

=

l

(

(

π

(Dst

a,

Dst

b

)

0

)

a

π

(Src

a,

Src

b

)

0

a

dom

S

)

u

l

(

(

π

(Dst

a,

Dst

b

)

1

)

b

π

(Src

a,

Src

b

)

1

b

im

S

)

=

(

π

(Dst

a,

Dst

b

)

0

)

l

n

a

a

dom

S

o

π

(Src

a,

Src

b

)

0

u

(

π

(Dst

a,

Dst

b

)

1

)

l

b

b

im

S

π

(Src

a,

Src

b

)

1

=

(

π

(Dst

a,

Dst

b

)

0

)

l

dom

S

π

(Src

a,

Src

b

)

0

u

(

π

(Dst

a,

Dst

b

)

1

)

l

im

S

π

(Src

a,

Src

b

)

1

=

l

dom

S

×

l

im

S.

Corollary

1980

.

(

a

0

×

(

L

)

b

0

)

u

(

a

1

×

(

L

)

b

1

) = (

a

0

u

a

1

)

×

(

L

)

(

b

0

u

b

1

).

Corollary

1981

.

a

0

×

(

L

)

b

0

6

a

1

×

(

L

)

b

1

a

0

6

a

1

b

0

6

b

1

.