Re: Grothendieck: more complete URL

[Colin McLarty <colin.mclarty@case.edu>]

Certainly it depends on how the axioms are phrased.  And I only said I
would not be surprised!  When I wrote that, I had the idea that in
Tohoku he phrased AB5 for all filtered colimits of objects, but I see
it is in fact phrased for colimits of subobjects of the given one --
which is pretty obvious now that I see it.

I suppose the issue for constructivizing the proof then comes from AB3
on arbitrary sums together  AB4-5 on their properties.   It would
depend sensitively on how "arbitrary sums" are defined.

colin





2010/9/9 Toby Bartels <toby+categories@ugcs.caltech.edu>:
> Colin McLarty wrote:
>
>>I would not be surprised if Grothendieck's Tohoku proof that all AB5
>>categories have enough injectives is straightforwardly constructive --
>>with the unhelpful limitation that from a constructive viewpoint
>>nearly no categories satisfy the AB5 axioms.  Especially the last
>>axiom, 5, requires completeness in a strong sense which is tailored to
>>make each step of the classical Baer proof work.
>
> Does this depend on how the axiom is phrased?
> An elementary version says that an Ab5 category
> is an cocomplete abelian category such that,
> given any object X, subobject A of X,
> and directed system (B_i)_i of subobjects of X,
> A \cap \sum_i B_i = \sum_i (A \cap B_i).
> The obvious proof that modules form an Ab5 category
> works in the internal language of any topos with NNO.
>
> It is less clear to me whether it follows from this
> that filtered colimits preserve exact sequences,
> which is the more abstract form of axiom 5.
>
>
> --Toby
>


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