Hi Andrej, Isn't Z the initial /ring/? 0 isn't initial, as 0=1 holds only in itself (Spec Z is the terminal scheme, Spec 0 the empty scheme, so the initial scheme). -Josh On Thu, 26 Oct 2006, 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