The Krull dimension of the semiring of natural numbers is equal to 2

Summary

Let $R$ be a ring. Its Krull dimension is the supremum of the lengths $n$ of chains $P_0\subsetneq P_1 \subsetneq\dots\subsetneq P_n$ of prime ideals of $R$. When $R$ is a field, the null ideal is the only prime ideal, and it is a maximal ideal so that its Krull dimension is zero. When $R$ is a principal ideal domain which is not a field, there are two kinds of prime ideals: the null ideal is prime (as in any domain), and the other prime ideals are the maximal ideals of $R$, generated by a prime element $p$. In particular, the Krull dimension of the ring of integers is equal to $1$. It is classic that these concepts can be defined for semirings as well. A semiring $R$ is a set endowed with a commutative and associative addition with a neutral element $0$, an associative multiplication with a neutral element $1$, such that addition distributes over multiplication: $(a+b)c=ac+bc$ and $c(a+b)=ca+cb$. When its multiplication is commutative, the semiring is said to be commutative. Semirings $R$ have ideals: these are nonempty subsets $I$ which are stable under addition ($a+b\in I$ for $a,b\in I$), and stable under multiplication by any element of $R$: for general semirings, one has to distinguish between left, right, and two-sided ideals; for commutative semirings, the notions coincide. An ideal $P$ of a semiring $R$ is said to be prime if $R\setminus P$ is a multiplicative subset; explicitely, $P\neq R$, and if $ab\in P$, then $a\in P$ or $b\in P$. An ideal $P$ of a semiring $R$ is said to be maximal if $P\neq R$ and if there is no ideal $I$ such that $P\subsetneq I\subsetneq R$. A semiring $R$ is said to be local if it admits exactly one maximal ideal; this means that the set of non-invertible elements of $R$ is an ideal. The amusing part comes from the classification of prime and maximal ideals of the semiring $\mathbf N$ of natural numbers, which I learned of via a Lean formalization project led by Junyan Xu. Theorem. The semiring $\mathbf N$ is local; its maximal id...