7. EXAMPLES OF CATEGORIES WITH RESTRICTED IDENTITIES

18

1

.

f

u

(

X

×

A,B

Y

) =

f

u

((

X

÷

A

)

×

FCD

(

Y

÷

B

)) = id

FCD

Y

÷

B

f

id

FCD

X

÷

A

=

id

FCD

(

B,B

)

Y

f

id

FCD

(

A,A

)

X

.

2

.

Let

unfixed

filters

X

v

[

A

0

]

u

[

A

1

]

and

Y

v

[

B

0

]

u

[

B

1

].

Then

for

X

F

(

A

1

)

we

have

h

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

)

iX

=

E

C

(

B

0

,B

1

)

h

X

×

A

0

,B

0

Y

i

E

C

(

A

1

,A

0

)

X

=

(

h

X

×

A

0

,B

0

Y

i

(

X ÷

A

0

))

÷

B

1

=

(

(

X

÷

A

0

)

×

FCD

(

Y

÷

B

0

)

(

X ÷

A

0

))

÷

B

1

.

On the other hand,

h

X

×

A

1

,B

1

Y

iX

=

(

X

÷

A

1

)

×

FCD

(

Y

÷

B

1

)

X

If [

X

]

X

then (use isomorphisms)

X

÷

A

1

and

X ÷

A

0

X

÷

A

0

. So

h

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

)

iX

=

and

h

X

×

A

1

,B

1

Y

iX

=

.

If [

X

]

6

X

then (use isomorphisms)

X 6

X

÷

A

1

and

X ÷

A

0

6

X

÷

A

0

. So

h

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

)

iX

= (

Y

÷

B

0

)

÷

B

1

=

Y

÷

B

1

and

h

X

×

A

1

,B

1

Y

iX

=

Y

÷

B

1

.

So in all cases,

h

ι

A

1

,B

1

(

X

×

A

0

,B

0

Y

)

iX

=

h

X

×

A

1

,B

1

Y

iX

.

Lemma

2131

.

FiXme

: This lemma seems not used.

X ÷

A

= (

X u

[

A

])

÷

A

for

every unfixed filter

X

and small set

A

.

Proof.

(

X u

[

A

])

÷

A

= (

X ÷

A

)

u

([

A

]

÷

A

) =?? = (

X ÷

A

)

u>

F

(

A

)

=

X ÷

A

.

Corollary

2132

.

There is a pointfree funcoid

p

such that

h

p

iX

=

X ÷

A

.

Proof.

Let

q

be the order embedding (see the diargram) from unfixed filters

F

such that

A

∈ F

to filters on

A

.

Then

hX ÷

A

iX

=

h

(

X u

[

A

])

÷

A

iX

=

D

q

id

pFCD

(unfixed filters)

[

A

]

E

X

.

Let

f

be a funcoid. Define pointfree funcoid

S

f

between unfixed filters as:

Definition

2133

.

For every unfixed filters

X

and

Y

h

S

f

iX

= [

h

f

i

(

X ÷

Src

f

)];

(

S

f

)

1

Y

= [

f

1

(

Y ÷

Dst

f

)]

.

It is really a pointfree funcoid:

Proof.

For an unfixed filter

Y

we have

Y 6 h

S

f

iX ⇔ Y 6

[

h

f

i

(

X ÷

Src

f

)]

Y ÷

Dst

f

6 h

f

i

(

X ÷

Src

f

)

⇔ X ÷

Src

f

6

f

1

(

Y ÷

Dst

f

)

⇔ X 6

[

f

1

(

Y ÷

Dst

f

)]

⇔ X 6

(

S

f

)

1

Y

.

Definition

2134

.

S

F

=

S

f

for an unfixed funcoid

F

and

f

F

.

We need to prove validity of the above definition:

Proof.

Let

f, g

F

, let

f

:

A

0

B

0

,

g

:

A

1

B

1

. Need to prove

S

f

=

S

g

.

We have

ι

A

0

t

A

1

,B

0

t

B

1

f

=

ι

A

0

t

A

1

,B

0

t

B

1

g.

h

S

ι

A

0

t

A

1

,B

0

t

B

1

f

iX

=

[

h

ι

A

0

t

A

1

,B

0

t

B

1

f

i

(

X

÷

(

A

0

t

A

1

)]

=

E

FCD

(

B

0

,B

0

t

B

1

)

h

f

i

E

FCD

(

A

0

t

A

1

,A

0

(

X ÷

(

A

0

t

A

1

))

=

[(

h

f

i

((

X ÷

(

A

0

t

A

1

))

÷

A

0

))

÷

B

0

] = [

h

f

i

(

X ÷

A

0

)] =

h

S

f

iX

.

Similarly

h

S

ι

A

0

t

A

1

,B

0

t

B

1

g

iX

=

h

S

g

iX

.

So

h

S

f

iX

=

h

S

g

iX

.

Proposition

2135

.

1

.

S

from a Hom-set

FCD

(

A, B

) is an order embedding.

2

.

S

from the category

FCD

is a prefunctor.

3

.

S

from unfixed funcoids is an order embedding and a prefunctor (= semi-

group homomorphism).

Proof.