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/ ]