Database Reference
In-Depth Information
}:
A
α
A
→
B
α
C
Then we define the schema mapping
M
1
={
Φ
with SOtgd
Φ
equal to conjunction
{∀
∈
A
α
A
∈
f
α
∗
(
A
x
(r(
x
)
⇒
r(
x
))
|
r
and
α(r)
⊆
)
=
TA
}
1
r
∈
O(r,r)
|
α(r)
∈
f
⊆
TA
}
A
α
B
with the sketch's mapping
M
1
={
, where
is the
α
-intersection schema (defined in Definition
16
in Sect.
3.1
) with
α
∗
(
A
α
A
=
)
TA
Flux(α,
M
1
)
=
f
.
Then we define the
DB
morphism
α
∗
(
M
1
)
=
and hence its flux is
α
B
α
C
α
∗
(
M
1
)
C
B
.
Λ(f )
=
◦
is
A
:
A
→
=
B
⊗
C
=
This morphism from
A
into
C
B
is uniquely defined by the morphism
f
:
A
⊗
B
→
C
: in fact, its flux is uniquely determined by
Λ(f )
=
is
A
=
α
∗
(
M
1
)
∩
is
A
=
f
=
f.
α
∗
(
M
1
)
◦
∩
TA
}:
B
α
C
→
C
Analogously, we define the schema mapping
M
2
={
Ψ
with SOtgd
Ψ
equal to the conjunction
{∀
∈
B
α
C
α
∗
(
B
α
C
x
(r(
x
)
⇒
r(
x
))
|
r
and
α(r)
∈
)
=
TB
∩
TC
}
with the sketch's mapping
MakeOperads
1
r
∈
O(r,r)
|
α(r)
∈
TB
∩
TC
.
M
2
=
⊗
B
=
α
∗
(
B
α
C
)
→
C
Hence, we define the
DB
morphism
eval
B,C
=
α
∗
(
M
2
)
:
C
B
eval
B,C
=
C
B
which is a monomorphism from the fact that
B
.
Consequently, we obtain for the commutativity of this exponential diagram, that
is,
f
=
TB
∩
TC
=
⊗
id
B
)
=
eval
B,C
∩
id
B
)
=
eval
B,C
∩
( Λ(f )
⊗
eval
B,C
◦
(Λ(f )
⊗
(Λ(f )
⊗
id
B
)
∩
Λ(f )
∩
Λ(f )
=
Λ(f )
(from the fact that
Λ(f )
=
B
⊗
C
∩
TB
=
TB
∩
TC
⊆
C
B
id
B
)
iff
Λ(f )
≈
f
.
Λ
is a bijection because
DB
(A
⊗
B,C)
={
g
|⊥
=
TB
∩
TC
). Thus,
f
=
eval
B,C
◦
(Λ(f )
×
⊆
g
⊆
A
⊗
B
⊗
C
}
=
{
g
|
g
∈
0
K
}
, where
K
is a bounded algebraic sublattice (of closed objects) of the lattice
(
C
,
⊆
)
in Proposition
52
and
=
denotes a bijection, i.e.,
K
={
a
|
a
∈
C
and
a
⊆
DB
(A,B
⊗
C)
=
.Also
DB
(A,C
B
)
=
TA
∩
TB
∩
TC
}
K
, thus
|
DB
(A
⊗
B,C)
|=
DB
(A,C
B
)
|=|
K
|
|
. Consequently,
Λ
is a bijection such that for any
f
∈
DB
(A
⊗
B,C)
,
Λ(f )
=
f
f
.
Let us consider now the complex objects
A
∈
K
, i.e.,
Λ(f )
≈
=
1
≤
j
≤
m
A
j
,m
≥
1,
B
=
1
≤
i
≤
k
B
i
,
k
=
1
≤
l
≤
n
C
l
,n
≥
1 and
C
≥
1. Then
eval
B,C
is the monomorphism
in
C
, obtained by Theorem
6
in Sect.
3.2.5
from the PO relation (from
the isomorphism
C
B
:
C
⊗
B
→
B
),
C
B
⊗
B
C
⊗
B
⊗
⊗
B
≈
C
⊗
B
⊗
B
(from
C
⊗
B
B
)
,
⊕
≈
C
⊗
B
C
in the complete lattice
L
DB
=
(Ob
DB
,
,
⊗
)
(in Proposition
51
),
with
in
={
in
li
:
C
l
⊗
B
i
→
C
l
|
1
≤
l
≤
n,
1
≤
i
≤
k
}
.
