From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3474
Path: news.gmane.org!not-for-mail
From: Steve Vickers <s.j.vickers@cs.bham.ac.uk>
Newsgroups: gmane.science.mathematics.categories
Subject: Re: Characterization of integers as a commutative ring with unit
Date: Thu, 26 Oct 2006 15:48:52 +0100
Message-ID: <E1GdFef-0002lZ-Jl@mailserv.mta.ca>
NNTP-Posting-Host: main.gmane.org
Mime-Version: 1.0 (Apple Message framework v752.2)
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: ger.gmane.org 1241019328 8922 80.91.229.2 (29 Apr 2009 15:35:28 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:35:28 +0000 (UTC)
To: categories@mta.ca
Original-X-From: rrosebru@mta.ca Thu Oct 26 21:39:05 2006 -0300
Return-path: <cat-dist@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 26 Oct 2006 21:39:05 -0300
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
	(envelope-from <cat-dist@mta.ca>)
	id 1GdFef-0002lZ-Jl
	for categories-list@mta.ca; Thu, 26 Oct 2006 21:33:01 -0300
Original-Sender: cat-dist@mta.ca
Precedence: bulk
X-Keywords: 
X-UID: 37
Original-Lines: 49
Xref: news.gmane.org gmane.science.mathematics.categories:3474
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/3474>

Dear Andrej,

Z is the initial ring with unit. (Doesn't matter whether you require
commutativity.)

It's not clear to me why you felt the need to say "non-trivial" in (3).

Regards,

Steve.

On 26 Oct 2006, at 09:56, Andrej Bauer wrote:

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