An introduction to p-adic L-functions — Lean blueprint

1.2. Part II — Iwasawa theory and the Main Conjecture🔗

Part II reinterprets \zeta_p as an element of the Iwasawa algebra and matches it against arithmetic.

  • The Coleman map (§9–§10). Coleman's theorem on norm-coherent systems of units in the cyclotomic tower Coleman (1979) produces a map from local units to the Iwasawa algebra; applied to cyclotomic units it manufactures the p-adic L-function on the algebraic side.

  • Iwasawa's theorem on the zeros of \zeta_p (§11–§12). Measures on the Galois group \Gal(\Q(\mu_{p^\infty})/\Q), the equivariance of the Coleman map, the fundamental exact sequence, and explicit generators for global and local cyclotomic units combine to identify the ideal generated by \zeta_p.

  • The Iwasawa Main Conjecture (§13). With the structure theory of finitely generated \Lam-modules in hand, the Main Conjecture equates the characteristic ideal of a certain Galois module with the ideal generated by \zeta_p. We follow the notes' proof for Vandiver primes.

  • Iwasawa's \mu-invariant (§14) and Iwasawa theory for modular forms (§15). The \mu = 0 theorem and its consequences, then the \mathrm{GL}(2) analogue that recasts the whole story for modular forms.

The chapters that follow this overview are populated by /develop and /blueprint as the formalisation proceeds.