Re: disjoint_coproducts_bis_?

Dear Eduardo,

Thank you for your clarifications.

The fact that you did not use the language of indexed categories or
fibrations in formulating your statement, and that you referred to specific
objects and epimorphic families involving the site CC, made me think that
you assumed CC to be a site in the standard sense, rather than a site
internal to SS, and hence I answered accordingly. My argument certainly does
not apply in the case of a site internal to SS; in this situation, one
should appropriately formalize the statement in the higher-order internal
logic of the topos in question (in which case, the resulting sentence
becomes valid in this logic) and use the machinery of indexed categories or
fibrations to 'externalize' it.

Concerning your last question, I would like to remark that, in general, if
one is able to interpret a statement M involving certain semantic notions or
constructions as the semantic interpretation of a syntactic statement S in a
system admitting a soundness theorem for such kind of interpretations, then,
if S can be established within the system by purely syntactic means, one can
rely on the soundness theorem to 'canonically' deduce M. Going through a
syntactic system to lift results from a given context (playing the role of a
'standard model' of the system that one keeps in mind when working in it) to
a more general one is a most effective (and conceptually satisfying) method,
as the history of our subject, as well as its most recent developments,
show. For instance, following the discovery of the internal language of a
topos, many categorical results about toposes have been established or
interpreted as semantic interpretations of syntactic statements provable in
the internal logic. In the case of Diaconescu's Theorem, the route which has
first been taken to establish it over a general base topos has not been that
of designing a 'syntactic' version of it, but rather that of developing
appropriate generalizations of the various notions involved in it within the
framework of indexed categories/fibrations. However, I think that it would
be feasible to develop a logical system for doing category theory over a
base topos; in this respect, the book "Relative Category Theory and
Geometric Morphisms: A Logical Approach" (Oxford Logic Guides) by J. Chapman
and F. Rowbottom might be relevant - its abstract reads as follows: 

"Topos theory provides an important setting and language for much of
mathematical logic and set theory. It is well known that a typed language
can be given for a topos to be regarded as a category of sets. This enables
a fruitful interplay between category theory and set theory. However, one
stumbling block to a logical approach to topos theory has been the treatment
of geometric morphisms. This book presents a convenient and natural solution
to this problem by developing the notion of a frame relative to an
elementary topos. The authors show how this technique enables a logical
approach to be taken to topics such as category theory relative to a topos
and the relative Giraud theorem. The work is self-contained except that the
authors presuppose a familiarity with basic category theory and topos
theory. Logicians, set and category theorists, and computer scientist
working in the field will find this work essential reading."

Best regards,
Olivia   

 


> -----Messaggio originale-----
> Da: Eduardo J. Dubuc [mailto:edubuc@dm.uba.ar]
> Inviato: giovedì 25 luglio 2013 23:22
> A: Categories list
> Oggetto: categories: disjoint_coproducts_bis_?
> 
> Hi, first many thanks to all who answered my question (in the list and in
> mathoverflow). I feel now the need to further clarify my question which I
> thought was clear enough.
> 
> A) Three answers respond to the intended interpretation of my question and
> say the same, that the arguing is correct.
> 
> 1) Looks valid to me: I would possibly expand it to:
> COPRODUCT_{all f: C ---> X, all C in CC} FC  ---> FC, is an epimorphism,
> therefore for any a: * ---> FX there exists
> c: * ---> COPRODUCT_{all f: C ---> X, all C in CC} FC lifting a, and since
> coproducts in SS are disjoint, c factors through some component FC and
> you're done. ? David Roberts.
> 
> It is mysterious however for what stands the symbol "*" ?
> 
> 2) This argument looks OK as long as everything is understood to be in the
> internal logic of SS. In particular, the implicit existential quantifiers
"there
> exists C and there exists c" should be understood internally (i.e., as
local
> existence); similarly for the quantifier "for some i \in I". Andreas
Blass.
> 
> This is very clear.
> 
> 3) Your statement is valid internally in SS, that is once formalized in
the
> internal language of the topos SS; this can be done in geometric logic, by
> considering a (possibly infinitary) disjunction over all the arrows f: C
---> X for
> C in CC (interpreted by the arrows Ff in SS) and existential
quantifications.
> Olivia Caramello.
> 
> This seems somehow less clear, the wording  "(possibly infinitary)
> disjuntions" opens the door for a misunderstanding, and should be
> explained.
> 
> Well, I had some other private answers on the negative, and also in the
form
> "yes and no". All these answers do not interpret my question the way it
was
> intended. They talk about fibrations, coverings, atoms, etc, nothing to do
> with my question. They interpret my question essentially by an external
> view, while it is purely internal.
> 
> Now, two new postings to the list made me think it is pertinent to clarify
and
> expand the question:
> 
> Answering Olivia 3), Thomas  Streicher writes:
> 
> 4) Since CC is internal to SS which is assumed as different from Set it
doesn't
> make sense to consider an infinite disjunction over all arrows
> f: C --> X for C in CC.   Thomas
> 
> And Olivia answers:
> 
> 5) It seems to me that Eduardo assumed CC to be a site for EE in the
classical
> sense, i.e. not a site internal to SS but to Set (since he wrote that "CC
has
> objects, and that these objects are objects of EE which are generators in
the
> sense that given any X in EE,  the family of all f: C ---> X, all C in CC,
is
> epimorphic"); so an infinite disjunction makes sense in this case. Olivia
> 
> Well, it seems to me things are now mixed up, and I will intent to
clarify,
> expecting also to be not quite right.
> 
> First, I said in my original posting and in mathoverflow:
> 
> "As usual in the literature (Joyal-Tierney, Moerdijk, Bunge, and many
> more) consider that CC has objects, and that these objects are  objects of
EE
> which are generators in the sense that given any X in EE,  the family of
all f: C
> ---> X, all C in CC, is epimorphic."
> 
> "As usual in the literature", Olivia miss this point when she answers
Thomas.
> Technically speaking I am assuming CC to be an internal site in SS. My
> question is purely refered to the validity in the internal language of the
topos
> SS.
> 
> I give two examples:
> 
> 6) "Thus, we take the point of view that  an arbitrary, but fixed,
> (elementary) topos is our basic universe of sets, We work in this universe
as
> we would in naive set theory, except that, of course, we cannot use the
> axiom of choice, or the law of excluded middle. This has been shown to be
> correct by various authors (e.g. Boileau-Joyal).
> Joyal-Tierney, An extension of the galois theory of grothendieck, Memoirs
> 309."
> 
> 7) "Throughout this paper SS denotes a fixed base topos, all toposes are
> assumed to be Grothendieck toposes over SS, and all geometric morphisms
> are taken to be bounded. Moerdijk, Continuos fibrations and inverse limits
of
> toposes  Compositio Mathematica 58."
> 
> Then, in these two papers  their sites happily have objects, their objects
> happily have elements (as if they were sets, not externally in the sense
of
> sections from an object in the site), etc etc. But one has to work
carefully,
> see for example the definition of open site in 6).
> 
> For the validity of all this only (e.g. Boileau-Joyal) is needed (no
theory of
> indexed categories or fibrations, etc).
> 
> Then, thats it !, the arguing is correct !, why bother more ?, as answers
1) 2)
> and 3) point out.
> 
> Well, it seems I still need some more reassuring facts.
> 
> I quote a (private, but since then Thomas has written to the list, I feel
he
> would not object) knowledgeable answer by Thomas
> 
> 8) my reply would be that given a g.m.  F -| U : EE -> SS  this
corresponds to a
> fibration P_F of toposes over SS (P_F is obtained by pulling back the
> codomain fibration along F). In the internal language of SS one can speak
> about the fibration P_F only in a restricted way.
> 
> 1) Does it make sense to take
> 
> E = COPRODUCT_{all f: C ---> X, all C in CC} FC ?
> 
> We have g: E ---> FX an epimorphism, so we can take c in E such that a =
g(c).
> Well, the g.m. F -| U : EE -> SS  being bounded is already equivalent to
the
> existence of a generic family G -> FI. Since P_F is a locally small
fibration
> (because U has a right adjoint) by Th.10.5 of www.mathematik.tu-
> darmstadt.de/~streicher/FIBR/FibLec.pdf your claim 1)follows. See also
> footnote 15 on p.78 of loc.cit. Maybe you find
> pp.51-52 of Bunge and Funk's book more illuminating in this respect.
> 
> Then we would need the validity of:
> 
> 2) Given x in COPRODUCT_{i in I} S_i , then x in S_i for some i in I.
> Depends on how you read this. If you read it externally for a Grothendieck
> topos SS over Set it is wrong if SS is not connected. But the answer is
trivially
> YES if you think of (S_i)_{i \in I} as a map S
> -> I in SS. But for general toposes SS there is no other meaning of
> family of objects in SS indexed by I.
> 
> Then, this justify that the arguing is correct, according with 1) and 2).
> 
>   From this I figured out and wrote (privately to Thomas)
> 
> 9) Thanks for your answer, it confirms that the arguing is correct.
> Given an internal site CC in SS, the expression {all f: C ---> X, all C in
CC}
> actually determines an object in SS which legitimates the index in the
> coproduct expression COPRODUCT_{all f: C --->  X, all C in CC} FC, then
the
> answer for 2) is trivially yes as you say.
> 
> and he answered "right!".
> 
> But he also writes later in the Mail:
> 
> 10) The problem rather is that in (the language of) SS you can't quantify
over
> such families (nor can you quantify over objects of SS in SS). Well, there
are
> possibilities arising from Algebraic Set Theory but that means that you
work
> in a category of classes constructed from SS.
> In any case reasoning "like in Set" doesn't work for arbitrary base
toposes.
> 
> How we should understand this ?. Luckily in my question there is no
> quantification of this sort. I understand that you can quantify (abusing
> notation) over objects of SS when these objects are objects of an internal
site
> CC, as it is done in 6) and 7).
> 
> So, this seems to be no objection to the validity of the arguing in my
original
> question.
> 
> I am really sorry if the experts find this long discussion banal, but I am
> posting it since I know it would be useful to many interested non experts
in
> the subject.
> 
> And now, I rise a new question to the list:
> 
> B)
> 
> 1) To do many mathematical reasonings and constructions over an arbitrary
> base topos, in several places in the literature classical category theory
(pull-
> backs, subobject classifiers, colimits, effective epimorphisms, etc etc)
is
> painfully and carefully used  (e.g. the books Topos theory, Vol. 10,
Academic
> Press, London, 1977, or Sheaves in Geometry and Logic, Springer, 1992).
> 
> Why bother ?
> 
> Take for example Diaconescu Theorem, Can we reason as follows ?:
> 
> 2) This theorem needs no proof, since the proof of the statement with the
> topos of sets as a base topos (SGA4 expose IV, Proposition 4.9.4, p356,
SLN
> 269) can be done with an arbitrary base topos since "we work in this
universe
> as we would in naive set theory". Just check that no use is made of
choice,
> the excluded middle, quantification over "large"
> families or any other non kosher things.
> 
> e.d.
> 
> 


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]