background image

4.3. CATEGORY

REL

62

Obvious

362

.

P

(

P

U, A

) is also a set of typed sets.

Definition

363

.

I will denote

T

U

=

T

P

U

.

Remark

364

.

This means that

T

U

is the set of typed subsets of a set

U

.

Obvious

365

.

T

U

=

n

(

P

U,X

)

X

P

U

o

=

{

P

U

} ×

P

U

=

P

(

P

U, U

).

Obvious

366

.

T

U

is a complete atomistic boolean lattice. Particularly:

1

.

T

U

= (

P

U,

);

2

.

>

T

U

= (

P

U, U

);

3

. (

P

U, A

)

t

(

P

U, B

) = (

P

U, A

B

);

4

. (

P

U, A

)

u

(

P

U, B

) = (

P

U, A

B

);

5

.

d

A

S

(

P

U, A

) = (

P

U,

S

A

S

A

);

6

.

d

A

S

(

P

U, A

) =

 

P

U,

(

T

A

S

A

if

A

6

=

U

if

A

=

!

;

7

. (

P

U, A

) = (

P

U, U

\

A

);

8

. atomic elements are (

P

U,

{

x

}

) where

x

U

.

Typed sets are “better” than regular sets as (for example) for a set

U

and a typed

set

X

the following are defined by regular order theory:

atoms

X

;

X

;

d

T

U

.

For regular (“non-typed”) sets these are not defined (except of atoms

X

which how-

ever needs a special definition instead of using the standard order-theory definition

of atoms).

Typed sets are convenient to be used together with filters on sets (see below),

because both typed sets and filters have a set

P

U

as their type.

Another advantage of typed sets is that their binary product (as defined below)

is a

Rel

-morphism. This is especially convenient because below defined products

of filters are also morphisms of related categories.

Well, typed sets are also quite awkward, but the proper way of doing modern

mathematics is

type theory

not ZFC, what is however outside of the topic of this

book.

4.3. Category Rel

I remind that

Rel

is the category of (small) binary relations between sets, and

Set

is its subcategory where only monovalued entirely defined morphisms (func-

tions) are considered.

Definition

367

.

Order on

Rel

(

A, B

) is defined by the formula

f

v

g

GR

f

GR

g

.

Obvious

368

.

This order is isomorphic to the natural order of subsets of the

set

A

×

B

.

Definition

369

.

X

[

f

]

Y

GR

X

[GR

f

]

GR

Y

and

h

f

i

X

=

(Dst

f,

h

GR

f

i

GR

X

) for a

Rel

-morphism

f

and typed sets

X

T

Src

f

,

Y

T

Dst

f

.

Definition

370

.

For category

Rel

there is defined reverse morphism:

(

A, B, F

)

1

= (

B, A, F

1

).

Obvious

371

.

(

f

1

)

1

=

f

for every

Rel

-morphism

f

.