The canonical natural $\iota(n) = n \cdot 1_F$ of a field

Let $F$ be a field (Field) with additive identity $0_F$ and multiplicative identity $1_F$. Define $\iota : \mathbb{N} \to F$ by recursion on $\mathbb{N}$ (The natural numbers $\mathbb{N}$ (von Neumann), The recursion theorem):

$\iota(0) \;:=\; 0_F, \qquad \iota(n+1) \;:=\; \iota(n) + 1_F .$

$\iota(n)$ is the canonical natural of $n$ in $F$. It is also written $n \cdot 1_F$, and for $n \ge 1$ it is $1_F$ added to itself $n$ times.

Why the notation is needed at all. A natural number in this library is a von Neumann natural, that is a set (The natural numbers $\mathbb{N}$ (von Neumann)), and a set is not an element of $F$. So $1/n$, $n^{\alpha}$ and $x/n$ are not expressions of $F$ when $n$ is a natural: what they mean is $1/\iota(n)$, $\iota(n)^{\alpha}$ and $x/\iota(n)$. The map $\iota$ is what carries a counting number into the field, and writing it is the whole reason a reader meets $1/\iota(k+1)$ where an informal text would write $1/(k+1)$.

• Where the index shift comes from. $\mathbb{N}$ contains $0$ (The natural numbers $\mathbb{N}$ (von Neumann)) and $\iota(0) = 0_F$, so $1/\iota(k)$ is undefined at $k = 0$. A family of reciprocals indexed by $\mathbb{N}$ is therefore written over $\iota(k+1)$, which is why the harmonic and telescoping families of this library run over $k+1$ rather than over $k$. This is bookkeeping, not a restriction: the values are the usual ones.

• This definition records notation; the arithmetic is proved elsewhere. That $\iota$ is strictly increasing and positive on $n \ge 1$, and that it carries sums to sums and products to products, is Canonical naturals are positive and strictly increasing, stated for an ordered field. That lemma introduces the same element by the equivalent recursion $1 \cdot 1_F = 1_F$, $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$, which agrees with the definition above because $\iota(1) = \iota(0) + 1_F = 1_F$. Nothing here is new mathematics; the definition exists so that the notation has a home a reader can look up.

• The symbol $\iota$ is used in this library for other canonical maps, and this definition does not govern them. It also denotes the canonical field embedding $\iota : \mathbb{Q} \to F$ (The unique embedding of ℚ into an ordered field), the isometric embedding of a metric space into a completion (A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace ↗), and an inclusion map $\iota : S \to X$ of a subspace. Each of those is introduced where it is used and means something different from the map defined here. What the four share is only that each is the canonical map of its situation.

• Fields, not just ordered fields. The recursion needs no order, so the definition is stated for a field; every use in this library is in an ordered field, and the order is what makes $\iota$ injective (Canonical naturals are positive and strictly increasing). In a field of positive characteristic $\iota$ is not injective, which is one reason the injectivity is a lemma rather than part of the definition.