# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeApr 24th 2010

noticed that the entry was missing, so I created a stub for integer

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeApr 25th 2010

I expanded this a bit, been meaning to write it.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeApr 25th 2010

Thanks, Toby. I edited a bit more. I made the definition as a group again primary and moved the structure of a ring to the second sentence of the article. Have a look to see if you can live with this. Otherwise feel free to edit it again, I am not dogmatic about this, but it looks more logical to me this way.

• CommentRowNumber4.
• CommentAuthorTobyBartels
• CommentTimeApr 26th 2010

Well, I certainly think that being the initial ring is the most important feature, but it’s not a big deal.

• CommentRowNumber5.
• CommentAuthorTobyBartels
• CommentTimeApr 26th 2010

Todd noticed a link and created algebraic integer.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeNov 2nd 2011

Added to integer a pointer to Mike’s HoTT formalization of the integers.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeNov 2nd 2011
• (edited Nov 2nd 2011)

I was puzzled for a second when looking at

Definition succ (z : int) : int :=
match z with
| pos n => pos (S n)
| zero => pos 0
| neg 0 => zero
| neg (S n) => neg n
end.


in Integers.v, but then I realized that “one” is donoted by “0” here.

Why is that?

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeNov 2nd 2011

Why is that?

Ah, I get it.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeNov 2nd 2011

Ah, I get it.

Good. One is denoted by ’pos 0’ where ’pos n’ means ’the positive integer n+1’. It’s perhaps not the prettiest choice and doesn’t need to be enshrined for eternity. (-:

I added a pointer to the more common definition of integers in type theory in the Coq source.

• CommentRowNumber10.
• CommentAuthorzskoda
• CommentTimeNov 23rd 2016
• (edited Nov 23rd 2016)

$1.$ the link

at integer seem not to work.

$2.$ The statement in the idea section that the ring of integers is obtained as the Grothendieck group of the commutative monoid $\mathbb{N}$ is not really honest, this is not the common idea of integers. Grothendieck group construction is as default for one commutative operation (despite versions for categories etc.) and it is not the way either historically was discovered nor that classroom teaching ever does it. Instead, one considers natural numbers as (linearly) ordered rig, and then one makes a negative copy with opposite order and extends the structure to a structure of an ordered ring, doing case by case (multiplying negative and positive, two negatives etc.). This is cumbersome in the sense of many cases to check (especially if one is to prove associativity and alike), but there is an intuition attached to each of the cases appearing in the description (negative values as debt etc.) and it somehow works better in mathematical education. One of the reasons is that it avoids the classes of equivalence (the artifact of the Gorthendieck group approach), which are a difficult concept for pupils, more difficult than the case by case learning (disjoint unions are easier than quotients).

• CommentRowNumber11.
• CommentAuthorTodd_Trimble
• CommentTimeNov 23rd 2016
• (edited Nov 23rd 2016)

As an expression of an nPOV – not necessarily coinciding with first encounters in the classroom – I think it’s perfectly honest.

Even with the default meaning of one binary operation (referring to a left adjoint from commutative monoids to abelian groups), an nPOV counter is that the extension to rigs/rings just comes along for the ride. The point being that this left adjoint preserves the symmetric monoidal structure, hence takes the monoidal unit for commutative monoids $\mathbb{N}$ to the monoidal unit for abelian groups $\mathbb{Z}$, and monoidal units for symmetric monoidal structures automatically carry (commutative) monoid structures w.r.t. the monoidal product, which are rigs in one case and rings in the other. This leads to a neat description of the “Grothendieck ring” construction of a rig $R$ as just $\mathbb{Z} \otimes_\mathbb{N} R$.

• CommentRowNumber12.
• CommentAuthorzskoda
• CommentTimeNov 23rd 2016

Isn’t that somewhat circular ? To show the existence of the left adjoint you need to do something. Imagine that you start with Peano arithmetic and want to build these constructs. You will either have to do case by case again or you will have to do quotienting and prove that the latter induces all the structures including the linear order which is indispensable part of the understanding of $\mathbb{Z}$.

• CommentRowNumber13.
• CommentAuthorTodd_Trimble
• CommentTimeNov 23rd 2016

Zoran, I’ve added a few words to integer which builds a bridge between the more historical conception and this nPOV. Please see if that seems more satisfactory to you. More words can be added of course.

• CommentRowNumber14.
• CommentAuthorDavidRoberts
• CommentTimeNov 23rd 2016

Double entry bookkeeping is, to my eyes, the Grothendieck group construction. See eg this article on Jstor (paywall) for a discussion of why double entry bookkeeping was introduced due to disbelief in negative numbers.

• CommentRowNumber15.
• CommentAuthorMike Shulman
• CommentTimeNov 23rd 2016

I think it’s fine. The right Coq file is https://github.com/HoTT/HoTT/blob/master/theories/Spaces/Int.v.

• CommentRowNumber16.
• CommentAuthorzskoda
• CommentTimeNov 24th 2016

The ordered procedure which I was mentioning is called symmetrization and works much beyond the special case of integers, but I am not sure if it is also some sort of an adjoint or not. Maybe it is also something in a $n$POV direction.

• CommentRowNumber17.
• CommentAuthorTodd_Trimble
• CommentTimeDec 29th 2016

Some fine-tuning and additional glosses on the Idea section, mentioning double-entry bookkeeping (partita doppia) and linking to a blogpost of Bob Walters.

• CommentRowNumber18.
• CommentAuthorKeithEPeterson
• CommentTimeDec 29th 2016

Changed,

$\mathbb{N} \stackrel{1 + -}{\to} \mathbb{N} \stackrel{1 + -}{\to} \mathbb{N} \stackrel{1 + -}{\to} \ldots$

to,

$\mathbb{N} \stackrel{1 + (-)}{\to} \mathbb{N} \stackrel{1 + (-)}{\to} \mathbb{N} \stackrel{1 + (-)}{\to} \ldots$

to avoid ambiguity in this Abelian group.