Database Reference
In-Depth Information
∩
R
∈
f
and
∀
1
≤
k
≤|
R
|
∀
d
i
∈
π
k
(R)
Va l(d
i
)
|
R
=
T
w
(g)
∩
T
w
(f ).
Consequently,
T
w
(g
◦
f)
=
T
w
(g)
◦
T
w
(f )
. It holds for complex arrows as well (by
considering the composition of their ptp arrows in
f
g
and
).
Let us show that the monomorphism
inc
A
:
T
w
(A)
→
TA
, for a given morphism
α
∗
(
M
AB
)
f
B
, corresponds to the definition of arrows in
DB
category,
specified by Theorem
1
, that is, there is an SOtgd
Ψ
of a schema mapping such that
inc
A
=
=
:
A
→
α
∗
(MakeOperads(
))
.
Let us define the set of relational symbols in the instance-database
T
w
(A)
by
S
T
w
A
={
{
Ψ
}
r
i
|
r
i
∈ R
and
α(r
i
)
∈
T
w
(A)
}
, and its schema
C
=
(S
T
w
A
,
∅
)
, so that
α
∗
(
T
w
(A)
)
for the instance
database
TA
). Then we define the SOtgd
Φ
by a conjunctive formula
∀
=
C
)
(we define analogously the schema
T
A
=
(S
TA
,
∅
x
i
r
i
(
x
i
)
r
i
(
x
i
)
|
S
T
w
A
.
⇒
r
i
∈
In fact,
MakeOperads(
{
Ψ
}
)
={
1
r
i
∈
O(r
i
,r
i
)
|
r
i
∈
S
T
w
A
}∪{
1
r
∅
}
is a sketch's map-
ping from the schema
C
into
T
A
and
α
∗
MakeOperads
{
}
inc
A
=
Ψ
α
∗
1
r
i
∈
S
T
w
A
∪{
1
r
∅
}
=
O(r
i
,r
i
)
|
r
i
∈
=
id
r
i
:
S
T
w
A
∪{
α(r
i
)
→
α(r
i
)
∈
O(r
i
,r
i
)
|
r
i
∈
q
⊥
}
.
Thus,
inc
A
=
T
{
α(r
i
)
∈
O(r
i
,r
i
)
|
r
i
∈
S
T
w
A
}=
T(T
w
(A))
=
(from point 4 of
Proposition
12
)
=
T
w
(A)
and hence
inc
A
:
T
w
(A)
→
TA
is a monomorphism (for
TA
) and, by duality,
inc
O
A
:
the inclusion
T
w
(A)
T
w
(A)
is an epimor-
phism. It is easy to verify that the natural transformations
ξ
and
ξ
−
1
⊆
TA
are well de-
fined.
Analogously to the monad
(T,η,μ)
and comonad
(T,η
C
,μ
C
)
of the endofunc-
tor
T
, we can define such structures for the weak endofunctor
T
w
as well:
(T
w
,T
w
)
Proposition 13
DB
defines the monad (T
w
,η
w
,μ
w
) and the comonad (T
w
,η
w
,μ
w
) in
DB
such that
η
w
=
The weak power-view endofunctor T
w
=
:
DB
−→
−→
−→
ξ
−
1
T
w
is a natural epimorphism and η
w
=
η
C
•
η
:
I
DB
•
ξ
:
T
w
I
DB
is a natural monomorphisms
(
'
•
' is a vertical composition for natural transforma-
−→
−→
T
w
and μ
w
:
tions
),
while μ
w
:
T
w
T
w
T
w
T
w
T
w
are equal to the natural
−→
identity transformation id
T
w
:
T
w
T
w
(
because T
w
=
T
w
T
w
).
Proof
It is easy to verify that all commutative diagrams of the monad and the
comonad are composed of identity arrows.
