background image

4.3. CATEGORY

REL

63

Obvious

375

.

f

1

=[

f

]

∗−

1

for every

Rel

-morphism

f

.

Obvious

376

.

(

g

f

)

1

=

f

1

g

1

for every composable

Rel

-morphisms

f

and

g

.

Proposition

377

.

h

g

f

i

=

h

g

i

◦ h

f

i

for every composable

Rel

-morphisms

f

and

g

.

Proof.

Exercise.

Proposition

378

.

The above definitions of monovalued morphisms of

Rel

and of injective morphisms of

Set

coincide with how mathematicians usually define

monovalued functions (that is morphisms of

Set

) and injective functions.

Proof.

Let

f

be a

Rel

-morphism

A

B

.

The following are equivalent:

f

is a monovalued relation;

• ∀

x

A, y

0

, y

1

B

: (

x f y

0

x f y

1

y

0

=

y

1

);

• ∀

x

A, y

0

, y

1

B

: (

y

0

6

=

y

1

⇒ ¬

(

x f y

0

)

∨ ¬

(

x f y

1

));

• ∀

y

0

, y

1

B

x

A

: (

y

0

6

=

y

1

⇒ ¬

(

x f y

0

)

∨ ¬

(

x f y

1

));

• ∀

y

0

, y

1

B

: (

y

0

6

=

y

1

⇒ ∀

x

A

: (

¬

(

x f y

0

)

∨ ¬

(

x f y

1

)));

• ∀

y

0

, y

1

B

: (

x

A

: (

x f y

0

x f y

1

)

y

0

=

y

1

);

• ∀

y

0

, y

1

B

:

y

0

(

f

f

1

)

y

1

y

0

=

y

1

;

f

f

1

v

1

B

.

Let now

f

be a

Set

-morphism

A

B

.

The following are equivalent:

f

is an injective function;

• ∀

y

B, a, b

A

: (

a f y

b f y

a

=

b

);

• ∀

y

B, a, b

A

: (

a

6

=

b

⇒ ¬

(

a f y

)

∨ ¬

(

b f y

));

• ∀

y

B

: (

a

6

=

b

⇒ ∀

a, b

A

: (

¬

(

a f y

)

∨ ¬

(

b f y

)));

• ∀

y

B

: (

a, b

A

: (

a f y

b f y

)

a

=

b

);

f

1

f

v

1

A

.

Proposition

379

.

For a binary relation

f

we have:

1

.

h

f

i

S

S

=

S

h

f

i

S

for a set of sets

S

;

2

.

S

S

[

f

]

Y

⇔ ∃

X

S

:

X

[

f

]

Y

for a set of sets

S

;

3

.

X

[

f

]

S

T

⇔ ∃

Y

T

:

X

[

f

]

Y

for a set of sets

T

;

4

.

S

S

[

f

]

S

T

⇔ ∃

X

S, Y

T

:

X

[

f

]

Y

for sets of sets

S

and

T

;

5

.

X

[

f

]

Y

⇔ ∃

α

X, β

Y

:

{

α

}

[

f

]

{

β

}

for sets

X

and

Y

;

6

.

h

f

i

X

=

S

h

f

i

atoms

X

for a set

X

(where atoms

X

=

n

{

x

}

x

X

o

).

Proof.

1

.

y

∈ h

f

i

[

S

⇔ ∃

x

[

S

:

x f y

⇔ ∃

P

S, x

P

:

x f y

P

S

:

y

∈ h

f

i

P

⇔ ∃

Q

h

f

i

S

:

y

Q

y

[

h

f

i

S.

2

.

[

S

[

f

]

Y

⇔ ∃

x

[

S, y

Y

:

x f y

X

S, x

X, y

Y

:

x f y

⇔ ∃

X

S

:

X

[

f

]

Y.

3

By symmetry.