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. The classical corollary, that all sheaf categories (i.e. sheaves of modules) have enough injectives, includes saying that all module categories have enough injectives. So it cannot be more constructive than that. I have not looked at constructive forms of the result, or relativizing the whole to any base topos. best, Colin 2010/9/9 Steve Vickers <s.j.vickers@cs.bham.ac.uk>:
Dear Colin,
Can I ask a technical question about foundations here?
Does the "enough injectives" result assume a classical base theory? The classical result for module categories uses choice, and my understanding is that the result for sheaf categories uses Barr covers to make available the classical result.
I wonder if there's an unequivocally constructive formulation.
Regards,
Steve.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]