I was inspired to think about how algebraic number theory could be developed in first-order arithmetic, since most developments of ANT do make use of complex numbers. Most of the time such uses of continuous structures can be circumvented by employing tricks like rational approximations, but it's not entirely clear how all that could be done in first-order arithmetic. At least for "elementary" ANT, this most prominently comes up in the proof of Dirichlet's Unit Theorem, which even in the statement counts real and complex embeddings, and the standard proof further uses Minkowski's Theorem on convex bodies.
While I have little doubt that the answer to this question is positive, let me state it anyway:
Can Dirichlet's Unit Theorem be stated and proven in Peano arithmetic?
The application of Minkowski's Theorem can probably be replaced with a clever pigeonhole principle argument (like in the usual proof of finiteness of the class number), I am more interested in how one would deal with the question of real vs complex embeddings.
If there is one, I would be interested in some reference which systematically develops (or at least describes how one could do that) algebraic number theory in first-order arithmetic.
One can of course extend this last request to other areas, two coming to my mind being analytic number theory and class field theory. If anyone has any references for those I am interested, but principal focus is still on algebraic number theory.
The standard approach to doing this sort of thing would be to use a richer conservative extension: e.g. prove the result more-or-less as usual in ACA$_0$ and then apply the fact that ACA$_0$ is conservative over PA.
The language of ACA$_0$ is rich enough to talk about $\mathbb{R}$, $\mathbb{C}$, and related objects by coding their elements as sets of naturals, and the theory itself is strong enough to ensure that $(i)$ these structures behave as desired (e.g. the compactness of $[0,1]$ follows from the weaker theory WKL$_0$) and $(ii)$ iron out "coding issues" (e.g. ones arising from non-unique base-$2$ representations). ACA$_0$ is also enough to prove many standard results of group, ring, and field theory (e.g. the existence of maximal and prime ideals).
At a glance I don't see anything in the usual proof of Dirichlet's Unit Theorem (or others) that would use more than ACA$_0$, but I'm not familiar enough with it to be certain. In general, "non-logic-y" theorems of second-order arithmetic which can't be proved in ACA$_0$ seem pretty rare (reflecting the fact that independence from PA outside logic is pretty rare).