nLab integer

Contents

Context

Algebra

Arithmetic

Contents

Idea

An integer is a number that is a natural number or the negative of one.

The ring \mathbb{Z} of all integers may defined as the free group on one generator or as the initial ring.

In keeping with a historical point of view in which integers are natural numbers with a sign attached, one may write

={n,n|n,0=0}={,3,2,1,0,1,2,3,}. \mathbb{Z} = \{n, -n | n \in \mathbb{N}, 0 = -0\} = \{ \ldots, -3, -2, -1, 0, 1, 2, 3, \ldots \} \,.

From an nPOV, one may consider this as follows: \mathbb{Z} is a filtered colimit of sets

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

whereby n-n \in \mathbb{Z} is represented by the element 00 in the n thn^{th} copy of \mathbb{N} appearing in this diagram (starting the count at the 0 th0^{th} copy). The resulting induced map to the colimit

× m:(m,n)nm\mathbb{N} \times \mathbb{N} \cong \sum_{m \in \mathbb{N}} \mathbb{N} \to \mathbb{Z}: (m, n) \mapsto n-m

imparts a monoid (in fact a group) structure on \mathbb{Z} descended from the monoid structure on ×\mathbb{N} \times \mathbb{N}; compare double-entry bookkeeping in medieval mathematics (partita doppia).

As a group, \mathbb{Z} is abelian and is the Grothendieck group of the monoid (or semigroup) \mathbb{N} of natural numbers.

The monoid of natural numbers is naturally even a rig – in fact the initial rig – and this multiplicative structure extends to \mathbb{Z} to make it a ring – in fact the initial ring.

In homotopy type theory

Given a dependent type theory with dependent product types, dependent sum types, identity types, empty type, unit type, and suspension types, the type of integers is defined as the loop space of the suspension of the suspension of the empty type:

Ω(Σ(Σ()))\mathbb{Z} \coloneqq \Omega(\Sigma(\Sigma(\emptyset)))

As higher inductive types

There are many definitions of the integers as a higher inductive type. Here we give 5 such definitions:

Definition

The integers are defined as the higher inductive type generated by:

  • A function inj:2×inj : \mathbf{2} \times \mathbb{N} \rightarrow \mathbb{Z}.
  • An identity representing that positive and negative zero are equal: ν 0:inj(0,0)=inj(1,0)\nu_0: inj(0, 0) = inj(1, 0).
Definition

The integers are defined as the higher inductive type generated by:

  • A term 0:0 : \mathbb{Z}.
  • A function s:s : \mathbb{Z} \to \mathbb{Z}.
  • A function p 1:p_1 : \mathbb{Z} \to \mathbb{Z}.
  • A function p 2:p_2 : \mathbb{Z} \to \mathbb{Z}.
  • A dependent product of identities representing that p 1p_1 is a section of ss:
    σ: a:p 1(s(a))=a\sigma: \prod_{a:\mathbb{Z}} p_1(s(a)) = a
  • A dependent product of identities representing that p 2p_2 is a retracion of ss:
    ρ: a:s(p 2(a))=a\rho: \prod_{a:\mathbb{Z}} s(p_2(a)) = a
Definition

The integers are defined as the higher inductive type generated by:

  • A term 0:0 : \mathbb{Z}.
  • A function s:s : \mathbb{Z} \to \mathbb{Z}.
  • A function p:p : \mathbb{Z} \to \mathbb{Z}.
  • A dependent product of identities representing that pp is a section of ss:
    σ: a:p(s(a))=a\sigma: \prod_{a:\mathbb{Z}} p(s(a)) = a
  • A dependent product of identities representing that pp is a retracion of ss:
    ρ: a:s(p(a))=a\rho: \prod_{a:\mathbb{Z}} s(p(a)) = a
  • A dependent product of identities representing the coherence condition:
    κ: a:ap s(σ(a))=ρ(a)\kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)
Definition

The integers are defined as the higher inductive type generated by:

  • A term 0:0 : \mathbb{Z}.
  • A function s:s : \mathbb{Z} \to \mathbb{Z}.
  • A function n:n : \mathbb{Z} \to \mathbb{Z}.
  • An identity representing that zero and negative zero are equal: ν:n(0)=0\nu: n(0) = 0.
  • A dependent product of identities representing that negation is an involution:
    ι: a:n(n(a))=a\iota: \prod_{a:\mathbb{Z}} n(n(a)) = a
  • A dependent product of identities representing the coherence condition for the above:
    κ ι: a:ap n(ι(a))=ι(a)\kappa_\iota: \prod_{a:\mathbb{Z}} ap_n(\iota(a)) = \iota(a)
  • A dependent product of identities representing that nsnn \circ s \circ n is a section of ss:
    σ: a:n(s(n(s(a))))=a\sigma: \prod_{a:\mathbb{Z}} n(s(n(s(a)))) = a
  • A dependent product of identities representing that nsnn \circ s \circ n is a retracion of ss:
    ρ: a:s(n(s(n(a))))=a\rho: \prod_{a:\mathbb{Z}} s(n(s(n(a)))) = a
  • A dependent product of identities representing the coherence condition:
    κ: a:ap s(σ(a))=ρ(a)\kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)
Definition

The integers are defined as the higher inductive type generated by:

  • A function inj:×inj : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{Z}.
  • A dependent product of functions between identities representing that equivalent differences are equal:
    equivdiff: a: b: c: d:(a+d=c+b)(inj(a,b)=inj(c,d))equivdiff : \prod_{a:\mathbb{N}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{N}} \prod_{d:\mathbb{N}} (a + d = c + b) \to (inj(a,b) = inj(c,d))
  • A set-truncator
    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} isProp(a=b)

Properties

We assume in this section that the integers are defined according to definition 2.1 above in the context of homotopy type theory.

Commutative ring structure on the integers

Definition

The integer zero 0:0:\mathbb{Z} is defined as

0inj(0,0)0 \coloneqq inj(0, 0)
Definition

Let ()+():×(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N} be addition of the natural numbers, let ρ:×\rho:\mathbb{N} \times \mathbb{N} \to \mathbb{N} be the symmetric difference or metric of the natural numbers, and let <:×𝟚\lt:\mathbb{N} \times \mathbb{N} \to \mathbb{2} be the decidable strict order on the natural numbers into the booleans. The binary operation addition ()+():×(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is inductively defined as

inj(0,a)+inj(0,b)inj(0,a+b)inj(0,a) + inj(0,b) \coloneqq inj(0,a+b)
inj(1,a)+inj(1,b)inj(1,a+b)inj(1,a) + inj(1,b) \coloneqq inj(1,a+b)
inj(0,a)+inj(1,b)inj(a<b,ρ(a,b))inj(0,a) + inj(1,b) \coloneqq inj(a \lt b,\rho(a,b))
inj(1,a)+inj(0,b)inj(b<a,ρ(a,b))inj(1,a) + inj(0,b) \coloneqq inj(b \lt a,\rho(a,b))

for a:a:\mathbb{N}, b:b:\mathbb{N}.

Definition

The unary operation negation ():-(-):\mathbb{Z} \to \mathbb{Z} is defined as

inj(a,b)inj(¬a,b)-inj(a, b) \coloneqq inj(\neg a, b)

for a:2a:\mathbf{2}, b:b:\mathbb{N}, ¬:22\neg:\mathbf{2} \to \mathbf{2}

Definition

The binary operation subtraction ()():×(-)-(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

inj(a,b)inj(c,d)inj(a,b)+inj(¬c,d)inj(a, b) - inj(c, d) \coloneqq inj(a, b) + inj(\neg c, d)

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The integer number one 1:1:\mathbb{Z} is defined as

1inj(0,1)1 \coloneqq inj(0,1)
Definition

The binary operation multiplication ()():×(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

inj(a,b)inj(c,d)inj(ac,bd)inj(a,b) \cdot inj(c,d) \coloneqq inj(a \oplus c,b \cdot d)

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}, ()():×(-)\cdot(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}, ()():2×22(-)\oplus(-):\mathbf{2} \times \mathbf{2} \to \mathbf{2} (exclusive or binary operation in 2\mathbf{2}).

Definition

The right \mathbb{N}-action exponentiation () ():×(-)^{(-)}:\mathbb{Z} \times \mathbb{N} \to \mathbb{Z} is inductively defined as

inj(a,b) 0inj(0,1)inj(a,b)^0 \coloneqq inj(0,1)
inj(a,b) 2ninj(0,b 2n)inj(a,b)^{2n} \coloneqq inj(0,b^{2n})
inj(a,b) 2n+1inj(a,b 2n+1)inj(a,b)^{2n+1} \coloneqq inj(a,b^{2n+1})

for a:2a:\mathbf{2}, b:b:\mathbb{N}, n:n:\mathbb{N}, () ():×(-)^{(-)}:\mathbb{N} \times \mathbb{N} \to \mathbb{N}.

Order structure on the integers

Definition

The predicate is positive, denoted as isPositive(inj(a,b))isPositive(inj(a,b)), is defined as

isPositive(inj(a,b))(a=0)×(b>0)isPositive(inj(a,b)) \coloneqq (a = 0) \times (b \gt 0)

for a:2a:\mathbf{2}, b:b:\mathbb{N}, and the strict order relation <\lt on the natural numbers.

Definition

The predicate is negative, denoted as isNegative(inj(a,b))isNegative(inj(a,b)), is defined as

isPositive(inj(a,b))(a=1)×(b>0)isPositive(inj(a,b)) \coloneqq (a = 1) \times (b \gt 0)

for a:2a:\mathbf{2}, b:b:\mathbb{N}, and the strict order relation <\lt on the natural numbers.

Definition

The predicate is zero, denoted as isZero(inj(a,b))isZero(inj(a,b)), is defined as

isZero(inj(a,b))b=0isZero(inj(a,b)) \coloneqq b = 0

for a:2a:\mathbf{2}, b:b:\mathbb{N}.

Definition

The predicate is non-positive, denoted as isNonPositive(inj(a,b))isNonPositive(inj(a,b)) is defined as

isNonPositive(inj(a,b))isPositive(inj(a,b))isNonPositive(inj(a,b)) \coloneqq isPositive(inj(a,b)) \to \emptyset

for a:2a:\mathbf{2}, b:b:\mathbb{N}.

Definition

The predicate is non-negative, denoted as isNonNegative(inj(a,b))isNonNegative(inj(a,b)), is defined as

isNonNegative(inj(a,b))isNegative(inj(a,b))isNonNegative(inj(a,b)) \coloneqq isNegative(inj(a,b)) \to \emptyset

for a:2a:\mathbf{2}, b:b:\mathbb{N}.

Definition

The predicate is non-zero, denoted as isNonZero(inj(a,b))isNonZero(inj(a,b)), is defined as

isNonZero(inj(a,b))isPositive(inj(a,b))+isNegative(inj(a,b))isNonZero(inj(a,b)) \coloneqq \Vert isPositive(inj(a,b)) + isNegative(inj(a,b)) \Vert

for a:2a:\mathbf{2}, b:b:\mathbb{N}.

Definition

The predicate is less than, denoted as inj(a,b)<inj(c,d)inj(a,b) \lt inj(c,d), is defined as

inj(a,b)<inj(c,d)isPositive(inj(c,d)inj(a,b))inj(a,b) \lt inj(c,d) \coloneqq isPositive(inj(c,d) - inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The predicate is greater than, denoted as inj(a,b)>inj(c,d)inj(a,b) \gt inj(c,d), is defined as

inj(a,b)>inj(c,d)isNegative(inj(c,d)inj(a,b))inj(a,b) \gt inj(c,d) \coloneqq isNegative(inj(c,d) - inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The predicate is apart from, denoted as inj(a,b)#inj(c,d)inj(a,b) # inj(c,d), is defined as

inj(a,b)#inj(c,d)isNonZero(inj(c,d)inj(a,b))inj(a,b) # inj(c,d) \coloneqq isNonZero(inj(c,d) - inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The predicate is less than or equal to, denoted as inj(a,b)inj(c,d)inj(a,b) \leq inj(c,d), is defined as

inj(a,b)inj(c,d)isNonNegaitve(inj(c,d)inj(a,b))inj(a,b) \leq inj(c,d) \coloneqq isNonNegaitve(inj(c,d) - inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The predicate is greater than or equal to, denoted as inj(a,b)inj(c,d)inj(a,b) \geq inj(c,d), is defined as

inj(a,b)inj(c,d)isNonPositive(inj(c,d)inj(a,b))inj(a,b) \geq inj(c,d) \coloneqq isNonPositive(inj(c,d) - inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Pseudolattice structure on the integers

Definition

The ramp function ramp:ramp:\mathbb{Z} \to \mathbb{Z} is inductively defined as

ramp(inj(0,a))inj(0,a)ramp(inj(0, a)) \coloneqq inj(0, a)
ramp(inj(1,a))0ramp(inj(1, a)) \coloneqq 0

for a:a:\mathbb{N}.

Definition

The minimum min:×min:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

min(inj(a,b),inj(c,d))inj(a,b)ramp(inj(a,b)inj(c,d))min(inj(a,b),inj(c,d)) \coloneqq inj(a,b) - ramp(inj(a,b) - inj(c,d))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The maximum max:×max:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

max(inj(a,b),inj(c,d))inj(a,b)+ramp(inj(c,d)inj(a,b))max(inj(a,b),inj(c,d)) \coloneqq inj(a,b) + ramp(inj(c,d) - inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}, c:2c:\mathbf{2}, d:d:\mathbb{N}.

Definition

The absolute value |()|:\vert(-)\vert:\mathbb{Z} \to \mathbb{Z} is defined as

|inj(a,b)|max(inj(a,b),inj(a,b))\vert inj(a,b) \vert \coloneqq max(inj(a,b), -inj(a,b))

for a:2a:\mathbf{2}, b:b:\mathbb{N}.

Division and remainder

Definition

Integer division ()÷():× 0(-)\div(-):\mathbb{Z} \times \mathbb{Z}_{\neq 0} \to \mathbb{Z} is defined as

inj(0,a)÷inj(0,b)inj(0,a÷b)inj(0,a) \div inj(0,b) \coloneqq inj(0,a \div b)
inj(0,a)÷inj(1,b)inj(1,a÷b)inj(0,a) \div inj(1,b) \coloneqq inj(1,a \div b)
inj(1,a)÷inj(0,b)inj(1,a÷b)inj(1,a) \div inj(0,b) \coloneqq inj(1,a \div b)
inj(1,a)÷inj(1,b)inj(0,a÷b)inj(1,a) \div inj(1,b) \coloneqq inj(0,a \div b)

for a:a:\mathbb{N}, b: 0b:\mathbb{N}_{\neq 0}.

Terminology

The underlying sets \mathbb{Z} and \mathbb{N} 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; \mathbb{Z} is the ring of integers in the number field \mathbb{Q} of rational numbers. (Compare, for example, Gaussian integers and Gaussian numbers.)

The symbol ‘\mathbb{Z}’ derives from the German word ‘Zahlen’, which is a generic word for ‘numbers’. (Compare Dedekind's use of that word in the title of his famous book on the foundations of real numbers.)

References

For definitions as a higher inductive type in homotopy type theory, see:

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 π 1(S 1)\pi_1(S^1).)

Last revised on June 17, 2022 at 14:18:55. See the history of this page for a list of all contributions to it.