What route to take to Chebotarev?

Stream: PrimeNumberTheorem+

[Terence Tao]

I am not myself an expert in algebraic number theory, but my colleague Romyar Sharifi kindly pointed me towards his lecture notes where he proves (the Dirichlet density version of) the Chebotarev density theorem in Section 7. Roughly speaking, the idea is to first prove Chebotarev for cyclotomic extensions, then for abelian extensions (which in particular covers the case of cyclic extensions), and then arbitrary extensions. The latter two steps are mostly algebraic number theory in nature; it is just the first step in which analytic methods are used. It seems the cyclotomic case is very similar in spirit to the prime number theorem in arithmetic progressions (and indeed generalizes that theorem). I made a preliminary attempt to state some of the key steps in the blueprint at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/222 , focusing on the cyclotomic case. But I am not very confident that this is the optimal route, I'm hoping there is someone who is more familiar with the algebraic number theory side of things who can chime in.

[Terence Tao]

I'm reviving this old thread now that we have the issues system in place. I have in the blueprint a very sketchy route to the Chebotarev density theorem, based on (a) first establishing this theorem for cyclotomic extensions; (b) using this to establish the theorem for abelian extensions, and then (c) doing arbitrary extensions. All three steps are very sketchy right now, pointing to some notes of Sharifi. This is in large part because I do not have the algebraic number theory background to properly flesh out a blueprint for any of these steps. So I have opened PNT#584 as a blueprinting task (not a formalization task) to provide a more detailed blueprint for (a), for instance breaking up the three lemmas 2.5.1, 2.5.2, 2.5.3 currently in the blueprint into smaller pieces, that one can then hopefully try to formalize with further issues. This would be a task for someone expert in algebraic number theory but would not require significant expertise with Lean.