Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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.1. the link

    at integer seem not to work.

    2.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 RR as just R\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 nnPOV 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,

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

    to,

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

    to avoid ambiguity in this Abelian group.

  1. added another definition of the integers as a higher inductive type

    Anonymous

    diff, v31, current

  2. moved material about the type of integers in dependent type theory from integers to its own page at integers type

    Anonymous

    diff, v33, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeFeb 8th 2023

    added pointer to

    diff, v36, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeFeb 8th 2023