From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3471 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Characterization of integers as a commutative ring with unit Date: Thu, 26 Oct 2006 10:56:40 +0200 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019326 8906 80.91.229.2 (29 Apr 2009 15:35:26 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:35:26 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Oct 26 10:34:33 2006 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Oct 2006 10:34:33 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Gd5EZ-0007Eu-6s for categories-list@mta.ca; Thu, 26 Oct 2006 10:25:23 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 34 Original-Lines: 30 Xref: news.gmane.org gmane.science.mathematics.categories:3471 Archived-At: For the purposes of defining the data structure of integers in a Coq-like system, I am looking for an _algebraic_ characterization of integers Z as a commutative ring with unit. (The one-element ring is a ring.) Some possible characterizations which I don't much like: 1) Z is the free group generated by one generator. I want the ring structure, not the group structure. 2) Z is the free ring generated by the semiring of natural numbers. This just translates the problem to characterization of the semiring of natural numbers. 3) Z is the initial non-trivial ring. This is no good because "non-trivial" is an inequality "0 =/= 1" rather than an equality. 4) Let R be the free commutative ring with unit generated by X. Then Z is the image of the homomorphism R --> R which maps X to 0. This is just ugly and there must be something better. I feel like I am missing something obvious. Surely Z appears as a prominent member of the category of commutative rings with unit, does it not? Best regards, Andrej