Database Reference
In-Depth Information
(f
TΥ
i
=
Υ
i
=
Υ
for every
i
∈
ω
. Consequently,
LimP
×
Υ)
B
×
Υ
Υ
×
B
.
Thus, from the proof of Proposition
48
,
p
A
and
p
Υ
f
id
Υ
=
=
for this pullback di-
0
agram. It is easy to verify that
(
1
−
C
f
)
◦
p
A
=⊥
so that this diagram commutes.
9.1.3 Weak Monoidal Topos
The standard topos is a finitely complete and cocomplete category with subobject
classifier and with exponents. The well know example for the standard topos is
the
Set
category, but also the arrow-category
Set
↓
I
of bundles (fibres) over a set
I
of indices (where an object (a bundle) is a function with codomain equal to
I
)
used as a model for a Boolean algebraic logic. A bundle is a set-theoretic concept
of the sheaf concept, and one of the primary sources of topos theory is algebraic
geometry, in particular the study of sheaves [
11
], and the idea closely tied up with
models of intuitionistic logic. The fundamental theorem of topoi demonstrates that
if a category
D
is any topos and
A
is its object, then the arrow-category
D
↓
A
is
also a topos.
In a standard topos, the following properties of the morphisms are valid:
•
ISOMORPHIC
≡
MONIC
+
EPIC;
•
MONIC.
These properties are not valid in
DB
because it is not a standard topos. Recall that
in every category, we have that ISOMORPHIC
implies
MONIC
EQUALIZER
≡
+
EPIC and that
EQUALIZER
only implies
MONIC, so this is valid in
DB
as well.
In the previous sections of this chapter, we demonstrated that the database cate-
gory
DB
as a kind of
weak monoidal
topos, which differs from the standard topos by
the fact that instead of the standard exponents (with the Cartesian product in the ex-
ponent diagrams) we have the hom-objects which satisfy the “exponent” diagrams
where the Cartesian product '
×
' is replaced by the monoidal tensor product '
⊗
'.
Let us consider some of the properties of this weak monoidal topos.
Proposition 64
The weak monoidal topos
DB
preserves the epic-monic factoriza-
tion of the standard topoi
.
Proof
It is well known that in all topoi, each arrow has an epic-monic factorization.
In fact, for any
f
f
f
B
for a diagram
B
B
we have a pushout
:
A
→
A
colimit (because a topos is cocomplete) with cocone
p
:
B
→
ColimP
and
q
:
B
→
ColimP
, such that
p
B
a
monic arrow in a given topos, then it is an equalizer of this pair of arrows
p,q
◦
f
=
q
◦
f
. In this case, we denote by
im
f
:
f(A)
→
:
B
→
ColimP
, so that in this topos this equalizer is represented by the following
commutative diagram