Topos theory: axiom of choice implies a topos is Boolean
Rotwang
Logic/ and am stuck on how to fill in some gaps in a proof. The author
claims that, if a topos E has the property that every epic arrow has a
right inverse then E is Boolean, i.e. every monic f: a -> d has a
complement in sub(d), the lattice of subobjects of d. To show this, let
d + d be the coproduct of d with itself, and i_1, i_2: d -> d + d the
corresponding injections. Let g: d + d -> b be the coequaliser of i_1 o
f and i_2 o f: a -> d + d:
i_1 o f g
a -----> d + d -----> b
----->
i_2 o f
and let s: b -> d + d be a right inverse for g. Now let j_1: c_1 -> d be
the pullback of i_1 along s:
j_1
c_1 -----> d
| |
| | i_1
| |
v v
b -----> d + d
s
and similarly let j_2 be the pullback of i_2 along s. Finally, define j:
c -> d as the intersection of j_1 and j_2, i.e. j = j_1 o p_1 = j_2 o
p_2, where
p_1
c -----> c_1
| |
p_2 | | j_1
| |
v v
c_2 -----> d
j_2
is a pullback. Apparently j is a complement for f in sub(d). Proving
this amounts to showing that the domain of the pullback of f and j is
initial, and also that the coproduct map [f,j]: a + c -> d is epic. But
I have no idea how to prove either of these things. Can anybody give me
some hints?
Marc Olschok
Did the author already show that coproducts are disjoint and universal in
a topos? In this case assemble your maps as follows
p -----> c c <----- p
| | | |
| |p_1 p_2| |
| v v |
| c_1 -----> b <----- c_2 |
| | u_1 | u_2 | |
| j_1| |s |j_2 |
v v v v v
a -----> d -----> d+d <----- d <----- a
f i_1 i_2 f
where all rectanges are pullbacks. Observe that in that diagram
the row c_1 --> b <-- c_2 is again a coproduct.
In order to check that p is initial, check that the two compositions
p --> c --> c_1 --> b and p --> c --> c_2 -->b
are in fact equal, and hence there is a map from p to b which factors
through both coproduct inclusions u_1 and u_2
I do not see the second part right now.
--
Marc
Rotwang
>
> Did the author already show that coproducts are disjoint and universal in
> a topos?
No, but since reading your reply I've figured out proofs of the relevant
cases.
> In this case assemble your maps as follows
>
> p -----> c c <----- p
> | | | |
> | |p_1 p_2| |
> | v v |
> | c_1 -----> b <----- c_2 |
> | | u_1 | u_2 | |
> | j_1| |s |j_2 |
> v v v v v
> a -----> d -----> d+d <----- d <----- a
> f i_1 i_2 f
Wow, that looks like it took a while to draw. I'm very grateful for the
effort, thanks.
> where all rectanges are pullbacks. Observe that in that diagram
> the row c_1 --> b <-- c_2 is again a coproduct.
>
> In order to check that p is initial, check that the two compositions
>
> p --> c --> c_1 --> b and p --> c --> c_2 -->b
>
> are in fact equal, and hence there is a map from p to b which factors
> through both coproduct inclusions u_1 and u_2
Excellent, thank you.
By the way, in proving the facts you mentioned above I had to make
repeated use of two "fundamental facts" that Goldblatt states without
proof, namely that the pullback of any epic map is itself epic, and that
coproducts preserve pullbacks in the following sense: if both squares of
f f'
a -----> d <----- a'
| | |
g | k | | g'
| | |
v v v
b -----> c <----- b'
h h'
are pullbacks, then so is
[f,f']
a + a' --> d
| |
g + g' | | k
| |
v v
b + b' --> c
[h,h']
Do you know where I might find proofs of these two facts online, or if
not, do you happen to know whether they're proved in the book by Mac
Lane and Moerdijk (which I'm thinking of buying)?
Marc Olschok
One can phrase this the other way: pulling back the
coproduct diagram b --> c <-- b' along k: d --> c
produces a coproduct diagram a --> d <-- a'.
This is what I meant by "coproducts are universal".
> Do you know where I might find proofs of these two facts online, or if
> not, do you happen to know whether they're proved in the book by Mac
> Lane and Moerdijk (which I'm thinking of buying)?
I do not remember the exact location, but they are proved there
(as perhaps in almost every book on topos theory except Goldblatts :-).
In fact they show that pullbacks preserve all colimits by exhibiting
"pulling back along a map" as a suitable left adjoint.
Actually, once you have this fact available, you can also see that
it is enough to prove the claim (that every mono has a complement)
for the special case of true: 1 --> Omega because for a general
monic f: a --> d you can then pull back that coproduct along
the characteristic map k of f
f
a -----> d <----- a'
| | |
| k| |
v v v
1 ---> Omega <--- z
true
(in fact the complement of true must be false: 1 --> Omega).
I do not know if this makes the proof any easier.
--
Marc
Rotwang
I think I've figured out how to show that f u j = 1 (I'll omit
subscripts on identity arrows for brevity). Firstly, since f u j = (f u
j_1) n (f u j_2) it suffices to show that 1_d factors through f u j_1
and f u j_2. Now observe that, by the aforementioned fact about
pullbacks of coproducts, the following is a pullback:
j_1 + j_2
c_1 + c_2 -----> d + d
| |
| | [i_1, i_2] = 1
| |
v v
b ---------> d + d
s
and so it follows that the left arrow, let's call it k, is an
isomorphism, with (j_1 + j_2) o k = s. Defining g' = k^{-1} o g, we find
that g' is a coequaliser for i_1 o f and i_2 o f, with j_1 + j_2 a left
inverse for g'. Moreover, since [1,1] o i_1 o f = [1,1] o i_2 o f,
[1,1]: d + d -> d factors through g', and right-composing the resulting
factorisation with j_1 + j_2 shows that
[j_1, j_2] o g' = [1,1]: d + d -> d.
Now let F = (1 + j_2) o g' o i_1: d -> c_1 + d. The following diagram is
a pullback:
1 + f
c_1 + a -------> c_1 + d
| |
| | [T_{c_1}, chi]
| |
v v
I -----------> Omega
T
where I is a terminal object, T: I -> Omega is a subobject classifier,
T_e denotes the composite T o !: e -> I -> Omega for any object e and
chi is the character of f. Then
[T_{c_1}, chi] o F = [T_d, chi] o (j_1 + j_2) o g' o i_1
but [T_d, chi] o i_1 o f = T_a = [T_d, chi] o i_2 o f, so there exists
h: c_1 + c_2 -> Omega such that [T_d, chi] = h o g'. So
[T_{c_1}, chi] o F = h o g' o (j_1 + j_2) o g' o i_1
= h o g' o i_1
= [T_d, chi] o i_1 = T_d
so that F factors through 1 + f, say F = (1 + f) o G for some G: d ->
c_1 + a. But then
[j_1, f] o G = [j_1, 1] o (1 + f) o G
= [j_1, 1] o (1 + j_2) o g' o i_1
= [j_1, j_2] o g' o i_1
= [1,1] o i_1 = 1
so that 1 ( = 1_d) factors through [j_1, f] which itself factors through
j_1 u f. An almost identical proof shows that 1 factors through j_2 u f,
as required.
Rotwang
>
> [...]
>
> One can phrase this the other way: pulling back the
> coproduct diagram b --> c <-- b' along k: d --> c
> produces a coproduct diagram a --> d <-- a'.
>
> This is what I meant by "coproducts are universal".
>
>> Do you know where I might find proofs of these two facts online, or if
>> not, do you happen to know whether they're proved in the book by Mac
>> Lane and Moerdijk (which I'm thinking of buying)?
>
> I do not remember the exact location, but they are proved there
> (as perhaps in almost every book on topos theory except Goldblatts :-).
I gather that Goldblatt differs from other texts in that it says very
little about how topoi arise in algebraic geometry and is instead
focussed on the interplay between topos theory and logic. This suits me
since I'm not interested in AG but am learning about topos theory for
applications to the foundations of quantum mechanics, but the author
does have a frustrating habit of referring the reader to external
sources for proofs.
> In fact they show that pullbacks preserve all colimits by exhibiting
> "pulling back along a map" as a suitable left adjoint.
>
> Actually, once you have this fact available, you can also see that
> it is enough to prove the claim (that every mono has a complement)
> for the special case of true: 1 --> Omega because for a general
> monic f: a --> d you can then pull back that coproduct along
> the characteristic map k of f
>
> f
> a -----> d <----- a'
> | | |
> | k| |
> v v v
> 1 ---> Omega <--- z
> true
>
> (in fact the complement of true must be false: 1 --> Omega).
>
> I do not know if this makes the proof any easier.
Thanks very much for your reply.
Marc Olschok
> >> Do you know where I might find proofs of these two facts online, or if
> >> not, do you happen to know whether they're proved in the book by Mac
> >> Lane and Moerdijk (which I'm thinking of buying)?
> >
> > I do not remember the exact location, but they are proved there
> > (as perhaps in almost every book on topos theory except Goldblatts :-).
>
> I gather that Goldblatt differs from other texts in that it says very
> little about how topoi arise in algebraic geometry and is instead
> focussed on the interplay between topos theory and logic. This suits me
> since I'm not interested in AG but am learning about topos theory for
> applications to the foundations of quantum mechanics, but the author
> does have a frustrating habit of referring the reader to external
> sources for proofs.
I find it very unfortunate that Goldblatt introduces functors and
adjoints so very late in the book, thereby not having these clarifying
tools available earlier. So he is forced to postpone important
parts of the theory or refer to external sources.
For example, he does give the needed Theorem (and sketch of proof), that
every map f: a --> b in a topos E induces a functor S_f: E/a --> E/b
which has a right adjoint f*: E/b --> E/a ("taking pullback along f")
and that this f* in turn has a right adjoint P_f: E/a --> E/b.
But is comes only in section 15.3.
I think the Mac Lane / Moerdijk book might be a good choice for you.
Also, the small book by Kock and Wraith is perhaps still available
from <http://www.imf.au.dk/da/forskning/publikationer/instituttets-serier/lecture-notes-series/> (although the resellers website seems to be in flux).
--
Marc
Rotwang
>
>> [...]
>
> I think the Mac Lane / Moerdijk book might be a good choice for you.
> Also, the small book by Kock and Wraith is perhaps still available
> from <http://www.imf.au.dk/da/forskning/publikationer/instituttets-serier/lecture-notes-series/> (although the resellers website seems to be in flux).
Thanks.
James Dolan
rotwang <sg...@hotmail.co.uk> wrote:
|Marc Olschok wrote:
|>
|> [...]
|>
|> One can phrase this the other way: pulling back the
|> coproduct diagram b --> c <-- b' along k: d --> c
|> produces a coproduct diagram a --> d <-- a'.
|>
|> This is what I meant by "coproducts are universal".
|>
|>> Do you know where I might find proofs of these two facts online,
|>> or if not, do you happen to know whether they're proved in the
|>> book by Mac Lane and Moerdijk (which I'm thinking of buying)?
|>
|> I do not remember the exact location, but they are proved there (as
|> perhaps in almost every book on topos theory except Goldblatts :-).
|
|I gather that Goldblatt differs from other texts in that it says very
|little about how topoi arise in algebraic geometry and is instead
|focussed on the interplay between topos theory and logic.
i thought that that's how goldblatt _fails_ to differ from other texts
(more specifically, from other english-language texts with which i'm
familiar).
|This suits me since I'm not interested in AG but am learning about
|topos theory for applications to the foundations of quantum
|mechanics,
hmm. it seems to be a fairly well-kept secret that the way that
toposes arise in algebraic geometry is by means of the interplay
between topos theory and logic- that an "algebraic stack" is
essentially a moduli stack of models of a theory expressed in a
certain logic ("algebraic-geometric logic"), and that the various
toposes associated to the algebraic stack are essentially moduli
stacks of models of essentially the same theory, but expressed in a
different logic ("geometric logic"). the concepts of "moduli stack"
and of "classifying topos" are more or less re-inventions of the same
concept (except that the former is more associated with
algebraic-geometric logic and the latter with geometric logic).
it's likely that interesting applications of topos theory to the
foundations of quantum mechanics would tie in strongly with the
relationship between algebraic-geometric logic and geometric logic.
--
Rotwang
> in article <hnj3tj$da3$1...@news.eternal-september.org>,
> rotwang <sg...@hotmail.co.uk> wrote:
> |
> |
> |I gather that Goldblatt differs from other texts in that it says very
> |little about how topoi arise in algebraic geometry and is instead
> |focussed on the interplay between topos theory and logic.
>
> i thought that that's how goldblatt _fails_ to differ from other texts
> (more specifically, from other english-language texts with which i'm
> familiar).
You may be right. Goldblatt is the only topos theory book I've tried
reading, and my "I gather" was based on having read, and probably
inadequately digested, some reviews a while back.
> |This suits me since I'm not interested in AG but am learning about
> |topos theory for applications to the foundations of quantum
> |mechanics,
>
> hmm. it seems to be a fairly well-kept secret that the way that
> toposes arise in algebraic geometry is by means of the interplay
> between topos theory and logic- that an "algebraic stack" is
> essentially a moduli stack of models of a theory expressed in a
> certain logic ("algebraic-geometric logic"), and that the various
> toposes associated to the algebraic stack are essentially moduli
> stacks of models of essentially the same theory, but expressed in a
> different logic ("geometric logic"). the concepts of "moduli stack"
> and of "classifying topos" are more or less re-inventions of the same
> concept (except that the former is more associated with
> algebraic-geometric logic and the latter with geometric logic).
I'm afraid I don't know what much of this means.
> it's likely that interesting applications of topos theory to the
> foundations of quantum mechanics would tie in strongly with the
> relationship between algebraic-geometric logic and geometric logic.
Perhaps. Are you familiar with Prof. Chris Isham's work on topos theory
and QM? That's what I'm specifically trying to understand. He suggested
I start by reading Goldblatt, though I'm open to other suggestions of
course.
Ken Pledger
Rotwang <sg...@hotmail.co.uk> wrote:
> Hi all, I'm reading Goldblatt's /Topoi: The Categorial Analysis of
> Logic/ and am stuck on how to fill in some gaps in a proof....
Sorry to be late responding to this. Rob Goldblatt is in the
room next to me; but your question would come better from you than from
me. Just e-mail him: <rob.go...@msor.vuw.ac.nz>. Authors are
usually quite pleased when someone reads their work seriously.
Ken Pledger.
Rotwang
Well I managed to figure out the answer to the question in this thread
(with copious help from Marc Olschok). But I do have some other
questions about the book which I've been considering asking the author
about, and I guess I'll do so if you don't think he'll mind. Thanks.