Kummer's Criterion and Regular Primes in Lean

10.1. The aim🔗

Let p be an odd prime and let K=\mathbb{Q}(\zeta_p). Put A=\mathrm{Cl}(\mathcal{O}_K)/p\,\mathrm{Cl}(\mathcal{O}_K), with the natural action of \Delta=\operatorname{Gal}(K/\mathbb{Q})\simeq(\mathbb{Z}/p\mathbb{Z})^\times. The reflection route tries to prove p\mid h^+(K)\Longrightarrow p\mid h^-(K) by proving a statement about the character components of A. If A_i denotes the i-th eigenspace, the desired reflection statement is that a nonzero even component forces a nonzero reflected component: A_i\ne0 \Longrightarrow A_{1-i}\ne0. The index 1-i is always understood modulo p-1, in the standard representative range.