Database Reference
In-Depth Information
A
‡
B
with
id
id
A
B
, we obtain that
identity morphism
id
:
A
‡
B
→
=
T(A
‡
B)
id
=
id
A
‡
B
is well defined identity morphism.
Remark
From the fact that each object
A
B
, obtained by disjoint union, is iso-
morphic to the object
A
‡
B
, so that
A
B
can be equivalently substituted by
the separation-composed object
A
‡
B
, we will use only this second version of
separation-composition in
DB
category (the disjoint union of objects in
DB
will
be explicitly used prevalently for the demonstration purposes).
Corollary 13
The following three isomorphisms for the separation-composition of
objects in
DB
are valid
:
•
0
0
‡
C
.
(
Composition with zero
(
initial and final
)
object
)
C
‡
⊥
C
⊥
•
(
Commutativity
)
A
‡
B
B
‡
A
.
•
(
Associativity
)
A
‡
(B
‡
C)
A
‡
B
‡
C
(A
‡
B)
‡
C
.
Proof
Claim 1. We have
0
0
(
from Lemma
12
)
C
from Lemma
9
)
and
,
C
‡
⊥
C
⊥
0
‡
C
0
⊥
⊥
C(
from Lemma
12
)
C
from Lemma
9
).
with the interpretation
α
such that
C
=
α
∗
(
C
)
,wehavethe
identity morphism
id
C
=
For a given schema
C
α
∗
(
M
CC
)
α
∗
(
:
C
→
C
with
M
CC
=
{
1
r
|
r
∈
C
}∪{
1
r
∅
}
)
.
Let us define, as in the proof of point 4 of Lemma
9
, the morphisms
i
1
=
α
∗
(
M
CC
),α
∗
{
1
r
∅
}
=
id
C
,
⊥
1
:
C
→
C
⊥
0
and
i
2
=
α
∗
(
M
CC
),α
∗
{
1
r
∅
}
=
id
C
,
1
:
0
⊥
C
⊥
→
C.
1
0
0
, we obtain the
Then, by using the isomorphism
id
C
⊥
:
C
‡
⊥
→
C
⊥
composition
i
2
◦
id
C
⊥
1
=
id
C
,
1
◦
id
C
⊥
1
=
id
C
◦
1
1
⊥
id
C
,
⊥
◦⊥
=
id
C
,
1
=
0
⊥
i
2
:
⊥
→
C
‡
C
which is an isomorphism (it has been shown in the proof of point 4 of Lemma
9
)
and so is its inverse
(id
C
⊥
1
)
0
.
◦
i
1
=
i
1
:
C
→
C
‡
⊥
Claim 2. (Commutativity)
A
‡
B
A
B
from Lemma
12
)
A
from point 4 of Lemma
9
)
B
‡
A. (
from Lemma
12
)
B
Let us show that this commutativity is represented by the isomorphism
i
1
=
⊥
1
, id
B
,
id
A
,
1
:
⊥
A
‡
B
→
B
‡
A,
