Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
noticed that the entry was missing, so I created a stub for integer
I expanded this a bit, been meaning to write it.
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.
Well, I certainly think that being the initial ring is the most important feature, but it’s not a big deal.
Todd noticed a link and created algebraic integer.
Added to integer a pointer to Mike’s HoTT formalization of the integers.
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?
Why is that?
Ah, I get it.
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.
the link
at integer seem not to work.
The statement in the idea section that the ring of integers is obtained as the Grothendieck group of the commutative monoid 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).
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 to the monoidal unit for abelian groups , 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 as just .
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 .
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.
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.
I think it’s fine. The right Coq file is https://github.com/HoTT/HoTT/blob/master/theories/Spaces/Int.v.
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 POV direction.
Some fine-tuning and additional glosses on the Idea section, mentioning double-entry bookkeeping (partita doppia) and linking to a blogpost of Bob Walters.
Changed,
to,
to avoid ambiguity in this Abelian group.
moved material about the type of integers in dependent type theory from integers to its own page at integers type
Anonymous
added pointer to:
1 to 22 of 22