background image

2. injective;

3. entirely defined if

A

B

;

4. surjective if

B

A

.

Proof.

1.

(

A

B

)

(

B

A

)

1

B

Rel

;

(

A

B

)

(

A

B

)

1

1

B

Rel

;

(

A

C

B

)

(

A

C

B

)

1

B

C

.

2.

(

B

A

)

(

A

B

)

1

A

Rel

;

(

A

B

)

1

(

A

B

)

1

A

Rel

;

(

A

C

B

)

(

A

C

B

)

1

A

C

.

3.

(

B

A

)

(

A

B

)

1

A

Rel

;

(

A

B

)

1

(

A

B

)

1

A

Rel

;

(

A

C

B

)

(

A

C

B

)

1

A

C

.

4.

(

A

B

)

(

B

A

)

1

A

Rel

;

(

A

B

)

(

A

B

)

1

1

A

Rel

;

(

A

C

B

)

(

A

C

B

)

1

A

C

.

4 Rectangular embedding-restriction

Definition 25.

ι

B

0

,B

1

f

= (

A

1

C

B

1

)

f

(

B

0

C

A

0

)

for

f

Mor

C

(

A

0

;

A

1

)

.

For brevity

ι

B

f

=

ι

B ,B

f

.

Proposition 26.

ι

Src

f ,

Dst

f

f

=

f

.

Proof.

ι

Src

f ,

Dst

f

f

= (

Dst

f

C

Dst

f

)

f

(

Src

f

C

Src

f

) = 1

C

Dst

f

f

1

C

Src

f

=

f

.

Proposition 27.

The function

ι

B

0

,B

1

|

f

Mor

C

(

A

0

;

A

1

)

is injective, if

A

0

B

0

A

1

B

1

.

Proof.

Because

A

1

C

B

1

is a monomorphism and

A

0

C

B

0

is an epimorphism.

Proposition 28.

ι

C

0

,C

1

ι

B

0

,B

1

f

=

ι

C

0

,C

1

f

for

B

0

A

0

C

0

,

B

1

A

1

C

1

and

f

:

A

0

A

1

.

Proof.

ι

C

0

,C

1

ι

B

0

,B

1

f

= (

B

1

C

C

1

)

(

A

1

C

B

1

)

f

(

B

0

C

A

0

)

(

C

0

C

B

0

) = (

A

1

C

C

1

)

f

(

C

0

C

A

0

) =

ι

C

0

,C

1

f

.

Proposition 29.

Let

f

:

A

0

A

1

and

g

:

A

1

A

2

and

A

1

B

1

. Then

ι

B

0

,B

2

(

g

f

) =

ι

B

1

,B

1

g

ι

B

0

,B

1

f

.

Proof.

ι

B

0

,B

2

(

g

f

) = (

A

2

C

B

2

)

(

g

f

)

(

B

0

C

A

0

) = (

A

2

C

B

2

)

g

id

A

1

f

(

B

0

C

A

0

) =

(

A

2

C

B

2

)

g

(

B

1

A

1

)

(

A

1

B

1

)

f

(

B

0

C

A

0

) =

ι

B

1

,B

1

g

ι

B

0

,B

1

f

.

5 Examples of partially ordered dagger categories under Rel

5.1 Generalized rebase of filters

In [2] I defined

rebase

A ÷

A

for a set-theoretic filter

A

and a set

X

such that

X

∈ A

:

X

A

.

Now define a generalized rebase for every set-theoretic filter

A

and every set

A

:

Definition 30.

A ÷

A

=

d

{↑

A

(

X

A

)

|

X

∈ A}

.

Proposition 31.

In the case of

X

∈ A

:

X

A

these two definitions coincide.

Proof.

Let

X

∈ A

:

X

A

. Then as it is proved in [2]

{

X

P

A

| ∃

Y

∈ A

:

Y

X

}

is a filter.

If

P

∈ {

X

P

A

| ∃

Y

∈ A

:

Y

X

}

then

P

P

A

and

Y

P

for some

Y

∈ A

. Thus

P

Y

A

d

{↑

B

(

Y

A

)

|

Y

∈ A}

.

If

P

d

{↑

B

(

X

A

)

|

X

∈ A}

then by properties of generalized filter bases, there exists

X

∈ A

such that

P

X

A

. Also

P

P

A

. Thus

P

X

. Thus

P

∈ {

X

P

A

| ∃

Y

∈ A

:

Y

X

}

.

[TODO: Clear this proof: wording, consistent use of letters.]

Examples of partially ordered dagger categories under

Rel

3