7. EXAMPLES OF CATEGORIES WITH RESTRICTED IDENTITIES

20

id

C

(

B,C

)

Y

id

C

(

A,B

)

X

=

d

x

up

X,y

up

Y

(id

C

(

B,C

)

y

id

C

(

A,B

)

x

)

=

d

x

up

X,y

up

Y

id

C

(

A,B

)

x

y

= id

C

(

A,B

)

X

u

Y

.

A

A

B

Z

:

A

v

[

B

] is obvious.

Obvious

2140

.

E

A,B

RLD

=

RLD

(

A,B

)

id

A

B

.

Proposition

2141

.

RLD

with

X ×

A,B

Y

= (

X ÷

A

)

×

RLD

(

X ÷

B

) for every

unfixed filters

X

and

Y

is a category with binary product morphism.

Proof.

id

C

(

B,B

)

Y

f

id

C

(

A,A

)

X

=

f

u

(

X ×

A,B

Y

) because id

C

(

B,B

)

Y

f

id

C

(

A,A

)

X

=

(id

RLD

B

÷

(

B

×

B

))

f

(id

RLD

X ÷

A

÷

(

A

×

A

)) = id

RLD

B

f

id

RLD

X ÷

A

=

f

u

((

X ÷

A

)

×

RLD

(

Y ÷

B

)) =

f

u

(

X ×

A,B

Y

).

ι

A

1

,B

1

(

X ×

A

0

,B

0

Y

) =

E

B

0

,B

1

(

X ×

A

0

,B

0

Y

)

◦E

A

1

,A

0

=

RLD

(

B

0

,B

1

)

id

B

0

B

1

((

X ÷

B

0

)

×

(

Y ÷

A

0

))

◦ ↑

RLD

(

A

1

,A

0

)

id

A

0

A

1

= ((

X ÷

B

0

)

÷

B

1

)

×

((

Y ÷

A

0

)

÷

A

1

) =

(

X ÷

B

1

)

×

(

Y ÷

A

1

) =

X ×

A

1

,B

1

Y

.

Proposition

2142

.

ι

A,B

f

=

f

÷

(

A

×

B

) for every reloid

f

.

Proof.

ι

A,B

f

=

E

Dst

f,B

RLD

f

◦ E

A,

Src

f

RLD

=

d

RLD

F

up

f

(

Rel

(Dst

f,B

)

id

Dst

f

B

F

◦ ↑

Rel

(

A,

Src

f

)

id

A

Src

f

) =

d

RLD

F

up

f

(

Rel

(

A,B

)

(id

Dst

f

B

GR

F

id

Dst

f

B

)) =

d

RLD

F

up

f

Rel

(

A,B

)

(

F

(

A

×

B

)) =

f

÷

(

A

×

B

).

Proposition

2143

.

id

RLD

(

A,A

)

X

= id

RLD

X

÷

A

whenever

A

Z

and

A

3

X

v

[

A

].

Proof.

id

RLD

(

A,A

)

X

= id

RLD

X

÷

(

A

A

)

÷

(

A

×

A

) = id

RLD

X

÷

A

.

Definition

2144

.

Category

RLD

can be considered as a category with binary

product morphism with the binary product defined as:

X ×

A,B

Y

= (

X ÷

A

)

×

RLD

(

Y ÷

B

) for every unfixed filters

X

and

Y

.

It is really a binary product morphism:

Proof.

Need to prove the axioms:

1

.

f

u

(

X

×

A,B

Y

) =

f

u

((

X

÷

A

)

×

RLD

(

Y

÷

B

)) = id

RLD

Y

÷

B

f

id

RLD

X

÷

A

=

id

RLD

(

B,B

)

Y

f

id

RLD

(

A,A

)

X

.

2

.

Let unfixed filters

X

v

[

A

0

]

u

[

A

1

] and

Y

v

[

B

0

]

u

[

B

1

].

Then we

have

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

) =

E

C

(

B

0

,B

1

)

(

X

×

A

0

,B

0

Y

)

◦ E

C

(

A

1

,A

0

)

=

RLD

(

B

0

,B

1

)

id

B

0

B

1

((

X

÷

A

0

)

×

RLD

(

Y

÷

B

0

))

◦ ↑

RLD

(

A

1

,A

0

)

id

A

0

A

1

.

But (

X

÷

A

0

)

×

RLD

(

Y

÷

B

0

)

=

d

RLD

x

up(

X

÷

A

0

)

,y

up(

Y

÷

B

0

)

(

x

×

y

)

=

(by the bijection) =

d

RLD

x

up

X,y

up

Y

((

x

÷

A

0

)

×

(

y

÷

B

0

)).

Thus

by

definition

of

reloidal

product

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

)

=

d

RLD

(

A

1

,B

1

)

x

up

X,y

up

Y

(id

B

0

B

1

((

x

÷

A

0

)

×

(

y

÷

B

0

))

id

A

0

A

1

) =

d

RLD

(

A

1

,B

1

)

x

up

X,y

up

Y

((

x

÷

A

0

)

×

(

y

÷

B

0

)) =

d

RLD

(

A

1

,B

1

)

x

up(

X

÷

A

0

)

,y

up(

Y

÷

B

0

)

(

x

×

y

) = (

X

÷

A

1

)

×

RLD

(

Y

÷

B

1

) =

X

×

A

1

,B

1

Y

.

Definition

2145

.

Reloid

S

f

End

RLD

(small sets) is defined by the formula

GR

S

f

=

S

GR

f

for every reloid

f

.

FiXme

: Small sets vs small sets

×

small sets.

Definition

2146

.

Reloid

S

f

End

RLD

(small sets) if defined by the formula

S

f

=

S

F

for arbitrary

F

f

for every unfixed reloid

f

.

That the result does not depend on the choice of

F

obviously follows from the

corresponding result for filters.

Proposition

2147

.