Database Reference
In-Depth Information
is a pullback square
.
Thus
,
DB
is a kind of a monoidal elementary topos
.
Proof
From Proposition
55
in Sect.
8.1.5
dedicated to algebraic database lattice, we
ω
Υ
(
ω
Υ
)
have
Ω
)
. Diagram (
Ω
) above is a special
case of the class of pullbacks defined by Corollary
27
because
C
f
:
=
Υ
=
Υ
∪
=
Υ
∪
(
Υ
···
Ω
satisfies
the condition that for each its ptp arrow
C
f
ij
:
A
j
→
Υ
i
=
Υ
,
TA
j
⊆
TΥ
i
=
T
Υ
=
Υ
A
→
=
A
∈
Ob
DB
A
(from Proposition
26
in Sect.
3.2.5
). Thus,
Lim(C
f
)
=
A
×
C
f
where
C
f
f
(f
:
B
→
A
is a monomorphism
)
TB
B
and hence
Lim(C
f
)
=
A
∈
Ob
DB
A
⊂
Υ
A
we have that
f
A
×
B
. For a monomorphism
f
:
B
→
τ
−
1
J(C
f
)
τ
−
1
J(C
f
)
in
B
and hence, from Corollary
27
,
p
Υ
in
B
TB
=
=
.
Consequently, for each ptp monomorphism
f
ij
:
B
i
→
A
j
with
j
=
σ(i)
,we
obtain the following pullback square where
C
f
ij
f
ij
TB
i
B
i
:
(
ω
⊥
1
1
)
Note that the logic dual (width “false” arrow
false
=⊥
∪
:
Υ
→
Ω
)
(
1
−
C
f
)
=
and the complement-characteristic morphism
f
=
(
1
−
C
f
)
, such that
σ(i)
with
f
ji
=
f
TA
j
\
f
ij
}
f
ji
:
{
A
j
→
Υ
i
|
(f
ij
:
B
i
→
A
j
)
∈
,
1
≤
i
≤
k,j
=
,
corresponds to the following pullback diagram
where for
p
A
and
p
Υ
f
id
Υ
=
=
.
false
=∅
, and hence from the proof of Proposition
48
for the
components of
LimP
of the diagram
Υ
We have that
−
C
f
)
false
(
1
Ω
=
i
,
D
ilj
=
A
,for
l
(T A
j
∩⊥
(T A
j
\
f
ji
)
(T Υ
i
∩
f
ji
)
(T Υ
i
\⊥
∪
f
ij
=
f
ij
while
D
jli
=
0
1
)
∪
=⊥
∪
1
)
=
