FC09 — Jürgen Neukirch, Algebraic Number Theory (1999)

FC09 — Neukirch, Algebraic Number Theory.

This chapter contains 17 definitions, 11 theorems, 14 propositions, 2 lemmas, 6 corollaries, 2 examples and 4 conventions.

Of the 56 statements checked against Lean, 5 are formalized somewhere and 51 are not.

Status	Statements	Share	What it means
not formalized	51	91%	A documented search found no Lean statement of it anywhere.
in another Lean project	3	5%	Some other Lean development has it; using it means porting that code.
in lean-categories	1	2%	This repository states and proves it.
in Mathlib	1	2%	Mathlib states and proves it.
checked in total	56

Which versions of Lean and Mathlib were searched

Canonical source block: FC09 Neukirch Chapter V, FC09-C05-U001–FC09-C05-U056, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 56 rows through agent-memory, asserts exact order/uniqueness, and assigns exactly one route to every unit.
Project-first inspection used A=3b2239e161592472b34e02ad3b7da308f9ce7280 (Lean 4.33.0, Apache-2.0). The material C05 project layer is the quadratic Hilbert-symbol development in LeanCategories/Lattices/Valued: the norm criterion, odd-prime unit/mixed formulas, and the closed dyadic formula. These close U028 exactly, but strict bundle semantics prevents a quadratic specialization from earning the general n-th Hilbert-symbol rows U020–U027 or the wild explicit-reciprocity rows U029–U032. No project local-reciprocity or Lubin–Tate layer was found.
Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Its source-complete C05 contribution is the one-dimensional formal-group-law core: FormalGroup plus FormalGroup.IsComm closes U033. It has no local norm-residue/reciprocity, Hilbert-symbol, Lubin–Tate, or higher-ramification interface closing the remaining local-CFT bundles.
Current Mathlib was checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Targeted current-tree searches found no Lubin-Tate, local-reciprocity/norm-residue, hilbertSymbol, or Herbrand local-CFT layer, and Mathlib/RingTheory/Valuation/RamificationGroup.lean still explicitly states TODO: Define higher ramification groups in lower numbering. This blocks source-complete routes for U053–U056.
Open Mathlib PR #38213 was inspected at O=133714768d42ba1a6107b7a84e2d22222c7c69ed. Its new FormalGroupHom and FormalGroupIso APIs close U034 and, together with pinned substitution-inverse and base-change APIs, give direct short derivations for U036–U037. Because the PR is open/draft and absent from both P and H, these are reference-port, not mathlib. It does not provide the endomorphism-ring/formal-module/Lubin–Tate structures needed for U038–U052.
Open Mathlib PR #42687 was rechecked at O=a40561e249ebf45d2870f5d9d45bc2eb4d80b242. It defines abstract formation/field-formation/class-formation structures but no reciprocity/norm-residue theorem, while its proposed local class formation still contains sorry; it therefore does not close U001–U012 or U043–U052.
External local-CFT discovery was checked rather than inferred. kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509 contains intended local Herbrand and unramified-cohomology theorems, but the former depends on an explicit sorry for local units and the latter is itself sorried, so neither is credited. mariainesdff/LocalClassFieldTheory currently has no completed reciprocity/Lubin–Tate layer. A targeted Kronecker–Weber search found xroblot/SKW@3c8b2c9589b5a790f07ee7faf0b5ccfbe4005d10::kronecker_weber, whose statement exactly matches U013, but its current proof depends on TwoPower.lean with unresolved sorrys and the repository exposes no recognized license; U013 therefore remains unmatched.
Strict bundle semantics was enforced throughout. Ordinary cyclotomic Galois APIs do not earn the Kronecker–Weber or local-cyclotomic maximal-abelian statements; Hilbert 90 does not earn local reciprocity; basic formal-group laws/homomorphisms do not earn endomorphism rings, formal O-modules, or Lubin–Tate modules; and ideal-theoretic ramification does not earn upper-numbering reciprocity or Hasse–Arf without the missing higher-ramification layer.
Short derivations are credited only from checked interfaces. U028 is a notational translation of the project’s closed quadratic p-adic formulas. U036 uses the pinned two-sided substitution inverse of a zero-constant power series with unit linear coefficient and cancellation in the formal-group homomorphism identity to obtain the inverse homomorphism; the converse compares linear coefficients. U037 is formal-group base change followed by the PR’s homomorphism object.
All mathlib targets were path/token validated against P, U028 project targets against A, open-PR targets against O=133714768d42ba1a6107b7a84e2d22222c7c69ed with sorry excluded in the cited file, and negative/current/open/external checks against H/#42687/the inspected external revisions.
Route totals for C05: mathlib 1, project-existing 1, package-import 0, reference-port 3, unmatched 51.

Theorem (1.1)

FC09-C05-U001 · Chapter V, §1, source L13636 · not formalized

(1.1) Theorem. For a cyclic extension \(L|K\) of local fields, one has \[ \# H ^ {i} \big (G (L | K), L ^ {*} \big) = \left\{ \begin{array}{l l} [ L: K ] & \text {for i = 0 ,} \\ 1 & \text {for i = -1 .} \end{array} \right. \]

Not formalized. Pinned/current Mathlib has local fields, Galois cohomology, cyclotomic fields and Hilbert 90, but no proved local reciprocity/norm-residue, local existence, conductor, or Kronecker–Weber owner closes this source unit. The targeted ClassFieldTheory local theorems remain dependent on sorry.

Corollary (1.2)

FC09-C05-U002 · Chapter V, §1, source L13686 · not formalized

(1.2) Corollary. If \(L|K\) is an unramified extension of local fields, then for \(i = 0, -1\) , one has \[ H ^ {i} \big (G (L | K), U _ {L} \big) = 1 \quad a n d \quad H ^ {i} \big (G (L | K), U _ {L} ^ {(n)} \big) = 1 \quad f o r \quad n = 1, 2, \ldots \] In particular, \[ N _ {L | K} U _ {L} = U _ {K} \quad a n d \quad N _ {L | K} U _ {L} ^ {(n)} = U _ {K} ^ {(n)}. \]

Theorem (1.3)

FC09-C05-U003 · Chapter V, §1, source L13772 · not formalized

(1.3) Theorem. For every finite Galois extension \(L|K\) of local fields we have a canonical isomorphism \[ r _ {L | K}: G (L | K) ^ {a b} \stackrel {{\sim}} {{\longrightarrow}} K ^ {*} / N _ {L | K} L ^ {*}. \]

Definition / construction

FC09-C05-U004 · Chapter V, §1, source L13784 · not formalized

Inverting \(r_{L|K}\) gives us the local norm residue symbol \[ (, L | K): K ^ {*} \longrightarrow G (L | K) ^ {a b}. \] It is surjective and has kernel \(N_{L|K}L^{*}\) .

Definition / construction

FC09-C05-U005 · Chapter V, §1, source L13792 · not formalized

In global class field theory we will have to take into account the field \(R = Q_{\infty}\) along with the p-adic number fields \(Q_{p}\) . It also admits a reciprocity law: for the unique non-trivial Galois extension C|R, we define the norm residue symbol \[ (\quad , \mathbb {C} | \mathbb {R}): \mathbb {R} ^ {*} \longrightarrow G (\mathbb {C} | \mathbb {R}) \] by \[ (a, \mathbb {C} | \mathbb {R}) \sqrt {- 1} = \sqrt {- 1} ^ {\operatorname{sgn} (a)}. \] The kernel of \((\mathbb{C}|\mathbb{R})\) is the group \(\mathbb{R}_{+}^{*}\) of all positive real numbers, which is again the group of norms \(N_{\mathbb{C}|\mathbb{R}}\mathbb{C}^{*} = \{z\bar{z} \mid z \in \mathbb{C}^{*}\}\) .

Theorem (1.4)

FC09-C05-U006 · Chapter V, §1, source L13808 · not formalized

(1.4) Theorem. The rule \[ L \longmapsto \mathcal {N} _ {L} = N _ {L | K} L ^ {*} \] gives a 1-1-correspondence between the finite abelian extensions of a local field \(K\) and the open subgroups \(\mathcal{N}\) of finite index in \(K^{*}\) . Furthermore, \[ L _ {1} \subseteq L _ {2} \Longleftrightarrow \mathcal {N} _ {L _ {1}} \supseteq \mathcal {N} _ {L _ {2}}, \quad \mathcal {N} _ {L _ {1} L _ {2}} = \mathcal {N} _ {L _ {1}} \cap \mathcal {N} _ {L _ {2}}, \quad \mathcal {N} _ {L _ {1} \cap L _ {2}} = \mathcal {N} _ {L _ {1}} \mathcal {N} _ {L _ {2}}. \]

Proposition (1.5)

FC09-C05-U007 · Chapter V, §1, source L13846 · not formalized

(1.5) Proposition. If \(K\) contains the \(n\) -th roots of unity, and if the characteristic of \(K\) does not divide \(n\) , then the extension \(L = K(\sqrt[n]{K^*})|K\) is finite, and one has \[ N _ {L | K} L ^ {*} = K ^ {* n} \quad \text { and } \quad G (L | K) \cong K ^ {*} / K ^ {* n}. \]

Convention / notation

FC09-C05-U008 · Chapter V, §1, source L13852 · after FC09-C02-U065, FC09-C05-U006 · not formalized

Theorem (1.4) is called the existence theorem, because its essential statement is that, for every open subgroup N of finite index in \(K^{*}\) , there exists an abelian extension \(L|K\) such that \(N_{L|K}L^{*} = N\) . This is the “class field” of N. (Incidentally, when \(\text{char}(K) = 0\) , every subgroup of finite index is automatically open – see chap. II, (5.7).) Every open subgroup of \(K^{*}\) contains some higher unit group \(U_{K}^{(n)}\) , as these form a basis of neighbourhoods of 1 in \(K^{*}\) . We put \(U_{K}^{(0)} = U_{K}\) and define:

Definition (1.6)

FC09-C05-U009 · Chapter V, §1, source L13854 · not formalized

(1.6) Definition. Let \(L|K\) be a finite abelian extension, and \(n\) the smallest number \(\geq 0\) such that \(U_K^{(n)} \subseteq N_{L|K}L^*\) . Then the ideal \[ \mathfrak {f} = \mathfrak {p} _ {K} ^ {n} \] is called the conductor of \(L|K\) .

Proposition (1.7)

FC09-C05-U010 · Chapter V, §1, source L13862 · not formalized

(1.7) Proposition. A finite abelian extension \(L|K\) is unramified if and only if its conductor is \(f = 1\) .

Proposition (1.8)

FC09-C05-U011 · Chapter V, §1, source L13868 · not formalized

(1.8) Proposition. The group of norms of the extension \(\mathbb{Q}_p(\mu_{p^n})|\mathbb{Q}_p\) is the group \((p)\times U_{\mathbb{Q}_p}^{(n)}\) .

Corollary (1.9)

FC09-C05-U012 · Chapter V, §1, source L13892 · not formalized

(1.9) Corollary. Every finite abelian extension of \(L|\mathbb{Q}_p\) is contained in a field \(\mathbb{Q}_p(\zeta)\) , where \(\zeta\) is a root of unity. In other words: The maximal abelian extension \(Q_{p}^{ab}|Q_{p}\) is generated by adjoining all roots of unity.

Theorem (1.10)

FC09-C05-U013 · Chapter V, §1, source L13906 · not formalized

(1.10) Theorem. Every finite abelian extension \(L|\mathbb{Q}\) is contained in a field \(\mathbb{Q}(\zeta)\) generated by a root of unity \(\zeta\) .

Not formalized. A targeted external search found xroblot/SKW::kronecker_weber, but the current proof depends on TwoPower.lean, which still contains explicit sorrys; the repository also declares no recognized license. It is therefore not credited as a reference-port route.

Convention / notation

FC09-C05-U014 · Chapter V, §2, source L14024 · not formalized

We have to invoke a transcendental method which makes use of the completion \(\widehat{K}\) of the maximal unramified extension \(\widetilde{K}\) of a local field K. We extend the Frobenius \(\varphi \in G(\widetilde{K}|K)\) to \(\widehat{K}\) by continuity. First we prove the lemma (2.1): for every \(c \in \mathcal{O}_{\widehat{K}}\), resp. every \(c \in U_{\widehat{K}}\), the equation \(x^{\varphi} - x = c\), resp. \(x^{\varphi-1} = c\), admits a solution.

Not formalized. No checked project/pinned/current/open/external owner supplies Neukirch’s completed maximal-unramified Frobenius equations or Lubin–Tate series construction and its reciprocity action.

Lemma (2.1)

FC09-C05-U015 · Chapter V, §2, source L14026 · not formalized

(2.1) Lemma. For every \(c \in \mathcal{O}_{\widehat{K}}\) , resp. every \(c \in U_{\widehat{K}}\) , the equation \[ x ^ {\varphi} - x = c, \quad r e s p. \quad x ^ {\varphi - 1} = c, \] admits a solution in \(\mathcal{O}_{\widehat{K}}\) , resp. in \(U_{\widehat{K}}\) . If \(x^{\varphi} = x\) for \(x \in \mathcal{O}_{\widehat{K}}\) , then \(x \in \mathcal{O}_K\) .

Definition / construction

FC09-C05-U016 · Chapter V, §2, source L14062 · not formalized

For a power series \(F(X_{1},\ldots,X_{n})\in\mathcal{O}_{\widehat{K}}X_{1},\ldots,X_{n}\) , let \(F^{\varphi}\) be the power series in \(O_{\widehat{K}}X_{1},\ldots,X_{n}\) which arises from F by applying \(\varphi\) to the coefficients of F. A Lubin-Tate series for a prime element \(\pi\) of K is by definition a power series \(e(X)\in\mathcal{O}_{K}X\) with the properties \[ e (X) \equiv \pi X \bmod \deg 2 \quad \text { and } \quad e (X) \equiv X ^ {q} \bmod \pi , \] where \(q = q_{K}\) denotes, as always, the number of elements in the residue class field of K. The totality of all Lubin-Tate series is denoted by \(E_{\pi}\) . In \(E_{\pi}\) there are in particular the polynomials \[ e (X) = u X ^ {q} + \pi (a _ {q - 1} X ^ {q - 1} + \dots + a _ {2} X ^ {2}) + \pi X, \] where \(u, a_{i} \in O_{K}\) and \(u \equiv 1 \mod \pi\) . These are called the Lubin-Tate polynomials. The simplest one among them is the polynomial \(X^{q} + \pi X\) . In the case \(K = Q_{p}\) for example, \(e(X) = (1 + X)^{p} - 1\) is a Lubin-Tate polynomial for the prime element p.

Proposition (2.2)

FC09-C05-U017 · Chapter V, §2, source L14076 · not formalized

(2.2) Proposition. Let \(\pi\) and \(\overline{\pi}\) be prime elements of \(\widehat{K}\) , and let \(e(X) \in \mathcal{E}_{\pi}\) , \(\overline{e}(X) \in \mathcal{E}_{\overline{\pi}}\) be Lubin-Tate series. Let \(L(X_1, \ldots, X_n) = \sum_{i=1}^{n} a_i X_i\) be a linear form with coefficients \(a_i \in \mathcal{O}_{\widehat{K}}\) such that \[ \pi L (X _ {1}, \dots , X _ {n}) = \overline {{\pi}} L ^ {\varphi} (X _ {1}, \dots , X _ {n}). \] Then there is a uniquely determined power series \(F(X_{1},\ldots ,X_{n}) \in \mathcal{O}_{\widehat{K}}X_1,\dots ,X_n\) satisfying \[ F (X _ {1}, \dots , X _ {n}) \equiv L (X _ {1}, \dots , X _ {n}) \bmod \deg 2, \] \[ e \left(F \left(X _ {1}, \dots , X _ {n}\right)\right) = F ^ {\varphi} \left(\bar {e} \left(X _ {1}\right), \dots , \bar {e} \left(X _ {n}\right)\right). \] If the coefficients of \(e, \bar{e}, L\) lie in a complete subring \(\mathcal{O}\) of \(\mathcal{O}_{\hat{K}}\) such that \(\mathcal{O}^{\varphi} = \mathcal{O}\) , then \(F\) has coefficients in \(\mathcal{O}\) as well.

Corollary (2.3)

FC09-C05-U018 · Chapter V, §2, source L14154 · not formalized

(2.3) Corollary. Let \(\pi\) and \(\overline{\pi}\) be prime elements of \(K\) , and let \(e \in \mathcal{E}_{\pi}\) , \(\bar{e} \in \mathcal{E}_{\overline{\pi}}\) be Lubin-Tate series with coefficients in \(\mathcal{O}_K\) . Let \(\pi = u\overline{\pi}\) , \(u \in U_K\) , and \(u = \varepsilon^{\varphi - 1}\) , \(\varepsilon \in U_{\widehat{K}}\) . Then there is a uniquely determined power series \(\theta(X) \in \mathcal{O}_{\widehat{K}}X\) such that \(\theta(X) \equiv \varepsilon X \mod \deg 2\) and \[ e \circ \theta = \theta^ {\varphi} \circ \bar {e}. \] Furthermore, there is a uniquely determined power series \([u](X) \in \mathcal{O}_KX\) such that \([u](X) \equiv uX \bmod \deg 2\) and \[ \bar {e} \circ [ u ] = [ u ] \circ \bar {e}. \] They satisfy \[ \theta^ {\varphi} = \theta \circ [ u ]. \]

Theorem (2.4)

FC09-C05-U019 · Chapter V, §2, source L14176 · not formalized

(2.4) Theorem. Let \(a = up^{v_p(a)} \in \mathbb{Q}_p^*\) , and let \(\zeta\) be a primitive \(p^n\) -th root of unity. Then one has \[ \left(a, \mathbb {Q} _ {p} (\zeta) | \mathbb {Q} _ {p}\right) \zeta = \zeta^ {u ^ {- 1}}. \]

Definition / construction

FC09-C05-U020 · Chapter V, §3, source L14290 · not formalized

(bilinear in the multiplicative sense). This pairing is called the Hilbert symbol. Its relation to the norm residue symbol is described explicitly in the following proposition.

Not formalized. The project has a substantial quadratic Hilbert-symbol theory, but this source row is stated for the general n-th Hilbert symbol, tame n-th power residue symbol, or wild explicit reciprocity formula. Quadratic specialization is not credited to a general-n bundle.

Proposition (3.1)

FC09-C05-U021 · Chapter V, §3, source L14292 · not formalized

(3.1) Proposition. For \(a, b \in K^{*}\) , the Hilbert symbol \(\left(\frac{a,b}{\mathfrak{p}}\right) \in \mu_{n}\) is given by \[ \left(a, K (\sqrt [ n ]{b}) | K\right) \sqrt [ n ]{b} = \left(\frac {a , b}{\mathfrak {p}}\right) \sqrt [ n ]{b}. \]

Proposition (3.2)

FC09-C05-U022 · Chapter V, §3, source L14308 · not formalized

(3.2) Proposition. (i) \(\left(\frac{aa', b}{\mathfrak{p}}\right) = \left(\frac{a, b}{\mathfrak{p}}\right)\left(\frac{a', b}{\mathfrak{p}}\right),\) (ii) \(\left(\frac{a, bb'}{\mathfrak{p}}\right) = \left(\frac{a, b}{\mathfrak{p}}\right)\left(\frac{a, b'}{\mathfrak{p}}\right),\) (iii) \(\left(\frac{a,b}{\mathfrak{p}}\right) = 1\Longleftrightarrow a\) is a norm from the extension \(K(\sqrt[n]{b})|K,\) (iv) \(\left(\frac{a,b}{\mathfrak{p}}\right) = \left(\frac{b,a}{\mathfrak{p}}\right)^{-1},\) (v) \(\left(\frac{a,1 - a}{\mathfrak{p}}\right) = 1\) and \(\left(\frac{a, - a}{\mathfrak{p}}\right) = 1,\) (vi) If \(\left(\frac{a,b}{\mathfrak{p}}\right) = 1\) for all \(b\in K^{*}\) , then \(a\in K^{*n}\) .

Definition / construction

FC09-C05-U023 · Chapter V, §3, source L14356 · not formalized

Next we determine the Hilbert symbol explicitly in the case where K is a local field \((\neq\mathbb{R},\mathbb{C})\) whose residue characteristic p does not divide n. We call this the case of the tame Hilbert symbol. Since \(\mu_{n}\subseteq\mu_{q-1}\) one has \(n|q-1\) in that case. First we establish the lemma (3.3): for \((n,p) = 1\) and \(x \in K^{*}\), the extension \(K(\sqrt[n]{x})|K\) is unramified if and only if \(x \in U_{K}K^{*n}\).

Lemma (3.3)

FC09-C05-U024 · Chapter V, §3, source L14358 · not formalized

(3.3) Lemma. Let \((n, p) = 1\) and \(x \in K^{*}\) . The extension \(K(\sqrt[n]{x})|K\) is unramified if and only if \(x \in U_{K}K^{*n}\) .

Proposition (3.4)

FC09-C05-U025 · Chapter V, §3, source L14370 · not formalized

(3.4) Proposition. If \((n, p) = 1\) and \(a, b \in K^{*}\) , then \[ \left(\frac {a , b}{\mathfrak {p}}\right) = \omega \left((- 1) ^ {\alpha \beta} \frac {b ^ {\alpha}}{a ^ {\beta}}\right) ^ {(q - 1) / n}, \] where \(\alpha = v_{K}(a),\beta = v_{K}(b)\)

Definition / construction

FC09-C05-U026 · Chapter V, §3, source L14416 · not formalized

The symbol is called the Legendre symbol, or the \(n\)-th power residue symbol. Both names are justified by proposition (3.5): for \((n,p) = 1\) and \(u \in U_{K}\), one has \(\left(\frac{u}{\mathfrak{p}}\right) = 1\) if and only if \(u\) is an \(n\)-th power \(\bmod \mathfrak{p}_{K}\).

Proposition (3.5)

FC09-C05-U027 · Chapter V, §3, source L14418 · not formalized

(3.5) Proposition. Let \((n, p) = 1\) and \(u \in U_K\) . Then one has \[ \left(\frac {u}{\mathfrak {p}}\right) = 1 \quad \Longleftrightarrow \quad u \text { is an } n \text {-th power mod } \mathfrak {p} _ {K}. \]

Theorem (3.6)

FC09-C05-U028 · Chapter V, §3, source L14440 · in lean-categories

(3.6) Theorem. Let \(n = 2\) . For \(a, b \in \mathbb{Q}_p^*\) we write \[ a = p ^ {\alpha} a ^ {\prime}, \quad b = p ^ {\beta} b ^ {\prime}, \quad a ^ {\prime}, b ^ {\prime} \in U _ {\mathbb {Q} _ {p}}. \] If \(p \neq 2\) , then \[ \left(\frac {a , b}{p}\right) = (- 1) ^ {\frac {p - 1}{2} \alpha \beta} \left(\frac {a ^ {\prime}}{p}\right) ^ {\beta} \left(\frac {b ^ {\prime}}{p}\right) ^ {\alpha}. \] In particular, one has \(\left(\frac{p,p}{p}\right) = (-1)^{(p - 1) / 2}\) and \(\left(\frac{p,u}{p}\right) = \left(\frac{u}{p}\right)\) , if \(u\) is a unit. If \(p = 2\) and \(a,b\in U_{\mathbb{Q}_2}\) , then \[ \left(\frac {2 , a}{2}\right) = (- 1) ^ {(a ^ {2} - 1) / 8}, \] \[ \left(\frac {a , b}{2}\right) = \left(\frac {b , a}{2}\right) = (- 1) ^ {\frac {a - 1}{2} \frac {b - 1}{2}}. \]

Formalized. LeanCategories/Lattices/Valued/PadicMixedSymbol.lean::hilbertSymbol_odd_formula, hilbertSymbol_p_p, hilbertSymbol_unit_p; LeanCategories/Lattices/Valued/DyadicSymbol.lean::hilbertSymbol_dyadic_formula — The project proves the closed odd-prime formula in valuation/unit-part coordinates and the closed dyadic formula (-1)^(ε(u)ε(v)+αω(v)+βω(u)). Translating residueChar to the Legendre symbol gives Neukirch’s odd-p formula; specializing the dyadic formula to (2,a) and to two units gives exactly the two displayed p=2 identities.

Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C05-U029 · Chapter V, §3, source L14480 · not formalized

So let \(\mu_{p^{\nu}} \subseteq K\) , choose a prime element \(\pi\) of \(K\) , and let \(W\) be the ring of integers of the maximal unramified subextension \(T\) of \(K|\mathbb{Q}_p\) (i.e., the ring of Witt vectors over the residue class field of \(K\) ). Then every element \(x \in K\) can be written in the form \[ x = f (\pi), \] with a Laurent series \(f(X) \in W((X))\) . For an arbitrary Laurent series \(f(X) = \sum_{i\geq -m}a_iX^i\in W((X))\) , let \(f^{\mathcal{P}}(X)\) denote the series \[ f ^ {\mathcal {P}} (X) = \sum_ {i} a _ {i} ^ {\varphi} X ^ {i p}, \] where \(\varphi\) is the Frobenius automorphism of W. Further, let \(\operatorname{Res}(fdX) \in W\) denote the residue of the differential fdX, \[ d \log f := \frac {f ^ {\prime}}{f} d X, \] and \[ \log f := \sum_ {i = 1} ^ {\infty} (- 1) ^ {i + 1} \frac {(f - 1) ^ {i}}{i}, \] if \(f \in 1 + pWX\) .

Theorem (3.7)

FC09-C05-U030 · Chapter V, §3, source L14528 · not formalized

(3.7) Theorem. If \(x, y \in K^*\) and \(f, g \in W((X))^*\) such that \(f(\pi) = x\) and \(g(\pi) = y\) , then \[ \left(\frac {x , y}{\mathfrak {p}}\right) = \zeta^ {w (x, y)} \] where \[ w (x, y) = T r _ {W | \mathbb {Z} _ {p}} \operatorname{Res} h \cdot \left(\frac {1}{p} \log \frac {f ^ {p}}{f ^ {\mathcal {P}}} d \log g - \frac {1}{p} \log \frac {g ^ {p}}{g ^ {\mathcal {P}}} \frac {1}{p} d \log f ^ {\mathcal {P}}\right) \bmod p ^ {\nu}. \]

Proposition (3.8)

FC09-C05-U031 · Chapter V, §3, source L14550 · not formalized

(3.8) Proposition. For \(a \in U_{\Phi_{\nu}}^{(2p^{\nu - 1})}\) and \(b \in \Phi_{\nu}^{*}\) one has \[ \left(\frac {a , b}{\mathfrak {p}}\right) = \zeta^ {S (\zeta \log a D \log b) / p ^ {\nu}},\tag{1} \] where \(D \log b\) denotes the formal logarithmic derivative in \(\pi\) of an arbitrary representation of b as an integral power series in \(\pi\) with coefficients in \(Z_{p}\) . For \(a \in U_{\Phi_v}^{(1)}\) one has furthermore the two supplementary theorems (2) \[ \left(\frac {\zeta , a}{\mathfrak {p}}\right) = \zeta^ {S (\log a) / p ^ {\nu}},\tag{3} \] \[ \left(\frac {a , \pi}{\mathfrak {p}}\right) = \zeta^ {S ((\zeta / \pi) \log a) / p ^ {\nu}}. \]

Convention / notation

FC09-C05-U032 · Chapter V, §3, source L14576 · not formalized

one may also interpret the \(\zeta\) -exponent in the formulae (1)-(3) as the \((p-1)\) -st coefficient of a \(\pi\) -adic expansion of \(\log a D \log b\) . In this way it appears as a formal residue \(\mathrm{Res}_{\pi} \frac{1}{\pi^p} \log a D \log b\) . As to the supplementary theorems, one has to define also \(D \log \zeta = -\zeta^{-1}\) , \(D \log \pi = \pi^{-1}\) .

Definition (4.1)

FC09-C05-U033 · Chapter V, §4, source L14648 · in Mathlib

(4.1) Definiton. A (1-dimensional, commutative) formal group over a ring \(\mathcal{O}\) is a formal power series \(F(X,Y)\in \mathcal{O}X,Y\) with the following properties: (i) \(F(X,Y)\equiv X + Y\bmod \deg 2,\) \[ \begin{array}{l l} \text {(ii)} & F (X, Y) = F (Y, X) \\ \text {(iii)} & F (X, F (Y, Z)) = F (F (X, Y), Z) \end{array} \qquad \begin{array}{l l} \text {``commutativity''}, \\ \text {``associativity''.} \end{array} \]

Formalized. Mathlib/RingTheory/FormalGroup/Basic.lean::structure FormalGroup, class FormalGroup.IsComm — FormalGroup packages a two-variable formal power series with zero constant term, unit linear X/Y coefficients and associativity; FormalGroup.IsComm adds symmetry. The basic file derives the identity laws, so this is precisely Neukirch’s one-dimensional commutative formal-group definition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (4.2)

FC09-C05-U034 · Chapter V, §4, source L14696 · in another Lean project

(4.2) Definition. A homomorphism \(f: F \to G\) between two formal groups is a power series \(f(X) = a_{1}X + a_{2}X^{2} + \cdots \in \mathcal{O}X\) such that \[ f (F (X, Y)) = G \big (f (X), f (Y) \big). \]

Formalized. leanprover-community/mathlib4#38213@133714768d42ba1a6107b7a84e2d22222c7c69ed/Mathlib/RingTheory/FormalGroup/Hom.lean::structure FormalGroupHom — Open PR #38213 defines FormalGroupHom F G as a power series with zero constant term satisfying exactly f(F(X,Y)) = G(f(X),f(Y)), matching Definition 4.2.

Searched: O=133714768d42ba1a6107b7a84e2d22222c7c69ed (open draft PR #38213); P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C05-U035 · Chapter V, §4, source L14702 · not formalized

In example 3, for instance, the power series f is a homomorphism of the formal group F to the additive group \(G_{a}\) . It is called the logarithm of F.

Not formalized. Pinned Mathlib has the core formal-group-law object, and open PR #38213 adds formal-group homomorphisms; this row additionally requires a formal logarithm, endomorphism ring, formal O-module, or Lubin–Tate module construction/classification that is not exported by a checked compatible owner.

Definition / construction

FC09-C05-U036 · Chapter V, §4, source L14704 · in another Lean project

A homomorphism \(f: F \to G\) is an isomorphism if \(a_1 = f'(0)\) is a unit, i.e., if there is a homomorphism \(g = f^{-1}: G \to F\) such that \[ f (g (X)) = g (f (X)) = X. \]

Formalized. leanprover-community/mathlib4#38213@133714768d42ba1a6107b7a84e2d22222c7c69ed/Mathlib/RingTheory/FormalGroup/Hom.lean::structure FormalGroupHom, structure FormalGroupIso; Mathlib/RingTheory/PowerSeries/Substitution.lean::substInvOfIsUnit, subst_substInvOfIsUnit_right, subst_substInvOfIsUnit_left — FormalGroupIso packages a homomorphism with a two-sided homomorphic substitution inverse. Conversely, a homomorphism whose linear coefficient is a unit has the pinned substitution inverse; cancelling the original homomorphism in the homomorphism identity shows that inverse also respects the formal-group law. The reverse implication follows by comparing linear coefficients in the two substitution identities.

Searched: O=133714768d42ba1a6107b7a84e2d22222c7c69ed (open draft PR #38213); P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C05-U037 · Chapter V, §4, source L14710 · in another Lean project

If the power series \(f(X) = a_{1}X + a_{2}X^{2} + \cdots\) satisfies the equation \(f(F(X,Y)) = G(f(X), f(Y))\) , but its coefficients belong to an extension ring \(O'\) , then we call this a homomorphism defined over \(O'\) . The following proposition is immediately evident.

Formalized. leanprover-community/mathlib4#38213@133714768d42ba1a6107b7a84e2d22222c7c69ed/Mathlib/RingTheory/FormalGroup/Hom.lean::structure FormalGroupHom; Mathlib/RingTheory/FormalGroup/Basic.lean::def map (f : R →+* S) — Pinned FormalGroup.map base-changes a formal group along a ring map. A FormalGroupHom between the resulting base-changed groups over an extension ring is exactly Neukirch’s notion of a homomorphism “defined over” that extension ring.

Searched: O=133714768d42ba1a6107b7a84e2d22222c7c69ed (open draft PR #38213); P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (4.3)

FC09-C05-U038 · Chapter V, §4, source L14712 · not formalized

(4.3) Proposition. The homomorphisms \(f: F \to F\) of a formal group \(F\) over \(\mathcal{O}\) form a ring \(\operatorname{End}_{\mathcal{O}}(F)\) in which addition and multiplication are defined by \[ (f \underset {F} {+} g) (X) = F \big (f (X), g (X) \big), \quad (f \circ g) (X) = f \big (g (X) \big). \]

Definition (4.4)

FC09-C05-U039 · Chapter V, §4, source L14718 · not formalized

(4.4) Definition. A formal \(\mathcal{O}\) -module is a formal group \(F\) over \(\mathcal{O}\) together with a ring homomorphism \[ \mathcal {O} \longrightarrow \operatorname{End} _ {\mathcal {O}} (F), \quad a \longmapsto [ a ] _ {F} (X), \] such that \([a]_F(X) \equiv aX \mod \deg 2\) .

Definition (4.5)

FC09-C05-U040 · Chapter V, §4, source L14734 · not formalized

(4.5) Definition. A Lubin-Tate module over \(O_{K}\) for the prime element \(\pi\) is a formal \(O_{K}\) -module F such that \[ [ \pi ] _ {F} (X) \equiv X ^ {q} \bmod \pi . \]

Example / comparison

FC09-C05-U041 · Chapter V, §4, source L14742 · after FC09-C05-U017 · not formalized

Example: The formal multiplicative group \(\mathbb{G}_m\) is a formal \(\mathbb{Z}_p\) -module with respect to the mapping \[ \mathbb {Z} _ {p} \rightarrow \operatorname{End} _ {\mathbb {Z} _ {p}} (\mathbb {G} _ {m}), \quad a \mapsto [ a ] _ {\mathbb {G} _ {m}} (X) = (1 + X) ^ {a} - 1 = \sum_ {\nu = 1} ^ {\infty} \binom {a} {\nu} X ^ {\nu}. \] \(\mathbb{G}_m\) is a Lubin-Tate module for the prime element \(p\) because \[ [ p ] _ {\mathbb {G} _ {m}} (X) = (1 + X) ^ {p} - 1 \equiv X ^ {p} \bmod p. \] The following theorem gives a complete and explicit overall view of the totality of all Lubin-Tate modules. Let \(e(X)\) , \(\bar{e}(X) \in \mathcal{O}_KX\) be Lubin-Tate series for the prime element \(\pi\) of K, and let \[ F _ {e} (X, Y) \in \mathcal {O} _ {K} [ [ X, Y ] ] \quad \text { and } \quad [ a ] _ {e, \bar {e}} (X) \in \mathcal {O} _ {K} [ [ X ] ] \] \((a \in \mathcal{O}_{K})\) be the power series (uniquely determined according to (2.2)) such that \[ F _ {e} (X, Y) \equiv X + Y \bmod {\deg 2}, \quad e \big (F _ {e} (X, Y) \big) = F _ {e} \big (e (X), e (Y) \big), \] \[ [ a ] _ {e, \bar {e}} (X) \equiv a X \bmod \deg 2, \quad e ([ a ] _ {e, \bar {e}} (X)) = [ a ] _ {e, \bar {e}} (\bar {e} (X)). \] If \(e(X) = \bar{e}(X)\) we simply write \([a]_{e,\bar{e}}(X) = [a]_e(X)\) .

Theorem (4.6)

FC09-C05-U042 · Chapter V, §4, source L14772 · not formalized

(4.6) Theorem. (i) The Lubin-Tate modules for \(\pi\) are precisely the series \(F_{e}(X,Y)\) , with the formal \(\mathcal{O}_K\) -module structure given by \[ \mathcal {O} _ {K} \longrightarrow \operatorname{End} _ {\mathcal {O} _ {K}} (F _ {e}), \quad a \longmapsto [ a ] _ {e} (X). \] (ii) For every \(a \in \mathcal{O}_K\) the power series \([a]_{e,\bar{e}}(X)\) is a homomorphism \[ [ a ] _ {e, \bar {e}}: F _ {\bar {e}} \longrightarrow F _ {e} \] of formal O-modules, and it is an isomorphism if a is a unit.

Proposition (5.1)

FC09-C05-U043 · Chapter V, §5, source L14850 · not formalized

(5.1) Proposition. Let \(F\) be a formal \(\mathcal{O}_{K}\) -module. Then the set \(\overline{\mathfrak{p}}\) with the operations \[ x + _ {F} y = F (x, y) \quad \text { and } \quad a \cdot x = [ a ] _ {F} (x), \] \(x, y \in \overline{\mathfrak{p}}, a \in \mathcal{O}_K\) , is an \(\mathcal{O}_K\) -module in the usual sense. We denote it by \(\overline{\mathfrak{p}}_F\) . If \(f: F \to G\) is a homomorphism (isomorphism) of formal \(\mathcal{O}_K\) -modules, then \[ f: \overline {{{\mathfrak {p}}}} _ {F} \longrightarrow \overline {{{\mathfrak {p}}}} _ {G}, \quad x \longmapsto f (x), \] is a homomorphism (isomorphism) of ordinary \(O_{K}\) -modules.

Not formalized. No checked Lean source found supplies Lubin–Tate formal-module points/division points, their rank-one structure, the Lubin–Tate extension tower, Galois action, reciprocity law, class-field identification, or maximal-abelian-extension theorem required by this full row.

Definition / construction

FC09-C05-U044 · Chapter V, §5, source L14868 · not formalized

We now consider a Lubin-Tate module \(F\) for the prime element \(\pi\) of \(\mathcal{O}_K\) . We define the group of \(\pi^n\) -division points by \[ F (n) = \left\{\lambda \in \overline {{{\mathfrak {p}}}} _ {F} \mid \pi^ {n} \cdot \lambda = 0 \right\} = \ker \left([ \pi^ {n} ] _ {F}\right). \] This is an \(O_{K}\) -module, and an \(O_{K}/\pi^{n}O_{K}\) -module because it is killed by \(\pi^{n}O_{K}\) .

Proposition (5.2)

FC09-C05-U045 · Chapter V, §5, source L14876 · not formalized

(5.2) Proposition. \(F(n)\) is a free \(\mathcal{O}_K / \pi^n\mathcal{O}_K\) -module of rank 1.

Corollary (5.3)

FC09-C05-U046 · Chapter V, §5, source L14886 · not formalized

(5.3) Corollary. Associating \(a \mapsto [a]_F\) we obtain canonical isomorphisms \[ \mathcal {O} _ {K} / \pi^ {n} \mathcal {O} _ {K} \longrightarrow \operatorname{End} _ {\mathcal {O} _ {K}} (F (n)) \quad \text { and } \quad U _ {K} / U _ {K} ^ {(n)} \longrightarrow \operatorname{Aut} _ {\mathcal {O} _ {K}} (F (n)). \]

Definition / construction

FC09-C05-U047 · Chapter V, §5, source L14894 · after FC09-C05-U042 · not formalized

Given a Lubin-Tate module \(F\) for the prime element \(\pi\) , we now define the field of \(\pi^n\) -division points by \[ L _ {n} = K (F (n)). \] Since \(F(n) \subseteq F(n + 1)\) we get a tower of fields \[ K \subseteq L _ {1} \subseteq L _ {2} \subseteq \dots \subseteq L _ {\pi} := \bigcup_ {n = 1} ^ {\infty} L _ {n}. \] These fields are also called the Lubin-Tate extensions. They only depend on the prime element \(\pi\) , not on the Lubin-Tate module \(F\) . For if \(G\) is another Lubin-Tate module for \(\pi\) , then by (4.6), there is an isomorphism \(f: F \to G\) , \(f \in \mathcal{O}_KX\) such that \(G(n) = f(F(n)) \subseteq K(F(n))\) , and hence \(K(G(n)) = K(F(n))\) . If \(F\) is the Lubin-Tate module \(F_e\) belonging to a Lubin-Tate polynomial \(e(X) \in \mathcal{E}_{\pi}\) , then \(e(X) = [\pi]_F(X)\) and \(L_n|K\) is the splitting field of the \(n\) -fold iteration \[ e ^ {n} (X) = (e \circ \dots \circ e) (X) = [ \pi^ {n} ] _ {F} (X). \]

Example / comparison

FC09-C05-U048 · Chapter V, §5, source L14912 · not formalized

Example: If \(\mathcal{O}_K = \mathbb{Z}_p\) and \(F\) is the Lubin-Tate module \(\mathbb{G}_m\) , then \[ e ^ {n} (X) = [ p ^ {n} ] _ {\mathbb {G} _ {m}} (X) = (1 + X) ^ {p ^ {n}} - 1. \] So \(\mathbb{G}_{m}(n)\) consists of the elements \(\zeta-1\) , where \(\zeta\) varies over the \(p^{n}\) -th roots of unity. \(L_{n}|K\) is therefore the \(p^{n}\) -th cyclotomic extension \(\mathbb{Q}_{p}(\mu_{p^{n}})|\mathbb{Q}_{p}\) . The following theorem shows the complete analogy of Lubin-Tate extensions with cyclotomic fields.

Theorem (5.4)

FC09-C05-U049 · Chapter V, §5, source L14920 · not formalized

(5.4) Theorem. \(L_{n}|K\) is a totally ramified abelian extension of degree \(q^{n - 1}(q - 1)\) with Galois group \[ G (L _ {n} | K) \cong \operatorname{Aut} _ {\mathcal {O} _ {K}} (F (n)) \cong U _ {K} / U _ {K} ^ {(n)}, \] i.e., for every \(\sigma \in G(L_n|K)\) there is a unique class \(u \bmod U_K^{(n)}\) , with \(u \in U_K\) such that \[ \lambda^ {\sigma} = [ u ] _ {F} (\lambda) \quad f o r \quad \lambda \in F (n). \] Furthermore the following is true: let \(F\) be the Lubin-Tate module \(F_{e}\) associated to the polynomial \(e(X) \in \mathcal{E}_{\pi}\) , and let \(\lambda_{n} \in F(n) \setminus F(n-1)\) . Then \(\lambda_{n}\) is a prime element of \(L_{n}\) , i.e., \(L_{n} = K(\lambda_{n})\) , and \[ \phi_ {n} (X) = \frac {e ^ {n} (X)}{e ^ {n - 1} (X)} = X ^ {q ^ {n - 1} (q - 1)} + \dots + \pi \in \mathcal {O} _ {K} [ X ] \] is its minimal polynomial. In particular one has \(N_{L_n|K}(-\lambda_n) = \pi\) .

Theorem (5.5)

FC09-C05-U050 · Chapter V, §5, source L14970 · not formalized

(5.5) Theorem. For the field \(L_{n}|K\) of \(\pi^n\) -division points and for \(a = u\pi^{v_K(a)} \in K^*, u \in U_K\) , one has \[ (a, L _ {n} | K) \lambda = [ u ^ {- 1} ] _ {F} (\lambda), \quad \lambda \in F (n). \]

Corollary (5.6)

FC09-C05-U051 · Chapter V, §5, source L15014 · not formalized

(5.6) Corollary. The field \(L_{n}|K\) of \(\pi^n\) -division points is the class field relative to the group \((\pi)\times U_K^{(n)}\subseteq K^*\) .

Corollary (5.7)

FC09-C05-U052 · Chapter V, §5, source L15028 · not formalized

(5.7) Corollary. The maximal abelian extension of \(K\) is the composite \[ K ^ {a b} = \widetilde {K} L _ {\pi}, \] where \(L_{\pi}\) is the union \(\bigcup_{n=1}^{\infty} L_n\) of the fields \(L_n\) of \(\pi^n\) -division points.

Proposition (6.1)

FC09-C05-U053 · Chapter V, §6, source L15152 · not formalized

(6.1) Proposition. Let \(L_{n}|K\) be the field of \(\pi^n\) -division points of a Lubin-Tate module for the prime element \(\pi\) . Then \[ G _ {i} (L _ {n} | K) = G (L _ {n} | L _ {k}) \quad \text { for } \quad q ^ {k - 1} \leq i \leq q ^ {k} - 1. \]

Not formalized. Current Mathlib still lacks lower/upper-numbered higher ramification groups (the ramification-group file explicitly retains the lower-numbering TODO), so the Lubin–Tate ramification filtration, reciprocity compatibility, jump definition in that interface, and Hasse–Arf theorem are not source-completely owned.

Theorem (6.2)

FC09-C05-U054 · Chapter V, §6, source L15186 · not formalized

(6.2) Theorem. If \(L|K\) is a finite abelian extension, then the norm residue symbol \[ (\quad , L | K): K ^ {*} \longrightarrow G (L | K) \] maps the group \(U_K^{(n)}\) onto the group \(G^n (L|K)\) , for \(n\geq 0\) .

Definition / construction

FC09-C05-U055 · Chapter V, §6, source L15216 · not formalized

Higher ramification groups \(G^{t}(L|K)\) were introduced for arbitrary real numbers \(t \geq -1\) . Thus we may ask for which numbers they change. We call these numbers the jumps of the filtration \(\{G^{t}(L|K)\}_{t \geq -1}\) of \(G(L|K)\) . In other words, t is a jump if for all \(\varepsilon > 0\) , one has \[ G ^ {t} (L | K) \neq G ^ {t + \varepsilon} (L | K). \]

Proposition (6.3)

FC09-C05-U056 · Chapter V, §6, source L15222 · not formalized

(6.3) Proposition \((H_{ASSE}-A_{RF})\) . For a finite abelian extension \(L|K\) , the jumps of the filtration \(\{G^{t}(L|K)\}_{t\geq-1}\) of \(G(L|K)\) are rational integers.