 6. OPERATIONS ON THE SET OF UNFIXED MORPHISMS

16

2

Because of the previous, it is enough to prove that [

f

]

DT

f

Dt

.

Really, it is equivalent to [

f

]

v

T

f

v

t

what is obvious.

Proposition

2121

.

If every Hom-set is a distributive lattice, then the poset

of unfixed morphisms is a distributive lattice.

Proof.

It follows from the above isomorphism.

Proposition

2122

.

If every Hom-set is a co-brouwerian lattice, then the poset

of unfixed morphisms is a co-brouwerian lattice.

Proof.

It follows from the above isomorphism and the definition of pseudod-

ifference.

Proposition

2123

.

If every Hom-set is a lattice with quasidifference, then the

poset of unfixed morphisms is a lattice with quasidifference.

Proof.

It follows from the above isomorphism and the definition of quasidif-

ference.

Proposition

2124

.

1

. If every Hom-set is an atomic lattice, then the poset of unfixed morphisms

is an atomic lattice.

2

. If every Hom-set is an atomistic lattice, then the poset of unfixed mor-

phisms is an atomistic lattice.

Proof.

Follows from the above isomorphism.

6.7. Binary product morphism.

Definition

2125

.

For a category

C

with binary product morphism and

X, Y

A

define

X

×

Y

= [

X

×

A,B

Y

] where

A

Z

, [

A

]

w

X

,

B

Z

, [

B

]

w

Y

. (Such

A

and

B

exist by an axiom of categories with restricted identities.)

We need to prove validity of this definition:

Proof.

Let

A

0

Z

, [

A

0

]

w

X

,

B

0

Z

, [

B

0

]

w

Y

,

A

1

Z

, [

A

1

]

w

X

,

B

1

Z

,

[

B

1

]

w

Y

. We need to prove

X

×

A

0

,B

0

Y

X

×

A

1

,B

1

Y

, but it trivially follows

from an axiom in the definition of category with binary product morphism.

Proposition

2126

.

(

X

0

×

Y

0

)

u

(

X

1

×

Y

1

) = (

X

0

u

X

1

)

×

(

Y

0

u

Y

1

) for every

X

0

, X

1

, Y

0

, Y

1

A

.

Proof.

Take

A

0

Z

, [

A

0

]

w

X

0

,

B

0

Z

, [

B

0

]

w

Y

0

,

A

1

Z

, [

A

1

]

w

X

1

,

B

1

Z

, [

B

1

]

w

Y

1

.

Then (

X

0

×

Y

0

)

u

(

X

1

×

Y

1

) = [

X

0

×

A

0

t

A

1

,B

0

t

B

1

Y

0

]

u

[

X

1

×

A

0

t

A

1

,B

0

t

B

1

Y

1

] =

[(

X

0

×

A

0

t

A

1

,B

0

t

B

1

Y

0

)

u

(

X

1

×

A

0

t

A

1

,B

0

t

B

1

Y

1

)] = [(

X

0

u

X

1

)

×

A

0

t

A

1

,B

0

t

B

1

(

Y

0

u

Y

1

)] = (

X

0

u

X

1

)

×

(

Y

0

u

Y

1

).

Proposition

2127

.

f

A,B

=

f

u

(

A

×

B

).

Proof.

Take

F

f

.

Let

F

0

=

ι

A

t

Src

F,B

t

Dst

F

F

.

We have

F

0

f

.

f

A,B

= [

ι

A,B

F

0

] = [

E

B

t

Dst

F,B

F

0

◦ E

A,A

t

Src

F

] = [id

C

(

B

t

Dst

F,B

)

[

B

]

F

0

id

C

(

A,A

t

Src

F

)

[

A

]

] = [id

C

(

B

t

Dst

F,B

)

[

B

]

]

[

F

0

]

[id

C

(

A,A

t

Src

F

)

[

A

]

] = [id

C

(

B

t

Dst

F,B

t

Dst

F

)

[

B

]

]

[

F

0

]

[id

C

(

A

t

Src

F,A

t

Src

F

)

[

A

]

] = [id

C

(

B

t

Dst

F,B

t

Dst

F

)

[

B

]

F

0

id

C

(

A

t

Src

F,A

t

Src

F

)

[

A

]

] = [

F

0

u

(

A

×

A

t

Src

F,B

t

Dst

F

B

)] = [

F

0

]

u

[

A

×

A

t

Src

F,B

t

Dst

F

B

] =

f

u

(

A

×

B

).