Database Reference
In-Depth Information
(i)
is
O
A
=
is
−
A
◦
(T is
A
)
OP
is
TA
from
(
d
)
in Example
21
◦
is
−
A
◦
(id
TA
)
OP
=
◦
id
TA
(id
TA
)
OP
(
inverted arrow of an identity arrow is the same identity arrow
)
is
−
A
◦
=
is
−
A
.
Analogously (here
B
is replaced by
A
and
A
by
TA
),
(ii)
is
−
A
◦
=
id
TA
=
is
−
A
OP
TA
◦
T is
−
A
OP
is
−
1
=
is
A
from
(
d
)
in Example
21
◦
id
TA
◦
(id
TA
)
OP
is
A
=
(id
TA
)
OP
=
is
A
(
inverted arrow of an identity arrow is the same identity arrow
)
◦
◦
is
A
=
is
−
A
−
1
.
Thus, from (i) and (ii), the label '
OP
' for these isomorphic arrows is equivalent to
inverse-arrow label '
−
1
'.
Let us show the validity of the definition of the functor
S
and
T
1
(f
OP
)
=
id
TA
◦
is
A
=
=
(Tf )
OP
, based on Theorem
2
,for
f
:
A
→
B
:
(iii)
=
is
B
◦
is
−
A
OP
=
is
−
A
OP
(Tf )
OP
f
OP
is
OP
B
f
◦
◦
◦
from
(
i
)
and
(
ii
)
f
OP
is
−
B
:
=
is
A
◦
◦
TB
→
TA.
Thus, by composing on the left with
is
−
1
A
, we obtain
is
−
A
◦
is
−
A
◦
(Tf )
OP
=
is
A
◦
is
−
B
=
is
−
B
=
f
OP
is
−
1
B
f
OP
id
A
◦
f
OP
◦
◦
◦
. By composing on the right with
is
B
,
we obtain
is
−
A
◦
is
−
B
◦
(Tf )
OP
f
OP
f
OP
, that is, the definition
◦
is
B
=
◦
is
B
=
S
1
(f )
f
OP
:
B
→
A
in Theorem
3
is valid.
From Theorem
2
(because of
f
OP
:
B
→
A
,
A
and
B
are exchanged):
T
1
f
OP
=
(
from
(
iii
))
=
is
A
◦
f
OP
is
−
1
B
(Tf )
OP
◦
:
TB
→
TA.
0
Remark
The object
(i.e., empty database instance) is the
zero object
(both
terminal and initial) in
DB
. From any real object
A
in
DB
there is a unique arrow
(which is an epimorphism)
f
=
α
∗
(
M
AA
∅
)
=
α
∗
(
{
⊥
={⊥}
1
0
1
r
∅
}
)
={
q
⊥
}=⊥
:
A
⊥
