Database Reference
In-Depth Information
Let us define the set of relational symbols
=
r
i
|
⊆
f
⊆
S
f
=
r
i
|
∈
f
S
r
i
∈R
and
α(r
i
)
∈
Δ(α,
M
AB
)
r
i
∈R
and
α(r
i
)
with
f
)
, so that
f
α
∗
(
)
(analogously, from Def-
inition
16
, for the instance database
TA
we define the schema
(S
TA
,
=
TS
and its schema
C
=
(S
f
,
∅
=
C
=
A
α
A
∅
)
).
Consequently, we define the SOtgd
Φ
by a conjunctive formula
{∀
x
i
(r
i
(
x
i
)
⇒
r
i
(
x
i
))
|
r
i
∈
S
}
.
In fact,
MakeOperads(
{
Φ
}
)
={
1
r
i
∈
O(r
i
,r
i
)
|
r
i
∈
S
}∪{
1
r
∅
}
is a sketch's map-
ping between schemas
C
and
T
A
. Consequently,
α
∗
1
r
i
∈
α
∗
MakeOperads
{
}
=
S
∪{
in
f
OP
=
Φ
O(r
i
,r
i
)
|
r
i
∈
1
r
∅
}
id
R
=
α(
1
r
i
)
:
R
→
R
|
R
=
α(r
i
)
∈
S
⊆
f
∪{
q
⊥
}
:
f
→
TA,
=
with
in
f
OP
=
f
.
Thus, from the duality theorem, this property holds for the epimorphism
in
OP
f
:
f
(which is a dual (inverted arrow) of the monomorphism
in
f
=
in
B
:
f
→
TB
TB
in Lemma
11
) as well.
Consequently, the morphism
T
e
(h
1
;
h
2
)
=
in
OP
f
OP
is well de-
fined in
DB
due to Theorem
1
. It is easy to verify that also
T
e
is a well defined
functor. In fact, for any identity arrow
(id
A
;
g
◦
T(h
2
◦
f)
◦
in
id
B
)
:
J(f)
−→
J(f)
,
T
e
(id
A
;
in
OP
in
OP
id
B
)
=
f
◦
T(id
B
◦
f)
◦
in
f
OP
=
f
◦
Tf
◦
in
f
OP
.
=
in
OP
f
∩
Tf
∩
in
f
OP
=
f
T
e
(id
A
;
Thus, when
f, id
A
, id
B
are simple arrows,
id
B
)
(from
in
OP
→
f
is equal
to the identity arrow
id
f
. It is easy to verify that it holds also when
f, id
A
and
id
B
are complex arrows as well.
For any two arrows
(h
1
;
h
2
)
:
J(f)
−→
J(g)
and
(l
1
;
l
2
)
:
J(g)
−→
J(k)
if all
arrows
f,g,k,h
1
,h
2
,l
1
and
l
2
are simple arrows then
f
=
Tf
=
in
f
OP
=
f
) and, consequently,
T
e
(id
A
;
:
f
id
B
)
=
∩
T
e
(l
1
;
T
e
(h
1
;
T
e
(l
1
;
T
e
(h
1
;
l
2
)
◦
h
2
)
h
2
)
=
k
∩
l
2
∩
g
∩
g
∩
h
2
∩
f
=
k
l
2
)
∩
h
2
∩
f
(
since
h
2
◦
f
=
g
◦
h
1
)
=
k
∩
l
2
∩
g
∩
l
2
∩
∩
h
1
∩
h
2
∩
f
g
(
since
h
2
◦
f
=
g
◦
h
1
)
=
k
∩
l
2
∩
h
2
∩
f
