5. BINARY PRODUCT

11

5. Binary product

Definition

2091

.

The category

with binary product morphism

is a category

with restricted identities and additional axioms

1

. id

C

(

B,B

)

Y

f

id

C

(

A,A

)

X

=

f

u

(

X

×

A,B

Y

) (holding for every

A, B

Z

,

A

3

X

v

[

A

],

A

3

Y

v

[

B

],

X

×

A,B

Y

∈ C

(

A, B

) and morphism

f

∈ C

(

A, B

));

2

.

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

) =

X

×

A

1

,B

1

Y

whenever

X

v

[

A

0

]

u

[

A

1

] and

Y

v

[

B

0

]

u

[

B

1

].

Proposition

2092

.

The second axiom is equivalent to the following axiom:

1

.

f

X

×

A

0

,B

0

Y

f

=

X

×

A

1

,B

1

Y

whenever

X

v

[

A

0

]

u

[

A

1

] and

Y

v

[

B

0

]

u

[

B

1

],

f

:

A

1

B

1

.

Proof.

. Obvious.

.

f

X

×

A

0

,B

0

Y

f

=

X

×

A

1

,B

1

Y

because

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

) =

X

×

A

1

,B

1

Y

and

ι

A

0

,B

0

(

X

×

A

1

,B

1

Y

) =

X

×

A

0

,B

0

Y

.

Let’s prove

f

X

×

A

0

,B

0

Y

f

=

X

×

A

1

,B

1

Y

. Really, if

f

X

×

A

0

,B

0

Y

then

f

=

ι

A

1

,B

1

f

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

) =

X

×

A

1

,B

1

Y

and thus

f

=

X

×

A

1

,B

1

Y

.

Proposition

2093

.

[

A

]

×

A,B

[

B

] is the greatest morphism

>

C

(

A,B

)

:

A

B

.

Proof.

It’s enough to prove

f

u

([

A

]

×

A,B

[

B

]) =

f

for every

f

:

A

B

.

Really,

f

u

([

A

]

×

A,B

[

B

]) = id

C

(

B,B

)

B

f

id

C

(

A,A

)

A

= 1

B

f

1

A

=

f

.

Proposition

2094

.

For every category with binary product morphism

X

×

A,B

Y

= id

C

(

B,B

)

Y

◦>

C

(

A,B

)

id

C

(

A,A

)

X

Proof.

X

×

A,B

Y

w

id

C

(

B,B

)

Y

◦>

C

(

A,B

)

id

C

(

A,A

)

X

because id

C

(

B,B

)

Y

◦>

C

(

A,B

)

id

C

(

A,A

)

X

=

>

C

(

A,B

)

u

(

X

×

A,B

Y

).

id

C

(

B,B

)

Y

◦>

C

(

A,B

)

id

C

(

A,A

)

X

w

id

C

(

B,B

)

Y

(

X

×

A,B

Y

)

id

C

(

A,A

)

X

= (

X

×

A,B

Y

)

u

(

X

×

A,B

Y

) =

X

×

A,B

Y

.

Proposition

2095

.

ι

A,B

(

f

u

g

) =

ι

A,B

f

u

ι

A,B

g

for every parallel morphisms

f

and

g

and objects

A

and

B

, whenever all

E

X,Y

are metamonovalued and metain-

jective.

Proof.

ι

A,B

(

f

u

g

) =

E

Dst

f,B

(

f

u

g

)

◦ E

A,

Src

f

= (

E

Dst

f,B

f

◦ E

A,

Src

f

)

u

(

E

Dst

f,B

g

◦ E

A,

Src

f

) =

ι

A,B

f

u

ι

A,B

g

.

Proposition

2096

.

(

X

0

×

A,B

Y

0

)

u

(

X

1

×

A,B

Y

1

) = (

X

0

u

X

1

)

×

A,B

(

Y

0

u

Y

1

).

Proof.

(

X

0

×

A,B

Y

0

)

u

(

X

1

×

A,B

Y

1

) = id

C

(

B,B

)

Y

1

(

X

0

×

A,B

Y

0

)

id

C

(

A,A

)

X

1

=

id

C

(

B,B

)

Y

1

id

C

(

B,B

)

Y

0

◦>

C

(

A,B

)

id

C

(

A,A

)

X

1

id

C

(

A,A

)

X

0

= id

C

(

B,B

)

Y

0

u

Y

1

◦>

C

(

A,B

)

id

C

(

A,A

)

X

0

u

X

1

=

(

X

0

u

X

1

)

×

A,B

(

Y

0

u

Y

1

).

Proposition

2097

.

For a category with binary product morphism Im

f

,

Dom

f

, IM

f

, and DOM

f

are filters.

Proof.

That they are upper sets was proved above.

To prove that Im

f

is a filter it remains to show

A, B

Im

f

A

u

B

Im

f

.

Really,

A, B

Im

f

⇔ > ×

A

w

f

∧ > ×

B

w

f

⇒ > ×

(

A

u

B

)

w

f

A

u

B

Im

f

.

Dom

f

is similar.

The thesis for IM

f

, DOM

f

follows from above proved for Im

f

, Dom

f

.