Choice-free prime factorisation for a monogenic number ring

Put $A:={\mathcal{O}}_K=\mathbb{Z}[\alpha ]$. By [F1], $A\mathrm{/}pA\cong {\mathbb{F}}_p[t]\mathrm{/}(\bar{F})\mathrm{.}$

Since $pA\mathrm{\ne }0$, apply [F3] to write $pA={\prod }_{j=1}^r{Q}_j^{e_j}$ with distinct nonzero primes $Q_j$ and positive exponents $e_j$.

Under this isomorphism, [F2] decomposes $A\mathrm{/}pA$ as the product of the local rings $B_i:={\mathbb{F}}_p[t]\mathrm{/}(g_i^{a_i})$. The unique prime of $B_i$ is generated by $g_i$ and has residue field ${\mathbb{F}}_p[t]\mathrm{/}(g_i)$; therefore the primes of $A$ containing $pA$ are exactly the distinct inverse images $P_i=(p,{\tilde{g}}_i(\alpha ))$.

It follows that $A\mathrm{/}{P}_i\cong {\mathbb{F}}_p[t]\mathrm{/}(g_i)$, a field of degree $d_i$ over ${\mathbb{F}}_p$. Thus each $P_i$ is a nonzero prime above $(p)$ with residue degree $d_i$ by [F5].

The finite ring $A\mathrm{/}pA$ is the product in [F2], so every prime containing $pA$ is maximal. Each $Q_j$ contains $pA$ and hence equals one of the $P_i$ by step 2.1. Conversely, each $P_i$ contains $pA={\prod }_j{Q}_j^{e_j}$; its primality implies $Q_j\subseteq P_i$ for some $j$, and maximality makes $Q_j=P_i$. Hence the list $Q_1,\dots ,Q_r$ is exactly the list $P_1,\dots ,P_k$, with one exponent $e_i$ attached to each $P_i$.

Fix $i$ and put $S:=A_{P_i}$ and $\mathfrak{m}:=P_{i}S$. Each other $P_j$ contains an element outside $P_i$, which becomes a unit, so $pS={\mathfrak{m}}^{e_i}\mathrm{.}$ By [F4], $S$ is local with maximal ideal $\mathfrak{m}$; it is a domain because it is a localisation of the domain $A$. Also $\mathfrak{m}=(p,{\tilde{g}}_i(\alpha ))S$, so each power of $\mathfrak{m}$ is finitely generated by the monomials in these two generators.

The ideal $J:={\mathfrak{m}}^{e_i-1}$ is nonzero: it contains $p^{e_i-1}\mathrm{\ne }0$. If $J\subseteq {\mathfrak{m}}^{e_i}$, then $J=\mathfrak{m}J$. Among finite generating lists of $J$, take one of minimum length $n\ge 1$, say $v_1,\dots ,v_n$. The equality $J=\mathfrak{m}J$ gives $v_n={\sum }_{j=1}^n{c}_j{v}_j$ with $c_j\in \mathfrak{m}$. Since $1-c_n$ is a unit in the local ring $S$, this expresses $v_n$ in terms of the first $n-1$ generators, contradicting minimality. Hence ${\mathfrak{m}}^{e_i-1}\subseteq ̸{\mathfrak{m}}^{e_i}$. In $S\mathrm{/}pS=S\mathrm{/}{\mathfrak{m}}^{e_i}$ the maximal ideal therefore has nilpotency index exactly $e_i$, including $e_i=1$.

By [F1] and [F4], $A_{P_i}\mathrm{/}p{A}_{P_i}\cong {\mathbb{F}}_p[t{]}_{(g_i)}\mathrm{/}(\bar{F})\mathrm{.}$ Writing $\bar{F}=g_i^{a_i}{u}_i$ with $u_i={\prod }_{j\mathrm{\ne }i}{g}_j^{a_j}$, each factor of $u_i$ is a unit in ${\mathbb{F}}_p[t{]}_{(g_i)}$. Thus the displayed local ring is ${\mathbb{F}}_p[t{]}_{(g_i)}\mathrm{/}(g_i^{a_i})$. Its maximal ideal is generated by $g_i$ and has nilpotency index exactly $a_i$: its $a_i$-th power vanishes, while $g_i^{a_i-1}\mathrm{\notin }(g_i^{a_i})$, since cancellation in the polynomial localisation domain would otherwise make the nonunit $g_i$ a unit. Comparing its nilpotency index with step 5.1 gives $e_i=a_i$.

Substituting $e_i=a_i$ into the factorisation of step 1.2 yields $p{\mathcal{O}}_K={\prod }_{i=1}^k{P}_i^{a_i},P_i=(p,{\tilde{g}}_i(\alpha ))\mathrm{.}$ The residue degrees are those proved in step 3.1, and ${\sum }_i{a}_i{d}_i=\mathrm{deg}\bar{F}$. The polynomial factorisation and its CRT decomposition are finite; the only ideal-factorisation input [F3] explicitly uses finite least-coded choices and no Choice.