background image

6. DAGGER SYSTEMS OF SIDES

46

5. Negative results

The following negative result generalizes theorem 3.8 in [

3

].

Theorem

2274

.

The element 1

(Src Υ)(

A

,

A

)

is not complemented if

A

is a non-

atomic boolean lattice, for every monotone system of sides.

Proof.

Let

T

= 1

(Src Υ)(

A

,

A

)

.

Let’s suppose

T

t

V

=

>

for

V

(Src Υ)(

A

,

A

) and prove

T

u

V

6

=

.

Then

h

T

t

V

i

a

=

>

for all

a

6

=

and thus

h

V

i

a

t

a

=

>

.

Consequently

h

V

i

a

w ¬

a

for all

a

6

=

.

If

a

isn’t an atom, then there exists

b

with 0

@

b

@

a

and hence

h

V

i

a

w h

V

i

b

w

¬

b

A

¬

a

; thus

h

V

i

a

A

¬

a

.

There is such

c

@

>

that

a

v

c

for every atom

a

. (Really, suppose some element

p

6

=

has no atoms. Thus all atoms are in

¬

p

.)

For

a

6v

c

we have

h

V

i

a

u

a

A

for all

a

v ¬

c

thus

h

T

u

V

i

a

w h

V

i

a

u

a

A

.

Thus

h

(

T

u

V

)

id

¬

c

i

a

A

So

T

u

V

w

(

T

u

V

)

id

¬

c

A

. So

V

is not a complement of

T

.

Corollary

2275

.

(Src Υ)(

A

,

A

) is not boolean if

A

is a non-atomic boolean

lattice.

6. Dagger systems of sides

Proposition

2276

.

1

. For a partially ordered dagger category, each of Hom-set of which has least

element, we have

=

.

2

. For a partially ordered dagger category, each of Hom-set of which has

greatest element, we have

>

=

>

.

Proof.

f

Hom(

A, B

) :

v

f

⇔ ∀

f

Hom(

A, B

) :

⊥ v

f

⇔ ∀

f

Hom(

A, B

) :

⊥ v

f

1. Thus

is the least.

The other items is dual.

Definition

2277

.

Dagger system of presides with identities

is system of pre-

sides with identities with category Src Υ being a partially ordered dagger category
and (id

X

)

= id

X

for every

X

.

Proposition

2278

.

For a system of sides we have (

X

×

Y

)

=

Y

×

X

.

Proof.

(

X

×

Y

)

= (id

Y

◦> ◦

id

X

)

= id

X

◦>

id

Y

= id

X

◦> ◦

id

Y

=

Y

×

X

.

FiXme

: Which properties of pointfree funcoids can be generalized for sides?