symmetric monoidal (∞,1)-category of spectra
In keeping with a historical point of view in which integers are whole numbers with a sign attached, one may write
whereby is represented by the element in the copy of appearing in this diagram. The group structure on may be extracted from this filtered colimit description.
The underlying sets and are isomorphic. Some subcultures of mathematics (and not only set theorists) use the term ‘integer’ synonymously for a natural number. Computer scientists distinguish between ‘unsigned integers’ (natural numbers) and ‘signed integers’ (integers as described here). Translations can also cause confusion with the term ‘whole number’.
In number theory, one generalises integers to algebraic integers, an instance of the red herring principle. Accordingly, some number theorists will call the integers ‘rational integers’ to clarify; is the ring of integers in the number field of rational numbers. (Compare, for example, Gaussian integers and Gaussian numbers.)
A formalization in terms of homotopy type theory, using a unary notation, is in
(A different common formalization of integers in type theory is in a binary notation, as in the Coq standard library. Binary notation is exponentially more efficient for performing computations, but the unary notation was convenient for calculating .)