Re: Reply to Eduardo Dubuc

["Eduardo J. Dubuc" <edubuc@dm.uba.ar>]

On 26/07/13 17:08, Thomas Streicher wrote:
>>> 2) If on the other hand you work in a topos EE that is bounded
>>> over SS, then you cannot work "as in Sets" concerning
>>> constructions in EE that involve SS. Here it is necessary to
>>> resort to either the "teoria delle categorie sopra un topos di
>>> base" (indexed categories) or to the theory of fibrations.
>>>
>>> [[1===1]]
>>> Concerning your question, let me point out that, although you
>>> pretend to work entirely inside SS, you do not, as your
>>> construction involves EE. It certainly makes sense, since EE is
>>> locally small, and CC is small ( meaning internal to SS). What I
>>> want to warn you about is how you proceed from there without
>>> resorting to EE as a bounded SS- topos.
>
> I fully subscribe to this, That's what I also wanted to say but
> formulated less clearly.
>
> The saying that "toposes correspond to naive set theory without
> principle and excluded middle" is right only if "naive set theory"
> is identified with higher order logic. But in "naive category
> theory" you all the time have to quantify over families of objects
> and morphisms of a category where these collections don't form sets.
> In particular, you have to quantify over all objects of the base
> topos which you can't do inside the base topos.
>
> As Marta has said one has to resort to fibered/indexed reasoning
> which also cannot be (fully) expressed in the internal language of
> the base topos.
  >
  > [[2===2]]
  > As I wrote to Eduardo in a non-public mail I consider
> the "naive set theory" style arguments one often find in the
> literature as kind of "blueprints" for the precise fibered/indexed
> arguments.
>
> An alternative is using Algebraic Set Theory which allows one to
> build around every topos EE a category of classes in such a way that
> EE appears as internal to it. This, among other things, is the aim of
> a recent paper by Awodey, Butz, Simpson and myself which has is to
> appear at APAL and a preliminary version of which can be obtained
> from Alex's homepage
> (http://homepages.inf.ed.ac.uk/als/Research/Sources/set-models.pdf).
>
> Sorry for speaking pro domo but it is relevant here when one wants
> to fully stay within an internal language.
>
> Thomas

Thanks Marta an Thomas, I am learning a lot !.

I would like to comment in the items marked [[1===1]] and [[2===2]] of
your answers. It seems to me now that the argument in my question does
not need any theory of indexing categories.
See, concerning [1===1] above I can say:

My construction does not involve EE. It involves an internal site CC in
SS, a functor CC ---> SS, a coproduct in SS indexed by an object in SS,
and a SINGLE object X in EE, which is sheaf CC^op ---> SS. All this
involves ONLY SS, and no forbiden quantifications are used. So the
internal logic of SS should suffice.

Concerning [2===2], you are probably right in many cases, precisely
cases that I distrust because I feel the authors are not carefully
enough (this due to my ignorance together with a tendency to be as Saint
Thomas, "have to see to belive"). But in other cases not. For example,
the entire paper Joyal-Tierney, An extension of the galois theory of
grothendieck, Memoirs 309, is no "blue print" for nothing, it is in
final form, very careful, and entirely justified (even their change of
base) without any need of fibered/indexed arguments, as they say, (e.g.
Boileau-Joyal) suffices.

For example, they consider p: EE ---> SS, and say p_* sends sup-lattices
to sup-lattices, they consider a left adjoint  p^# (between the
categories of sup-lattices) and stablish an isomorphism

                Hom(L, p_*(M)) = p_*Hom(p^#(L), M)  in  SS

and say "expresses the (strong) adjointness p^# --| p_*" (page 44).

They use "strong", no mention at all to "indexed adjoint", and this
isomorphism is just a definition of strong.

But, is not true that a topos p: EE ---> SS is canonically indexed and
that for many things you can proceed tacitly without need to mention any
theory of indexed categories ?. Even for constructions in EE ?. For
example, a family in EE indexed by I in SS is just an arrow X ---> p*I,
and the COPRODUCT_{i \in I} X_i in EE is just X.

Please, do not think I am against fibered/indexed arguments, I can not
be either against or in favor, since I do not know the theory.

After your answers I understand now the theory is useful when you need
to use quantifications not avaiable in the internal logic of a topos and
other things of this sort.

Best  Eduardo.



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