From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6131 Path: news.gmane.org!not-for-mail From: Colin McLarty Newsgroups: gmane.science.mathematics.categories Subject: Re: Grothendieck: more complete URL Date: Thu, 9 Sep 2010 12:07:28 -0400 Message-ID: References: Reply-To: Colin McLarty NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1284075713 23996 80.91.229.12 (9 Sep 2010 23:41:53 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 9 Sep 2010 23:41:53 +0000 (UTC) To: Steve Vickers , Categories list Original-X-From: majordomo@mlist.mta.ca Fri Sep 10 01:41:51 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpy.mta.ca ([138.73.1.139]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OtqkW-00086W-WD for gsmc-categories@m.gmane.org; Fri, 10 Sep 2010 01:41:49 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:50887) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Otqir-0004pT-TJ; Thu, 09 Sep 2010 20:40:06 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Otqik-0005KL-38 for categories-list@mlist.mta.ca; Thu, 09 Sep 2010 20:39:58 -0300 In-Reply-To: <4C88BA4A.5010304@cs.bham.ac.uk> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6131 Archived-At: 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 : > 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/ ]