background image

Let

G

and

H

are graphs.

The exponential graph MOR

(

G

;

H

)

is dened by the formulas:

Ob MOR

(

G

;

H

) = (

Ob

H

)

Ob

G

;

(

f

;

g

)

2

GR MOR

(

G

;

H

)

, 8

(

v

;

w

)

2

GR

G

: (

f

(

v

);

g

(

w

))

2

GR

H

for every

f ; g

2

Ob MOR

(

G

;

H

) = (

Ob

H

)

Ob

G

.

Equivalently

(

f

;

g

)

2

GR MOR

(

G

;

H

)

, 8

(

v

;

w

)

2

GR

G

:

g

 f

(

v

;

w

)

f

¡

1

GR

H

(

f

;

g

)

2

GR MOR

(

G

;

H

)

,

g

(

GR

G

)

f

¡

1

GR

H

(

f

;

g

)

2

GR MOR

(

G

;

H

)

,

f

(

C

)

g

GR

G

GR

H

Evaluation

"

: (

MOR

(

G

;

H

)

G

)

!

H

If

(

f

;

g

)

2

GR MOR

(

G

;

H

)

and

x

2

GR

G

then

"

((

f

;

g

);

x

) = (

fx

;

gx

) =

g

 f

(

x

;

x

)

f

¡

1

3.2 Exponentials in category Fcd

The below gives denitions for exponential object, (exponential) evaluation, and exponential trans-
pose, but no proof is given that they are really exponential object, (exponential) evaluation, and
exponential transpose. Please write

porton@narod.ru

if you nd a proof.

If

G

,

H

are endofuncoids, then MOR

(

G

;

H

)

(

exponential object

) is an endofuncoid.

MOR

(

G

;

H

) =

G

f

t

2

atoms

FCD

((

Ob

H

)

Ob

G

; (

Ob

H

)

Ob

G

)

j

(

im

t

)

G

(

dom

t

)

¡

1

v

H

g

=

t

2

atoms

FCD

((

Ob

H

)

Ob

G

; (

Ob

H

)

Ob

G

)

j

(

dom

t

)

(

C

)

(

im

t

)

G

v

H

 

:

Evaluation:

"

¡¡

f

(

A

)

g

(

A

)

x

=

h

f

i

(

RLD

)

in

x

FCD

h

g

i

(

RLD

)

in

x:

"

¡¡

f

(

A

)

g

(

A

)

x

=

g

((

RLD

)

in

x

FCD

(

RLD

)

in

x

)

f

¡

1

=

f

(

C

)

g

((

RLD

)

in

x

FCD

(

RLD

)

in

x

)

for atomic

f ; g

2

FCD

(

Ob

G

;

Ob

H

)

.

Evaluation

"

:

MOR

(

A

;

B

)

A

!

B

"

(

F

x

) =

g

(

x

FCD

x

)

f

¡

1

j

f ; g

2

atoms

FCD

(

Ob

A

;

Ob

B

)

; f

g

/

F

 

:

"

(

F

x

) =

F

f

g

1

FCD

f

1

j

f

0

; g

0

; f

1

; g

1

2

atoms

F

;

(

f

0

FCD

f

1

)

(

g

0

FCD

g

1

)

/

F

g

.

Proposition 15.

"

:

MOR

(

A

;

B

)

A

!

B

.

Proof.

We need to prove

"

(

MOR

(

A

;

B

)

A

)

v

B

"

. ??

Transpose

f

:

Z

!

MOR

(

A

;

B

)

for a morphism

f

:

Z

A

!

B

(

f

)

x

=

G

f

b

FCD

h

f

i

(

x

b

)

j

b

2

atoms

FCD

g

:

Proposition 16.

f

:

Z

!

MOR

(

A

;

B

)

.

Proof.

We need to prove

f

Z

v

MOR

(

A

;

B

)

 

f

whenever

f

(

Z

A

)

v

B

f

. ??

Awoday 6.5 Equational denition gives a simple way to check cartesian closed categories.
It's enough to prove:

1.

"

(

f

1

A

) =

f

2.

"

 

(

g

1

A

) =

g

"

(

f

1

A

)

x

=

"

((

f

)

x

x

) =

F

f

g

1

FCD

f

1

j

f

0

; g

0

; f

1

; g

1

2

atoms

F

;

(

f

0

FCD

f

1

)

(

g

0

FCD

g

1

)

/

(

f

)

x

g

= ??

??

6

Section 3