Database Reference
In-Depth Information
(f
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
Search WWH ::




Custom Search