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

FC09 — Neukirch, Algebraic Number Theory.

This chapter contains 30 definitions, 14 theorems, 27 propositions, 3 lemmas, 9 corollaries, 6 conventions and 1 other statements.

Of the 90 statements checked against Lean, 4 are formalized somewhere and 86 are not.

Status	Statements	Share	What it means
not formalized	86	96%	A documented search found no Lean statement of it anywhere.
in Mathlib	3	3%	Mathlib states and proves it.
in lean-categories	1	1%	This repository states and proves it.
checked in total	90

Which versions of Lean and Mathlib were searched

Canonical source block: FC09 Neukirch Chapter VI, FC09-C06-U001–FC09-C06-U090, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 90 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). LeanCategories/Algebra/IdeleGroup.lean provides the restricted-product idèle group, principal idèles, local compactness/Haar measure, and the quotient IdeleClassGroup; only U005 is source-complete because Neukirch U002 additionally bundles the finite-S idèle subgroups and their exhaustion of all idèles. No project S-idèle, ray-class, global idèle-norm, Artin-symbol, or global reciprocity layer was found.
Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Its adèle stack (AdeleRing, finite restricted products, infinite completions) closes U001. The native Jacobi implementation closes U090 and, via its signed-numerator, quadratic-reciprocity, and supplementary-character theorems, closes the full signed Gauss reciprocity package U089. Ordinary class groups, S-integers, local norms, transfer, and Frobenius infrastructure do not close any further global-CFT bundle; notably SInteger.lean still lists finite generation/Dirichlet’s S-unit theorem as TODO.
Current Mathlib was checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. There is still no first-class idèle, ray-class, global reciprocity, or Hilbert-class-field module. Targeted open-PR searches found no idèle/ray/Artin-symbol work. Open PR #42687 at O=a40561e249ebf45d2870f5d9d45bc2eb4d80b242 provides abstract class-formation infrastructure but no global reciprocity theorem or global instance. Open PR #40661 at O=184a5900ddc04998dd9d5976cb9c242f265dd56b is explicitly a file of *_wanted Hilbert-class-field statements and contains an unfinished sorry, so it is not a reference-port owner.
External global-CFT discovery was checked rather than inferred. kbuzzard/ClassFieldTheory has no global adèle/idèle/Artin/ray-class layer. acmepjz/lean-iwasawa@7fffeb8c80fbe13f989f318c23cbb0dcf2230092 (Apache-2.0) contains experimental Hilbert-class-field and Artin-map files, but artinMap, surjectivity, Artin equivalence, and related maximal-unramified results explicitly depend on sorrys. TauCeti at R=2c1e8865b4b9bf705ce1e43a8e50d27145f24f6a (Apache-2.0) has substantial Frobenius/Artin-prime and Chebotarev setup, but not the Chebotarev density theorem itself, so it does not close U035–U036; its Artin-prime layer also lacks the local-reciprocity/idèle compatibility bundled in U074–U076.
Strict bundle semantics was enforced. The headline IdeleGroup object does not earn U002 without its S-idèle subgroups/exhaustion; a principal-idèle map does not earn U003 without the S-unit identification; generic coinduction/Tate cohomology does not earn U026–U034 without the actual global idèle/S-unit G-modules; Frobenius definitions do not earn Artin reciprocity; generic transfer does not earn Furtwängler’s U082 triviality theorem; and the project’s quadratic local Hilbert symbols do not earn the general n-th Hilbert product/power-residue laws U085–U088.
Short derivations are credited only where all ingredients are checked. U089 applies native Jacobi reciprocity to absolute values, uses jacobiSym.neg to account for signed generators, and uses at_neg_one, at_two, and the explicit quadratic characters for the two supplementary laws. No global class-field theorem is smuggled into that route.
All mathlib targets were path/token validated against P, U005 project targets against A, and the negative current/open/external checks against H/#42687/#40661 and the inspected external revisions.
Route totals for C06: mathlib 3, project-existing 1, package-import 0, reference-port 0, unmatched 86.

Definition / construction

FC09-C06-U001 · Chapter VI, §1, source L15234 · in Mathlib

An adèle of K — this curious expression, which has the stress on the second syllable, is derived from the original term “additive idèle” — is a family \[ \alpha = (\alpha_ {\mathfrak {p}}) \] of elements \(\alpha_{\mathfrak{p}} \in K_{\mathfrak{p}}\) where \(\mathfrak{p}\) runs through all primes of \(K\) , and \(\alpha_{\mathfrak{p}}\) is integral in \(K_{\mathfrak{p}}\) for almost all \(\mathfrak{p}\) . The adèles form a ring, which is denoted by \[ \mathbb {A} _ {K} = \prod_ {\mathfrak {p}} K _ {\mathfrak {p}}. \] Addition and multiplication are defined componentwise. This kind of product is called the “restricted product” of the \(K_{p}\) with respect to the subrings \(O_{p} \subseteq K_{p}\) .

Formalized. Mathlib/NumberTheory/NumberField/AdeleRing.lean::def AdeleRing; Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean::def FiniteAdeleRing; Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean::def RestrictedProduct; Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean::def InfiniteAdeleRing — AdeleRing (𝓞 K) K is exactly the product of all infinite completions with the finite restricted product whose components are integral almost everywhere. This is Neukirch’s adèle ring, with componentwise ring operations.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C06-U002 · Chapter VI, §1, source L15248 · not formalized

The idèle group of K is defined to be the unit group \[ I _ {K} = \mathbb {A} _ {K} ^ {*}. \] Thus an idèle is a family \[ \alpha = (\alpha_ {\mathfrak {p}}) \] of elements \(\alpha_{\mathfrak{p}} \in K_{\mathfrak{p}}^{*}\) where \(\alpha_{\mathfrak{p}}\) is a unit in the ring \(\mathcal{O}_{\mathfrak{p}}\) of integers of \(K_{\mathfrak{p}}\) , for almost all \(\mathfrak{p}\) . In analogy with \(\mathbb{A}_K\) , we write the idèle group as the restricted product \[ I _ {K} = \prod_ {\mathfrak {p}} K _ {\mathfrak {p}} ^ {*} \] with respect to the unit groups \(\mathcal{O}_{\mathfrak{p}}^{*}\) . For every finite set of primes \(S\) , \(I_{K}\) contains the subgroup \[ I _ {K} ^ {S} = \prod_ {\mathfrak {p} \in S} K _ {\mathfrak {p}} ^ {*} \times \prod_ {\mathfrak {p} \not \in S} U _ {\mathfrak {p}} \] of \(S\) -idèles, where \(U_{\mathfrak{p}} = K_{\mathfrak{p}}^{*}\) for \(\mathfrak{p}\) infinite complex, and \(U_{\mathfrak{p}} = \mathbb{R}_{+}^{*}\) for \(\mathfrak{p}\) infinite real. One clearly has \[ I _ {K} = \bigcup_ {S} I _ {K} ^ {S}, \] if \(S\) varies over all finite sets of primes of \(K\) .

Not formalized. Pinned Mathlib has the adèle ring, ordinary class groups and S-integer/S-unit definitions, and the project has a first-class idèle/idèle-class layer. This full row additionally needs an S-idèle exhaustion, S-unit theorem, idèlic ideal/norm map, compact norm-one class group, congruence/ray-class group, or narrow class exact sequence not exported by the checked interfaces.

Definition / construction

FC09-C06-U003 · Chapter VI, §1, source L15280 · not formalized

The inclusions \(K \subseteq K_{\mathfrak{p}}\) allow us to define the diagonal embedding \[ K ^ {*} \longrightarrow I _ {K}, \] which associates to \(a \in K^{*}\) the idèle \(\alpha \in I_{K}\) whose p-th component is the element a in \(K_{p}\) . We thus view \(K^{*}\) as a subgroup of \(I_{K}\) and we call the elements of \(K^{*}\) in \(I_{K}\) principal idèles. The intersection \[ K ^ {S} = K ^ {*} \cap I _ {K} ^ {S} \] consists of the numbers \(a \in K^{*}\) which are units at all primes \(\mathfrak{p} \notin S\) , \(\mathfrak{p} \nmid \infty\) , and which are positive in \(K_{\mathfrak{p}} = \mathbb{R}\) for all real infinite places \(\mathfrak{p} \notin S\) . They are called \(S\) -units. In particular, for the set \(S_{\infty}\) of infinite places, \(K^{S_{\infty}}\) is the unit group \(\mathcal{O}_{K}^{*}\) of \(\mathcal{O}_{K}\) . We get the following generalization of Dirichlet’s unit theorem.

Proposition (1.1)

FC09-C06-U004 · Chapter VI, §1, source L15294 · not formalized

(1.1) Proposition. If \(S\) contains all infinite places, then the homomorphism \[ \lambda : K ^ {S} \longrightarrow \prod_ {\mathfrak {p} \in S} \mathbb {R}, \quad \lambda (a) = \left(\log | a | _ {\mathfrak {p}}\right) _ {\mathfrak {p} \in S}, \] has kernel \(\mu(K)\) , and its image is a complete lattice in the \((s-1)\) -dimensional trace-zero space \(H = \left\{(x_{\mathfrak{p}}) \in \prod_{\mathfrak{p} \in S} \mathbb{R} \mid \sum_{\mathfrak{p} \in S} x_{\mathfrak{p}} = 0\right\}\) , \(s = \#S\) .

Definition (1.2)

FC09-C06-U005 · Chapter VI, §1, source L15336 · in lean-categories

(1.2) Definition. The elements of the subgroup \(K^{*}\) of \(I_{K}\) are called principal idèles and the quotient group \[ C _ {K} = I _ {K} / K ^ {*} \] is called the idèle class group of \(K\) .

Formalized. LeanCategories/Algebra/IdeleGroup.lean::def principalIdele, abbrev PrincipalIdeleSubgroup, abbrev IdeleClassGroup — principalIdele is the diagonal embedding of Kˣ; PrincipalIdeleSubgroup is its range and IdeleClassGroup is literally the quotient IdeleGroup K ⧸ PrincipalIdeleSubgroup K, exactly Definition 1.2.

Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (1.3)

FC09-C06-U006 · Chapter VI, §1, source L15382 · not formalized

(1.3) Proposition. \(Cl_K \cong I_K / I_K^{S_\infty} K^*\) , and \(\text{Pic}(\overline{\mathcal{O}}) \cong I_K / I_K^0 K^*\) .

Proposition (1.4)

FC09-C06-U007 · Chapter VI, §1, source L15386 · not formalized

(1.4) Proposition. \(I_K = I_K^S K^*\) , i.e., \(C_K = I_K^S K^* / K^*\) , if \(S\) is a sufficiently big finite set of places of \(K\) .

Proposition (1.5)

FC09-C06-U008 · Chapter VI, §1, source L15400 · not formalized

(1.5) Proposition. \(K^{*}\) is a discrete, and therefore closed, subgroup of \(I_{K}\) .

Definition / construction

FC09-C06-U009 · Chapter VI, §1, source L15416 · after FC09-C03-U006, FC09-C06-U006 · not formalized

As \(K^{*}\) is closed in \(I_{K}\) , the fact that \(I_{K}\) is a locally compact Hausdorff topological group carries over to the idèle class group \(C_{K} = I_{K}/K^{*}\) . For any idèle \(\alpha = (\alpha_{\mathfrak{p}}) \in I_{K}\) , its class in \(C_{K}\) will be denoted by \([\alpha]\) . We define the absolute norm of \(\alpha\) to be the real number \[ \mathfrak {N} (\alpha) = \prod_ {\mathfrak {p}} \mathfrak {N} (\mathfrak {p}) ^ {v _ {\mathfrak {p}} \left(\alpha_ {\mathfrak {p}}\right)} = \prod_ {\mathfrak {p}} \left| \alpha_ {\mathfrak {p}} \right| _ {\mathfrak {p}} ^ {- 1}. \] If \(x \in K^*\) is a principal idèle, then we find by chap. III, (1.3), that \(\mathfrak{N}(x) = \prod_{\mathfrak{p}} |x|_{\mathfrak{p}}^{-1} = 1\) . We thus have a continuous homomorphism \[ \mathfrak {N}: C _ {K} \longrightarrow \mathbb {R} _ {+} ^ {*}. \]

Definition / construction

FC09-C06-U010 · Chapter VI, §1, source L15432 · not formalized

Here the arrow \[ C _ {K} \longrightarrow P i c (\overline {{{\mathcal {O}}}}) \] is induced by the continuous surjective homomorphism \[ I _ {K} \longrightarrow J (\bar {\mathcal {O}}), \quad (\alpha_ {\mathfrak {p}}) \longmapsto \prod_ {\mathfrak {p}} \mathfrak {p} ^ {v _ {\mathfrak {p}} (\alpha_ {\mathfrak {p}})}, \] with kernel \[ I _ {K} ^ {0} = \left\{\left(\alpha_ {\mathfrak {p}}\right) \in I _ {K} \mid | \alpha_ {\mathfrak {p}} | _ {\mathfrak {p}} = 1 \text { for all } \mathfrak {p} \right\}. \]

Theorem (1.6)

FC09-C06-U011 · Chapter VI, §1, source L15452 · not formalized

(1.6) Theorem. The group \(C_K^0 = \{[\alpha] \in C_K \mid \mathfrak{N}([\alpha]) = 1\}\) is compact.

Convention / notation

FC09-C06-U012 · Chapter VI, §1, source L15466 · not formalized

The idèle class group \(C_K\) plays a similar rôle for the algebraic number field \(K\) as the multiplicative group \(K_{\mathfrak{p}}^*\) does for a \(\mathfrak{p}\) -adic number field \(K_{\mathfrak{p}}\) . It comes equipped with a collection of canonical subgroups which are to be viewed as analogues of the higher unit groups \(U_{\mathfrak{p}}^{(n)} = 1 + \mathfrak{p}^n\) of a \(\mathfrak{p}\) -adic number field \(K_{\mathfrak{p}}\) . Instead of \(\mathfrak{p}^n\) , we take any integral ideal \(\mathfrak{m} = \prod_{\mathfrak{p} \nmid \infty} \mathfrak{p}^{n_{\mathfrak{p}}}\) . We may also write it as a replete ideal \[ \mathfrak {m} = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {n _ {\mathfrak {p}}} \] with \(n_{\mathfrak{p}} = 0\) for \(\mathfrak{p}|\infty\) , and we treat it in what follows as a module of \(K\) . For every place \(\mathfrak{p}\) of \(K\) we put \(U_{\mathfrak{p}}^{(0)} = U_{\mathfrak{p}}\) , and \[ U _ {\mathfrak {p}} ^ {(n _ {\mathfrak {p}})} := \left\{ \begin{array}{l l} 1 + \mathfrak {p} ^ {n _ {\mathfrak {p}}}, & \text {if} \mathfrak {p} \nmid \infty , \\ \mathbb {R} _ {+} ^ {*} \subset K _ {\mathfrak {p}} ^ {*}, & \text {if} \mathfrak {p} \text {is real}, \\ \mathbb {C} ^ {*} = K _ {\mathfrak {p}} ^ {*}, & \text {if} \mathfrak {p} \text {is complex}, \end{array} \right. \] for \(n_{\mathfrak{p}} > 0\) . Given \(\alpha_{\mathfrak{p}} \in K_{\mathfrak{p}}^{*}\) we write \[ \alpha_ {\mathfrak {p}} \equiv 1 \bmod \mathfrak {p} ^ {n _ {\mathfrak {p}}} \iff \alpha_ {\mathfrak {p}} \in U _ {\mathfrak {p}} ^ {(n _ {\mathfrak {p}})}. \] For a finite prime p and \(n_{p} > 0\) this means the usual congruence; for a real place, it symbolizes positivity, and for a complex place it is the empty condition.

Definition (1.7)

FC09-C06-U013 · Chapter VI, §1, source L15486 · not formalized

(1.7) Definition. The group \[ C _ {K} ^ {\mathfrak {m}} = I _ {K} ^ {\mathfrak {m}} K ^ {*} / K ^ {*}, \] formed from the idèle group \[ I _ {K} ^ {\mathfrak {m}} = \prod_ {\mathfrak {p}} U _ {\mathfrak {p}} ^ {(n _ {\mathfrak {p}})}, \] is called the congruence subgroup mod m, and the quotient group \(C_{K}/C_{K}^{m}\) is called the ray class group mod m.

Proposition (1.8)

FC09-C06-U014 · Chapter VI, §1, source L15504 · not formalized

(1.8) Proposition. The closed subgroups of finite index of \(C_K\) are precisely those subgroups that contain a congruence subgroup \(C_K^m\) .

Definition / construction

FC09-C06-U015 · Chapter VI, §1, source L15522 · not formalized

The ray class groups can be given the following purely ideal-theoretic description. Let \(J_{K}^{m}\) be the group of all fractional ideals relatively prime to m, and let \(P_{K}^{m}\) be the group of all principal ideals ( \(a) \in P_{K}\) such that \[ a \equiv 1 \bmod {\mathfrak {m}} \quad \text { and } \quad a \text { totally positive. } \] The latter condition means that, for every real embedding \(K \to \mathbb{R}\) , \(a\) turns out to be positive. The congruence \(a \equiv 1 \mod \mathfrak{m}\) means that \(a\) is the quotient \(b/c\) of two integers relatively prime to \(\mathfrak{m}\) such that \(b \equiv c \mod \mathfrak{m}\) . This is tantamount to saying that \(a \equiv 1 \mod \mathfrak{p}^{n_{\mathfrak{p}}}\) in \(K_{\mathfrak{p}}\) , i.e., \(a \in U_{\mathfrak{p}}^{(n_{\mathfrak{p}})}\) for all \(\mathfrak{p}|\mathfrak{m} = \prod_{\mathfrak{p} \nmid \infty} \mathfrak{p}^{n_{\mathfrak{p}}}\) . We put \[ C l _ {K} ^ {\mathfrak {m}} = J _ {K} ^ {\mathfrak {m}} / P _ {K} ^ {\mathfrak {m}}. \]

Proposition (1.9)

FC09-C06-U016 · Chapter VI, §1, source L15536 · not formalized

(1.9) Proposition. The homomorphism \[ (\quad): I _ {K} \longrightarrow J _ {K}, \quad \alpha \longmapsto (\alpha) = \prod_ {\mathfrak {p} \nmid \infty} \mathfrak {p} ^ {v _ {\mathfrak {p}} (\alpha_ {\mathfrak {p}})}, \] induces an isomorphism \[ C _ {K} / C _ {K} ^ {\mathfrak {m}} \cong C l _ {K} ^ {\mathfrak {m}}. \]

Proposition (1.10)

FC09-C06-U017 · Chapter VI, §1, source L15564 · not formalized

(1.10) Proposition. For any module \(\mathfrak{m} = (m)\) of the field \(\mathbb{Q}\) , one has \[ C _ {\mathbb {Q}} / C _ {\mathbb {Q}} ^ {\mathfrak {m}} \cong C l _ {\mathbb {Q}} ^ {\mathfrak {m}} \cong (\mathbb {Z} / m \mathbb {Z}) ^ {*}. \]

Proposition (1.11)

FC09-C06-U018 · Chapter VI, §1, source L15586 · not formalized

(1.11) Proposition. There is an exact sequence \[ 1 \longrightarrow \mathcal {O} ^ {*} / \mathcal {O} _ {+} ^ {*} \longrightarrow \prod_ {\mathfrak {p} \text { real }} \mathbb {R} ^ {*} / \mathbb {R} _ {+} ^ {*} \longrightarrow C l _ {K} ^ {1} \longrightarrow C l _ {K} \longrightarrow 1, \] where \(\mathcal{O}_+^*\) is the group of totally positive units of \(K\) .

Definition / construction

FC09-C06-U019 · Chapter VI, §2, source L15717 · not formalized

For an idèle \(\alpha \in I_L\) , we then define \(\sigma \alpha \in I_L\) to be the idèle with components \[ (\sigma \alpha) _ {\sigma \mathfrak {P}} = \sigma \alpha_ {\mathfrak {P}} \in (\sigma L) _ {\sigma \mathfrak {P}}. \] If \(L|K\) is a Galois extension with Galois group \(G = G(L|K)\) , then every \(\sigma \in G\) yields an automorphism \(\sigma : I_L \to I_L\) , i.e., \(I_L\) is turned into an \(G\) -module. As to the fixed module \(I_L^G = \{\alpha \in I_L \mid \sigma \alpha = \alpha \text{ for all } \sigma \in G\}\) , we have the proposition (2.1): if \(L|K\) is Galois with group \(G\), then \(I_{L}^{G} = I_{K}\).

Not formalized. The project defines idèles and idèle classes, but no checked Galois action, global idèle norm, class-group extension map, or fixed-point theorem closes this source bundle. Field norms/local completions alone do not earn an idèlic norm/fixed-class statement.

Proposition (2.1)

FC09-C06-U020 · Chapter VI, §2, source L15725 · not formalized

(2.1) Proposition. If \(L|K\) is a Galois extension with Galois group \(G\) , then \[ I _ {L} ^ {G} = I _ {K}. \]

Definition / construction

FC09-C06-U021 · Chapter VI, §2, source L15777 · not formalized

Every \(\alpha_{\mathfrak{p}} \in L_{\mathfrak{p}}^{*}\) defines an automorphism \[ \alpha_ {\mathfrak {p}}: L _ {\mathfrak {p}} \longrightarrow L _ {\mathfrak {p}}, \quad x \longmapsto \alpha_ {\mathfrak {p}} x, \] of the \(K_{\mathfrak{p}}\) -vector space \(L_{\mathfrak{p}}\) , and as in the case of a field extension, we define the norm of \(\alpha_{\mathfrak{p}}\) by \[ N _ {L _ {\mathfrak {p}} | K _ {\mathfrak {p}}} (\alpha_ {\mathfrak {p}}) = \det (\alpha_ {\mathfrak {p}}). \] In this way we obtain a homomorphism \[ N _ {L _ {\mathfrak {p}} | K _ {\mathfrak {p}}}: L _ {\mathfrak {p}} ^ {*} \longrightarrow K _ {\mathfrak {p}} ^ {*}. \] It induces a norm homomorphism \[ N _ {L | K}: I _ {L} \longrightarrow I _ {K} \] between the idèle groups \(I_{L} = \prod_{p} L_{p}^{*}\) and \(I_{K} = \prod_{p} K_{p}^{*}\) . Explicitly the norm of an idèle is given by the following proposition.

Proposition (2.2)

FC09-C06-U022 · Chapter VI, §2, source L15803 · not formalized

(2.2) Proposition. If \(L|K\) is a finite extension and \(\alpha = (\alpha_{\mathfrak{P}}) \in I_L\) , the local components of the idèle \(N_{L|K}(\alpha)\) are given by \[ N _ {L | K} (\alpha) _ {\mathfrak {p}} = \prod_ {\mathfrak {P} | \mathfrak {p}} N _ {L _ {\mathfrak {P}} | K _ {\mathfrak {p}}} (\alpha_ {\mathfrak {P}}). \]

Proposition (2.3)

FC09-C06-U023 · Chapter VI, §2, source L15817 · not formalized

(2.3) Proposition. (i) For a tower of fields \(K \subseteq L \subseteq M\) we have \(N_{M|K} = N_{L|K} \circ N_{M|L}\) . (ii) If \(L|K\) is embedded into the Galois extension \(M|K\) and if \(G = G(M|K)\) and \(H = G(M|L)\) , then one has for \(\alpha \in I_L: N_{L|K}(\alpha) = \prod_{\sigma \in G / H} \sigma \alpha\) . (iii) \(N_{L|K}(\alpha) = \alpha^{[L:K]}\) for \(\alpha \in I_K\) . (iv) The norm of the principal idèle \(x \in L^*\) is the principal idèle of \(K\) defined by the usual norm \(N_{L|K}(x)\) .

Proposition (2.4)

FC09-C06-U024 · Chapter VI, §2, source L15857 · not formalized

(2.4) Proposition. If \(L|K\) is a finite extension, then the homomorphism \(I_K \to I_L\) induces an injection of idèle class groups \[ C _ {K} \longrightarrow C _ {L}, \quad \alpha K ^ {*} \longmapsto \alpha L ^ {*}. \]

Proposition (2.5)

FC09-C06-U025 · Chapter VI, §2, source L15871 · not formalized

(2.5) Proposition. If \(L|K\) is a Galois extension and \(G = G(L|K)\) , then \(C_L\) is canonically a \(G\) -module and \(C_L^G = C_K\) .

Definition / construction

FC09-C06-U026 · Chapter VI, §3, source L15947 · not formalized

Let \(L|K\) be a finite Galois extension with Galois group G. The G-module \(I_{L}\) may be described in the following simple manner, which immediately reduces us to local fields. For every place p of K we put \[ L _ {\mathfrak {p}} ^ {*} = \prod_ {\mathfrak {P} | \mathfrak {p}} L _ {\mathfrak {P}} ^ {*} \quad \text { and } \quad U _ {L, \mathfrak {p}} = \prod_ {\mathfrak {P} | \mathfrak {p}} U _ {\mathfrak {P}}. \] Since the automorphisms \(\sigma \in G\) permute the places of \(L\) above \(\mathfrak{p}\) , the groups \(L_{\mathfrak{p}}^{*}\) and \(U_{L,\mathfrak{p}}\) are \(G\) -modules, and we have for the \(G\) -module \(I_L\) the decomposition \[ I _ {L} = \prod_ {\mathfrak {p}} L _ {\mathfrak {p}} ^ {*}, \] where the restricted product is taken with respect to the subgroups \(U_{L,p} \subseteq L_{p}^{*}\) . Choose a place P of L above p, and let \(G_{\mathfrak{P}} = G(L_{\mathfrak{P}} | K_{\mathfrak{p}}) \subseteq G\) be its decomposition group. As \(\sigma\) varies over a system of representatives of \(G / G_{P}\) , \(\sigma P\) runs through the various places of L above p, and we get \[ L _ {\mathfrak {p}} ^ {*} = \prod_ {\sigma} L _ {\sigma \mathfrak {P}} ^ {*} = \prod_ {\sigma} \sigma (L _ {\mathfrak {P}} ^ {*}), U _ {L, \mathfrak {p}} = \prod_ {\sigma} U _ {\sigma \mathfrak {P}} = \prod_ {\sigma} \sigma (U _ {\mathfrak {P}}). \]

Not formalized. Pinned/current Mathlib and the Clay CFT code provide generic induced/coinduced representation and Tate/Herbrand infrastructure, but no proved global idèle/S-unit G-module decomposition or global class-field axiom. The source row therefore remains without a compatible theorem-level owner.

Proposition (3.1)

FC09-C06-U027 · Chapter VI, §3, source L15967 · not formalized

(3.1) Proposition. \(L_{\mathfrak{p}}^{*}\) and \(U_{L,\mathfrak{p}}\) are the induced \(G\) -modules \[ L _ {\mathfrak {p}} ^ {*} = \operatorname{Ind} _ {G} ^ {G _ {\mathfrak {P}}} (L _ {\mathfrak {P}} ^ {*}), \quad U _ {L, \mathfrak {p}} = \operatorname{Ind} _ {G} ^ {G _ {\mathfrak {P}}} (U _ {\mathfrak {P}}). \]

Definition / construction

FC09-C06-U028 · Chapter VI, §3, source L15973 · not formalized

Now let S be a finite set of places of K containing the infinite places. We then define \(I_{L}^{S} = I_{L}^{\overline{S}}\) , where \(\overline{S}\) denotes the set of all places of L which lie above the places of S. For \(I_{L}^{S}\) we have the G-module decomposition \[ I _ {L} ^ {S} = \prod_ {\mathfrak {p} \in S} L _ {\mathfrak {p}} ^ {*} \times \prod_ {\mathfrak {p} \not \in S} U _ {L, \mathfrak {p}}, \]

Proposition (3.2)

FC09-C06-U029 · Chapter VI, §3, source L15981 · not formalized

(3.2) Proposition. If \(L|K\) is a cyclic extension, and if \(S\) contains all primes ramified in \(L\) , then we have for \(i = 0, -1\) that \[ H ^ {i} (G, I _ {L} ^ {S}) \cong \bigoplus_ {\mathfrak {p} \in S} H ^ {i} (G _ {\mathfrak {P}}, L _ {\mathfrak {P}} ^ {*}) \quad a n d \quad H ^ {i} (G, I _ {L}) \cong \bigoplus_ {\mathfrak {p}} H ^ {i} (G _ {\mathfrak {P}}, L _ {\mathfrak {P}} ^ {*}), \] where for each p, P is a chosen prime of L above p.

Proposition (3.3)

FC09-C06-U030 · Chapter VI, §3, source L16013 · not formalized

(3.3) Proposition. If \(L|K\) is a cyclic extension and if \(S\) contains all ramified primes, then \[ h (G, I _ {L} ^ {S}) = \prod_ {\mathfrak {p} \in S} n _ {\mathfrak {p}}, \] where \(n_{\mathfrak{p}} = [L_{\mathfrak{P}}:K_{\mathfrak{p}}]\) .

Lemma (3.4)

FC09-C06-U031 · Chapter VI, §3, source L16035 · not formalized

(3.4) Lemma. Let V be an s-dimensional R-vector space, and let G be a finite group of automorphisms of V which operates as a permutation group on the elements of a basis \(v_{1}, \ldots, v_{s}\) : \(\sigma v_{i} = v_{\sigma(i)}\) . If \(\Gamma\) is a \(G\) -invariant complete lattice in \(V\) , i.e., \(\sigma \Gamma \subseteq \Gamma\) for all \(\sigma\) , then there exists a complete sublattice in \(\Gamma\) , \[ \Gamma^ {\prime} = \mathbb {Z} w _ {1} + \dots + \mathbb {Z} w _ {s}, \] such that \(\sigma w_{i} = w_{\sigma (i)}\) for all \(\sigma \in G\) .

Convention / notation

FC09-C06-U032 · Chapter VI, §3, source L16101 · not formalized

Now let L|K be a cyclic extension of degree n with Galois group \(G = G(L|K)\) , let S be a finite set of places containing the infinite places, and let \(\bar{S}\) be the set of places of L that lie above the places of S. We denote the group \(L^{\bar{S}}\) of \(\bar{S}\) -units simply by \(L^{S}\) .

Proposition (3.5)

FC09-C06-U033 · Chapter VI, §3, source L16103 · not formalized

(3.5) Proposition. The Herbrand quotient of the \(G\) -module \(L^S\) satisfies \[ h (G, L ^ {S}) = \frac {1}{n} \prod_ {\mathfrak {p} \in S} n _ {\mathfrak {p}}, \] where \(n_{\mathfrak{p}} = [L_{\mathfrak{P}}:K_{\mathfrak{p}}]\) .

Theorem (3.6)

FC09-C06-U034 · Chapter VI, §3, source L16175 · not formalized

(3.6) Theorem. If \(L|K\) is a cyclic extension of degree \(n\) with Galois group \(G = G(L|K)\) , then \[ h (G, C _ {L}) = \frac {\# H ^ {0} (G , C _ {L})}{\# H ^ {- 1} (G , C _ {L})} = n. \] In particular \((C_K:N_{L|K}C_L)\geq n\)

Corollary (3.7)

FC09-C06-U035 · Chapter VI, §3, source L16185 · not formalized

(3.7) Corollary. If \(L|K\) is cyclic of prime power degree \(n = p^{\nu} (\nu > 0)\) , then there are infinitely many places of \(K\) which do not split in \(L\) .

Corollary (3.8)

FC09-C06-U036 · Chapter VI, §3, source L16197 · not formalized

(3.8) Corollary. Let \(L|K\) be a finite extension of algebraic number fields. If almost all primes of \(K\) split completely in \(L\) , then \(L = K\) .

Proposition (4.1)

FC09-C06-U037 · Chapter VI, §4, source L16223 · not formalized

(4.1) Proposition. One has \(s \geq r\) , and there exists a set \(T\) of \(s - r\) primes of \(K\) that do not belong to \(S\) such that \[ L = K (\sqrt [ n ]{\Delta}), \] where \(\Delta\) is the kernel of the map \(K^S \to \prod_{\mathfrak{p} \in T} K_{\mathfrak{p}}^* / K_{\mathfrak{p}}^{*n}\) .

Theorem (4.2)

FC09-C06-U038 · Chapter VI, §4, source L16251 · after FC09-C06-U037 · not formalized

(4.2) Theorem. Let \(T\) be a set of places as in (4.1), and let \[ C _ {K} (S, T) = I _ {K} (S, T) K ^ {*} / K ^ {*}, \] where \[ I _ {K} (S, T) = \prod_ {\mathfrak {p} \in S} K _ {\mathfrak {p}} ^ {* n} \times \prod_ {\mathfrak {p} \in T} K _ {\mathfrak {p}} ^ {*} \times \prod_ {\mathfrak {p} \not \in S \cup T} U _ {\mathfrak {p}}. \] Then one has \[ N _ {L | K} C _ {L} \supseteq C _ {K} (S, T) \quad \text { and } \quad \left(C _ {K}: C _ {K} (S, T)\right) = [ L: K ]. \] In particular, if \(L|K\) is cyclic, then \(N_{L|K}C_L = C_K(S,T)\) .

Lemma (4.3)

FC09-C06-U039 · Chapter VI, §4, source L16275 · not formalized

(4.3) Lemma. \(I_K(S, T) \cap K^* = (K^{S \cup T})^n\) .

Theorem (4.4)

FC09-C06-U040 · Chapter VI, §4, source L16333 · not formalized

(4.4) Theorem (Global Class Field Axiom). If \(L|K\) is a cyclic extension of algebraic number fields, then \[ \# H ^ {i} \big (G (L | K), C _ {L} \big) = \left\{ \begin{array}{l l} [ L: K ] & \text {for i = 0 ,} \\ 1 & \text {for i = -1 .} \end{array} \right. \]

Corollary (4.5)

FC09-C06-U041 · Chapter VI, §4, source L16371 · not formalized

(4.5) Corollary. Let \(L|K\) be a cyclic extension. An element \(x \in K^*\) is a norm if and only if it is a norm locally everywhere, i.e., a norm in every completion \(L_{\mathfrak{P}}|K_{\mathfrak{p}}(\mathfrak{P}|\mathfrak{p})\) .

Proposition (5.1)

FC09-C06-U042 · Chapter VI, §5, source L16431 · not formalized

(5.1) Proposition. Let \(\Omega|\mathbb{Q}\) be the field obtained by adjoining all roots of unity, and let \(T\) be the torsion subgroup of \(G(\Omega|K)\) (i.e., the group of all elements of finite order). Then the fixed field \(\widetilde{\mathbb{Q}}|\mathbb{Q}\) of \(T\) is a \(\widehat{\mathbb{Z}}\) -extension.

Not formalized. This row is part of the global reciprocity construction: cyclotomic Z-hat extensions, products of local norm-residue symbols, the global idèle-class valuation, global norm-residue isomorphism, or local-global compatibility. No checked project/pinned/current/open/external Lean source supplies the complete bundle.

Convention / notation

FC09-C06-U043 · Chapter VI, §5, source L16461 · not formalized

We fix an isomorphism \(G(\widetilde{\mathbb{Q}}|\mathbb{Q}) \cong \widehat{\mathbb{Z}}\) . There is no canonical choice as in the case of local fields. However, the reciprocity law will not depend on the choice. Via \(G(\widetilde{\mathbb{Q}}|\mathbb{Q}) \cong \widehat{\mathbb{Z}}\) , we obtain a continuous surjective homomorphism \[ d: G _ {\mathbb {Q}} \longrightarrow \widehat {\mathbb {Z}} \] of the absolute Galois group \(G_{\mathbb{Q}} = G(\overline{\mathbb{Q}}|\mathbb{Q})\) . With this we continue as in chap. IV, §4, choosing \(k = \mathbb{Q}\) as our base field. If \(K|\mathbb{Q}\) is a finite extension, then we put \(f_K = [K \cap \widetilde{\mathbb{Q}} : \mathbb{Q}]\) and get a surjective homomorphism \[ d _ {K} = \frac {1}{f _ {K}} d: G _ {K} \longrightarrow \widehat {\mathbb {Z}}, \] which defines the \(\widehat{Z}\) -extension \(\widetilde{K}=K\widetilde{Q}\) of K. \(\widetilde{K}|K\) is called the cyclotomic \(\widehat{Z}\) -extension of K. We denote again by \(\varphi_{K}\) the element of \(G(\widetilde{K}|K)\) which is mapped to 1 by the isomorphism \(G(\widetilde{K}|K) \cong \widehat{\mathbb{Z}}\) , and by \(\varphi_{L|K}\) the restriction \(\varphi_K|_L\) if \(L|K\) is a subextension of \(\widetilde{K}|K\) . The automorphism \(\varphi_{L|K}\) must not be confused with the Frobenius automorphism corresponding to a prime ideal of \(L\) (see §7).

Definition / construction

FC09-C06-U044 · Chapter VI, §5, source L16483 · not formalized

For an arbitrary finite abelian extension \(L|K\) , we define the homomorphism \[ [ \mathrm{,} L | K ]: I _ {K} \longrightarrow G (L | K) \] by \[ [ \alpha , L | K ] = \prod_ {\mathfrak {p}} (\alpha_ {\mathfrak {p}}, L _ {\mathfrak {p}} | K _ {\mathfrak {p}}), \] where \(L_{p}\) denotes the completion of L with respect to a place \(P|p\) , and \((\alpha_{p}, L_{p}|K_{p})\) is the norm residue symbol of local class field theory. Note that almost all factors in the product are 1 because almost all extensions \(L_{p}|K_{p}\) are unramified and almost all \(\alpha_{p}\) are units.

Proposition (5.2)

FC09-C06-U045 · Chapter VI, §5, source L16497 · not formalized

(5.2) Proposition. If \(L|K\) and \(L'|K'\) are two abelian extensions of finite algebraic number fields such that \(K \subseteq K'\) and \(L \subseteq L'\) , then we have the commutative diagram \[ \begin{array}{c} I _ {K ^ {\prime}} \xrightarrow {[ , L ^ {\prime} | K ^ {\prime} ]} G (L ^ {\prime} | K ^ {\prime}) \\ N _ {K ^ {\prime} | K} \Big \downarrow \qquad \qquad \qquad \qquad \Big \downarrow \\ I _ {K} \xrightarrow {[ , L | K ]} G (L | K). \end{array} \]

Definition / construction

FC09-C06-U046 · Chapter VI, §5, source L16515 · after FC09-C06-U045 · not formalized

If \(L|K\) is an abelian extension of infinite degree, then we define the homomorphism \[ [ \quad , L | K ]: I _ {K} \longrightarrow G (L | K) \] by its restrictions \([, L|K]_{L'} := [, L'|K]\) to the finite subextensions \(L'\) of \(L|K\) . In other words, if \(\alpha \in I_K\) , then the elements \([\alpha, L'|K]\) define, by (5.2), an element of the projective limit \(\varprojlim_{L'} G(L'|K)\) , and \([\alpha, L|K]\) is precisely this element, once we identify \(G(L|K) = \varprojlim G(L'|K)\) . Again one has the equation \[ [ \alpha , L | K ] = \prod_ {\mathfrak {p}} (\alpha_ {\mathfrak {p}}, L _ {\mathfrak {p}} | K _ {\mathfrak {p}}), \] where \(L_{\mathfrak{p}}\) does not denote the completion of \(L\) with respect to a place above \(\mathfrak{p}\) , but rather the localization, i.e., the union of the completions \(L_{\mathfrak{p}}^{\prime}|K_{\mathfrak{p}}\) of all finite subextensions (see chap. II, §8). Then \(L_{\mathfrak{p}}|K_{\mathfrak{p}}\) is Galois, \(G(L_{\mathfrak{p}}|K_{\mathfrak{p}}) \subseteq G(L|K)\) , and the product \(\prod_{\mathfrak{p}}(\alpha_{\mathfrak{p}}, L_{\mathfrak{p}}|K_{\mathfrak{p}})\) converges in the profinite group to the element \([\alpha, L|K]\) . Indeed, if \(L^{\prime}|K\) varies over the finite subextensions of \(L|K\) , then the sets \(S_{L^{\prime}} = \{\mathfrak{p} | (\alpha_{\mathfrak{p}}, L_{\mathfrak{p}}^{\prime}|K_{\mathfrak{p}}) \neq 1\}\) are all finite, so that we may write down the finite products \[ \sigma_{L'} = \prod_{\mathfrak{p} \in S_{L'}} (\alpha_{\mathfrak{p}}, L_{\mathfrak{p}}|K_{\mathfrak{p}}) \in G(L|K), \] which converge to the global norm residue symbol.

Proposition (5.3)

FC09-C06-U047 · Chapter VI, §5, source L16551 · not formalized

(5.3) Proposition. For every root of unity \(\zeta\) and every principal idèle \(a \in K^{*}\) one has \[ [ a, K (\zeta) | K ] = 1. \]

Definition / construction

FC09-C06-U048 · Chapter VI, §5, source L16579 · not formalized

The homomorphism \([ \quad, \widetilde{K} | K] : I_K \to G(\widetilde{K} | K)\) therefore induces a homomorphism \[ [ \quad , \widetilde {K} | K ]: C _ {K} \longrightarrow G (\widetilde {K} | K), \] and we consider its composite \[ v _ {K}: C _ {K} \longrightarrow \widehat {\mathbb {Z}} \] with \(d_K: G(\widetilde{K}|K) \to \widehat{\mathbb{Z}}\) . The pair \((d_K, v_K)\) is then a class field theory, for we have the proposition (5.4): the map \(v_{K} \colon C_{K} \to \widehat{\mathbb{Z}}\) is surjective and is a henselian valuation with respect to \(d_{K}\).

Proposition (5.4)

FC09-C06-U049 · Chapter VI, §5, source L16593 · not formalized

(5.4) Proposition. The map \(v_{K}: C_{K} \to \widehat{\mathbb{Z}}\) is surjective and is a henselian valuation with respect to \(d_{K}\) .

Theorem (5.5)

FC09-C06-U050 · Chapter VI, §5, source L16631 · not formalized

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

Definition / construction

FC09-C06-U051 · Chapter VI, §5, source L16637 · not formalized

The inverse map of \(r_{L|K}\) yields a surjective homomorphism \[ (\quad , L | K): C _ {K} \rightarrow G (L | K) ^ {a b} \] with kernel \(N_{L|K}C_{L}\) . The map \((,L|K)\) is called the global norm residue symbol. We view it also as a homomorphism \(I_{K} \to G(L|K)^{ab}\) .

Definition / construction

FC09-C06-U052 · Chapter VI, §5, source L16645 · not formalized

For every place \(\mathfrak{p}\) of \(K\) , we have on the one hand the embedding \(G(L_{\mathfrak{p}}|K_{\mathfrak{p}}) \hookrightarrow G(L|K)\) , and on the other the canonical injection \[ \langle \quad \rangle : K _ {\mathfrak {p}} ^ {*} \rightarrow C _ {K}, \] which sends \(a_{\mathfrak{p}} \in K_{\mathfrak{p}}^{*}\) to the class of the idèle \[ \langle a _ {\mathfrak {p}} \rangle = (\dots , 1, 1, 1, a _ {\mathfrak {p}}, 1, 1, 1, \dots). \]

Proposition (5.6)

FC09-C06-U053 · Chapter VI, §5, source L16659 · not formalized

(5.6) Proposition. If \(L|K\) is an abelian extension and \(\mathfrak{p}\) is a place of \(K\) , then the diagram \[ \begin{array}{c} K _ {\mathfrak {p}} ^ {*} \xrightarrow {(\quad , L _ {\mathfrak {p}} | K _ {\mathfrak {p}})} G (L _ {\mathfrak {p}} | K _ {\mathfrak {p}}) \\ \langle \quad \rangle \Biggl \downarrow \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \Biggl \downarrow \\ C _ {K} \xrightarrow {(\quad , L | K)} G (L | K) \end{array} \] is commutative.

Corollary (5.7)

FC09-C06-U054 · Chapter VI, §5, source L16711 · not formalized

(5.7) Corollary. If \(L|K\) is an abelian extension and \(\alpha = (\alpha_{\mathfrak{p}}) \in I_K\) , then \[ (\alpha , L | K) = \prod_ {\mathfrak {p}} (\alpha_ {\mathfrak {p}}, L _ {\mathfrak {p}} | K _ {\mathfrak {p}}). \] In particular, for a principal idèle \(a \in K^{*}\) we have the product formula \[ \prod_ {\mathfrak {p}} (a, L _ {\mathfrak {p}} | K _ {\mathfrak {p}}) = 1. \]

Corollary (5.8)

FC09-C06-U055 · Chapter VI, §5, source L16733 · not formalized

(5.8) Corollary. For every finite abelian extension one has \[ N C _ {L} \cap K _ {\mathfrak {p}} ^ {*} = N _ {\mathfrak {p}} L _ {\mathfrak {p}} ^ {*}. \]

Theorem (6.1)

FC09-C06-U056 · Chapter VI, §6, source L16779 · not formalized

(6.1) Theorem. The map \[ L \longmapsto \mathcal {N} _ {L} = N _ {L | K} C _ {L} \] is a 1-1-correspondence between the finite abelian extensions \(L|K\) and the closed subgroups of finite index in \(C_K\) . Moreover one has: \[ 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}}. \] The field \(L|K\) corresponding to the subgroup \(\mathcal{N}\) of \(C_K\) is called the class field of \(\mathcal{N}\) . It satisfies \[ G (L | K) \cong C _ {K} / \mathcal {N}. \]

Not formalized. This row depends on the global existence theorem, ray class fields/conductors, Hilbert class fields, or explicit complex multiplication. Current/open experimental Hilbert-class-field files contain only wanted/sorried statements, so no source-complete route is credited.

Definition / construction

FC09-C06-U057 · Chapter VI, §6, source L16829 · after FC09-C06-U013, FC09-C06-U014 · not formalized

The above theorem is called the “existence theorem” of global class field theory because its main assertion is the existence, for any given closed subgroup N of finite index in \(C_{K}\) , of an abelian extension \(L|K\) such that \(N_{L|K}C_{L} = N\) . This extension L is the class field for N. The existence theorem gives a clear overview of all the abelian extensions of K once we bring in the congruence subgroups \(C_{K}^{m}\) of \(C_{K}\) corresponding to the modules \(m = \prod_{p \nmid \infty} p^{n_{p}}\) (see (1.7)). They are closed of finite index by (1.8), and they prompt the following definition.

Definition (6.2)

FC09-C06-U058 · Chapter VI, §6, source L16831 · not formalized

(6.2) Definition. The class field \(K^{m}|K\) for the congruence subgroup \(C_{K}^{m}\) is called the ray class field mod m.

Corollary (6.3)

FC09-C06-U059 · Chapter VI, §6, source L16847 · not formalized

(6.3) Corollary. Every finite abelian extension \(L|K\) is contained in a ray class field \(K^{\mathfrak{m}}|K\) .

Definition (6.4)

FC09-C06-U060 · Chapter VI, §6, source L16849 · not formalized

(6.4) Definition. Let \(L|K\) be a finite abelian extension, and let \(\mathcal{N}_L = N_{L|K}C_L\) . The conductor \(\mathfrak{f}\) of \(L|K\) (or of \(\mathcal{N}_L\) ) is the gcd of all modules \(\mathfrak{m}\) such that \(L \subseteq K^{\mathfrak{m}}\) (i.e., \(C_K^{\mathfrak{m}} \subseteq \mathcal{N}_L\) ).

Definition / construction

FC09-C06-U061 · Chapter VI, §6, source L16851 · after FC09-C05-U009, FC09-C06-U011 · not formalized

\(K^{\mathfrak{f}}|K\) is therefore the smallest ray class field containing \(L|K\) . But it is not true in general that \(\mathfrak{m}\) is the conductor of \(K^{\mathfrak{m}}|K\) . In chap. V, (1.6), we defined the conductor \(\mathfrak{f}_{\mathfrak{p}}\) of a \(\mathfrak{p}\) -adic extension \(L_{\mathfrak{p}}|K_{\mathfrak{p}}\) for a finite place \(\mathfrak{p}\) , to be the smallest power \(\mathfrak{f}_{\mathfrak{p}} = \mathfrak{p}^{n}\) such that \(U_{K}^{(n)} \subseteq N_{L_{\mathfrak{p}}|K_{\mathfrak{p}}} L_{\mathfrak{p}}^{*}\) . For an infinite place \(\mathfrak{p}\) we define \(\mathfrak{f}_{\mathfrak{p}} = 1\) . Then we view \(\mathfrak{f}\) as the replete ideal \(\mathfrak{f} \prod_{\mathfrak{p}|\infty} \mathfrak{p}^{0}\) and obtain the conductor formula of proposition (6.5), relating the conductor \(\mathfrak{f}\) of an abelian extension \(L|K\) to the conductors \(\mathfrak{f}_{\mathfrak{p}}\) of the local extensions \(L_{\mathfrak{p}}|K_{\mathfrak{p}}\).

Proposition (6.5)

FC09-C06-U062 · Chapter VI, §6, source L16853 · not formalized

(6.5) Proposition. If \(\mathfrak{f}\) is the conductor of the abelian extension \(L|K\) , and \(\mathfrak{f}_{\mathfrak{p}}\) is the conductor of the local extension \(L_{\mathfrak{p}}|K_{\mathfrak{p}}\) , then \[ f = \prod_ {p} f _ {p}. \]

Corollary (6.6)

FC09-C06-U063 · Chapter VI, §6, source L16879 · not formalized

(6.6) Corollary. Let \(L|K\) be a finite abelian extension and \(f\) its conductor. Then: \[ \mathfrak {p} \text { is ramified in } L \iff \mathfrak {p} | \mathfrak {f}. \]

Proposition (6.7)

FC09-C06-U064 · Chapter VI, §6, source L16887 · not formalized

(6.7) Proposition. Let \(m\) be a natural number and \(\mathfrak{m} = (m)\) . Then the ray class field mod \(\mathfrak{m}\) of \(\mathbb{Q}\) is the field \[ \mathbb {Q} ^ {\mathfrak {m}} = \mathbb {Q} (\mu_ {m}) \] of \(m\) -th roots of unity.

Definition / construction

FC09-C06-U065 · Chapter VI, §6, source L16907 · after FC09-C06-U018, FC09-C06-U063 · not formalized

Among all abelian extensions of K, the ray class field mod 1 occupies a special place. It is called the big Hilbert class field and has Galois group \[ G (K ^ {1} | K) \cong C l _ {K} ^ {1}. \] By (1.11), the group \(Cl_K^1\) is linked to the ordinary ideal class group by the exact sequence \[ 1 \longrightarrow \mathcal {O} ^ {*} / \mathcal {O} _ {+} ^ {*} \longrightarrow \prod_ {\mathfrak {p} \text { real }} \mathbb {R} ^ {*} / \mathbb {R} _ {+} ^ {*} \longrightarrow C l _ {K} ^ {1} \longrightarrow C l _ {K} \longrightarrow 1. \] The big Hilbert class field has conductor f = 1 and may therefore be characterized by (6.6) in the following way.

Proposition (6.8)

FC09-C06-U066 · Chapter VI, §6, source L16921 · not formalized

(6.8) Proposition. The big Hilbert class field is the maximal unramified abelian extension of K.

Definition / construction

FC09-C06-U067 · Chapter VI, §6, source L16923 · not formalized

Since the infinite places are always unramified, this means that all prime ideals are unramified. The Hilbert class field, or more precisely, the “small Hilbert class field”, is defined to be the maximal unramified abelian extension \(H|K\) in which all infinite places split completely, i.e., the real places stay real. It satisfies the proposition (6.9): the Galois group of the small Hilbert class field is canonically isomorphic to the ideal class group, \(G(H|K) \cong Cl_{K}\), so \([H:K] = h_{K}\).

Proposition (6.9)

FC09-C06-U068 · Chapter VI, §6, source L16925 · not formalized

(6.9) Proposition. The Galois group of the small Hilbert class field \(H|K\) is canonically isomorphic to the ideal class group: \[ G (H | K) \cong C l _ {K}. \] In particular, the degree \([H : K]\) is the class number \(h_{K}\) of K.

Definition / construction

FC09-C06-U069 · Chapter VI, §6, source L16951 · after FC09-C03-U111, FC09-C06-U063 · not formalized

Remark: The small Hilbert class field is in general not a ray class field in terms of the theory developed here. But it is in many other textbooks where ray class groups and ray class fields are defined differently (see for instance [107]). This other theory is obtained by equipping all number fields with the Minkowski metric \[ \langle x, y \rangle_ {K} = \sum_ {\tau} \alpha_ {\tau} x _ {\tau} \overline {{{{y}}}} _ {\tau} \quad \left(\tau \in \operatorname{Hom} (K, \mathbb {C})\right), \] \(\alpha_{\tau} = 1\) if \(\tau = \overline{\tau}\) , \(\alpha_{\tau} = \frac{1}{2}\) if \(\tau \neq \overline{\tau}\) . A ray class group can then be attached to any replete module \[ \mathfrak {m} = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {n _ {\mathfrak {p}}}, \] where \(n_{\mathfrak{p}} \in \mathbb{Z}\) , \(n_{\mathfrak{p}} \geq 0\) , and \(n_{\mathfrak{p}} = 0\) or \(= 1\) if \(\mathfrak{p} | \infty\) . The groups \(U_{\mathfrak{p}}^{(n_{\mathfrak{p}})}\) attached to the metrized number field \((K, \langle , \rangle_K)\) are defined by \[ U _ {\mathfrak {p}} ^ {(n _ {\mathfrak {p}})} = \left\{ \begin{array}{l l} 1 + \mathfrak {p} ^ {n _ {\mathfrak {p}}}, & \text { for } n _ {\mathfrak {p}} > 0, \text { and } U _ {\mathfrak {p}} \text { for } n _ {\mathfrak {p}} = 0, \text { if } \mathfrak {p} \nmid \infty , \\ \mathbb {R} ^ {*}, & \text { if } \mathfrak {p} \text { is real and } n _ {\mathfrak {p}} = 0, \\ \mathbb {R} _ {+} ^ {*}, & \text { if } \mathfrak {p} \text { is real and } n _ {\mathfrak {p}} = 1, \\ \mathbb {C} ^ {*} = K _ {\mathfrak {p}} ^ {*}, & \text { if } \mathfrak {p} \text { is complex. } \end{array} \right. \] The congruence subgroup mod \(\mathfrak{m}\) of \((K, \langle , \rangle_K)\) is then the subgroup \(C_K^{\mathfrak{m}} = I_K^{\mathfrak{m}}K^* / K^*\) of \(C_K\) formed with the group \[ I _ {K} ^ {\mathfrak {m}} = \prod_ {\mathfrak {p}} U _ {\mathfrak {p}} ^ {(n _ {\mathfrak {p}})}, \] and the factor group \(C_K / C_K^m\) is the ray class group mod m. The ray class field mod m of \((K, \langle , \rangle_K)\) is again the class field of \(K\) corresponding to the group \(C_K^m \subseteq C_K\) . As explained in chap. III, §3, the infinite places p have to be considered as ramified in an extension \(L|K\) if \(L_{\mathfrak{p}} \neq K_{\mathfrak{p}}\) . Likewise, the conductor of an abelian extension \(L|K\) , i.e., the gcd of all modules \(\mathfrak{m} = \prod_{\mathfrak{p}} \mathfrak{p}^{n_{\mathfrak{p}}}\) such that \(C_K^{\mathfrak{m}} \subseteq N_{L|K}C_L\) , is the replete ideal \[ f = \prod_ {\mathfrak {p}} f _ {\mathfrak {p}}, \] where now for an infinite place \(\mathfrak{p}\) , we have \(\mathfrak{f}_{\mathfrak{p}} = \mathfrak{p}^{n_{\mathfrak{p}}}\) with \(n_{\mathfrak{p}} = 0\) if \(L_{\mathfrak{p}} = K_{\mathfrak{p}}\) , and \(n_{\mathfrak{p}} = 1\) if \(L_{\mathfrak{p}} \neq K_{\mathfrak{p}}\) . Corollary (6.6) then continues to hold: a place \(\mathfrak{p}\) is ramified in \(L\) if and only if \(\mathfrak{p}\) occurs in the conductor \(\mathfrak{f}\) . This entails the following modifications of the above theory, as far as ray class fields are concerned. The ray class field mod 1 is the small Hilbert class field. It is now the maximal abelian extension of K which is unramified at all places. The big Hilbert class field is the ray class field for the module \(m = \prod_{p|_{\infty}} p\) . In the case of the base field Q, the field \(\mathbb{Q}(\zeta)\) of m-th roots of unity is the ray class field mod \(mp_{\infty}\) , where \(p_{\infty}\) is the infinite place. The ray class field for the module m becomes the maximal real subextension \(\mathbb{Q}(\zeta + \zeta^{-1})\) , which was not a ray class field before. This is the theory one finds in the textbooks alluded to above. It corresponds to the number fields with the Minkowski metric. The theory of ray class fields according to the treatment of this book is forced upon us already by the choice of the standard metric \(\langle x, y \rangle = \sum_{\tau} x_{\tau} \bar{y}_{\tau}\) on \(K_{R}\) taken in chap. I, §5. It is compatible with the Riemann-Roch theory of chap. III, and has the advantage of being simpler.

Theorem (6.10)

FC09-C06-U070 · Chapter VI, §6, source L17023 · not formalized

(6.10) Theorem. Let \(K\) be an imaginary quadratic number field and \(\mathfrak{a}\) an ideal of \(\mathcal{O}_K\) . Then one has: (i) The \(j\) -invariant \(j(\mathfrak{a})\) of \(\mathbb{C} / \mathfrak{a}\) is an algebraic integer which depends only on the ideal class \(\mathfrak{K}\) of \(\mathfrak{a}\) , and will therefore be denoted by \(j(\mathfrak{K})\) . (ii) Every \(j(\mathfrak{a})\) generates the Hilbert class field over \(K\) . (iii) If \(\mathfrak{a}_1, \ldots, \mathfrak{a}_h\) are representatives of the ideal class group \(Cl_K\) , then the numbers \(j(\mathfrak{a}_i)\) are conjugate to one another over \(K\) . (iv) For almost all prime ideals \(\mathfrak{p}\) of \(K\) one has \[ \varphi_ {\mathfrak {p}} j (\mathfrak {a}) = j \left(\mathfrak {p} ^ {- 1} \mathfrak {a}\right), \] where \(\varphi_{\mathfrak{p}} \in G(K(j(\mathfrak{a}))|K)\) is the Frobenius automorphism of a prime ideal \(\mathfrak{P}\) of \(K(j(\mathfrak{a}))\) above \(\mathfrak{p}\) .

Definition / construction

FC09-C06-U071 · Chapter VI, §6, source L17039 · not formalized

Note that for a totally imaginary field K there is no difference between big and small Hilbert class field. In order to go beyond the Hilbert class field, i.e., the ray class field mod 1, to the ray class fields for arbitrary modules \(m \neq 1\) , we form, for any lattice \(\Gamma \subseteq C\) , the Weber function \[ \tau_ {\Gamma} (z) = \left\{ \begin{array}{l l} - 2 ^ {7} 3 ^ {5} \frac {g _ {2} g _ {3}}{\varDelta} \wp_ {\Gamma} (z), & \mathrm{if} g _ {2} g _ {3} \neq 0, \\ - 2 ^ {9} 3 ^ {6} \frac {g _ {3}}{\varDelta} \wp_ {\Gamma} ^ {3} (z), & \mathrm{if} g _ {2} = 0, \\ 2 ^ {8} 3 ^ {4} \frac {g _ {2} ^ {2}}{\varDelta} \wp_ {\Gamma} ^ {2} (z), & \mathrm{if} g _ {3} = 0. \end{array} \right. \]

Convention / notation

FC09-C06-U072 · Chapter VI, §6, source L17045 · not formalized

For an ideal class \(\mathfrak{K} \in Cl_{K}\), let \(\mathfrak{K}^{*}\) denote the classes of the ray class group \(Cl_{K}^{\mathfrak{m}}\) sent to \((\mathfrak{m})\mathfrak{K}^{-1}\) under \(Cl_{K}^{\mathfrak{m}} \to Cl_{K}\). For \(\mathfrak{a}\) in \(\mathfrak{K}\) and an integral ideal \(\mathfrak{b}\) in \(\mathfrak{K}^{*}\), the principal ideal \(\mathfrak{a}\mathfrak{b}\mathfrak{m}^{-1} = (a)\) gives a value \(\tau_{\mathfrak{a}}(a)\) depending only on the class \(\mathfrak{K}^{*}\), denoted \[ \tau(\mathfrak{K}^{*}) = \tau_{\mathfrak{a}}(a). \] With these conventions one has theorem (6.11) on these invariants.

Theorem (6.11)

FC09-C06-U073 · Chapter VI, §6, source L17059 · not formalized

(6.11) Theorem. (i) The invariants \(\tau(\mathfrak{K}_1^*)\) , \(\tau(\mathfrak{K}_2^*)\) , …, for a fixed ideal class \(\mathfrak{K}\) , are distinct algebraic numbers which are conjugate over the Hilbert class field \(K^1 = K(j(\mathfrak{K}))\) . (ii) For an arbitrary \(\mathfrak{K}^*\) , the field \(K(j(\mathfrak{K}),\tau (\mathfrak{K}^{*}))\) is the ray class field mod \(\mathfrak{m}\) over \(K\) : \[ K ^ {\mathfrak {m}} = K \left(j (\mathfrak {K}), \tau (\mathfrak {K} ^ {*})\right). \]

Convention / notation

FC09-C06-U074 · Chapter VI, §7, source L17155 · not formalized

Let \(L|K\) be an abelian extension, and let \(\mathfrak{p}\) be an unramified prime ideal of \(K\) and \(\mathfrak{P}\) a prime ideal of \(L\) lying above \(\mathfrak{p}\) . The decomposition group \(G(L_{\mathfrak{P}}|K_{\mathfrak{p}}) \subseteq G(L|K)\) is then generated by the classical Frobenius automorphism \[ \varphi_ {\mathfrak {p}} = (\pi_ {\mathfrak {p}}, L _ {\mathfrak {P}} | K _ {\mathfrak {p}}), \] where \(\pi_{p}\) is a prime element of \(K_{p}\) . As an automorphism of L, \(\varphi_{p}\) is obviously characterized by the congruence \[ \varphi_ {\mathfrak {p}} a \equiv a ^ {q} \bmod \mathfrak {P} \quad \text {for all} \quad a \in \mathcal {O} _ {L} \] where q is the number of elements in the residue class field of p. We put \[ \varphi_ {\mathfrak {p}} =: \left(\frac {L | K}{\mathfrak {p}}\right). \]

Not formalized. Mathlib/TauCeti have Frobenius, decomposition, transfer, and class-group ingredients, but this source row requires the Artin map/class-field identification, Hilbert-class-field splitting/principalization, or Furtwängler transfer theorem. No checked source closes that full assertion.

Definition / construction

FC09-C06-U075 · Chapter VI, §7, source L17173 · after FC09-C06-U063 · not formalized

Now let m be a module of K such that L lies in the ray class field mod m. Such a module is called an module of definition for L. Since by (6.6) each prime ideal \(p \nmid m\) is unramified in L, we get a canonical homomorphism \[ \left(\frac {L | K}{\text { }}\right): J _ {K} ^ {\mathfrak {m}} \longrightarrow G (L | K) \] from the group \(J_K^{\mathfrak{m}}\) of all ideals of \(K\) which are relatively prime to \(\mathfrak{m}\) by putting, for any ideal \(\mathfrak{a} = \prod_{\mathfrak{p}} \mathfrak{p}^{\nu_{\mathfrak{p}}}\) : \[ \left(\frac {L | K}{\mathfrak {a}}\right) = \prod_ {\mathfrak {p}} \left(\frac {L | K}{\mathfrak {p}}\right) ^ {\nu_ {\mathfrak {p}}}. \] \(\left(\frac{L|K}{a}\right)\) is called the Artin symbol. If \(\mathfrak{p} \in J_K^\mathfrak{m}\) is a prime ideal and \(\pi_{\mathfrak{p}}\) a prime element of \(K_{\mathfrak{p}}\) , then clearly \[ \left(\frac {L | K}{\mathfrak {p}}\right) = \left(\langle \pi_ {\mathfrak {p}} \rangle , L | K\right), \] if \(\langle \pi_{\mathfrak{p}}\rangle \in C_K\) denotes the class of the idèle ( \(\ldots, 1, 1, \pi_{\mathfrak{p}}, 1, 1, \ldots\) ).

Theorem (7.1)

FC09-C06-U076 · Chapter VI, §7, source L17195 · not formalized

(7.1) Theorem. Let \(L|K\) be an abelian extension, and let \(\mathfrak{m}\) be a module of definition for it. Then the Artin symbol induces a surjective homomorphism \[ \left(\frac {L | K}{\text { }}\right): C l _ {K} ^ {\mathfrak {m}} \longrightarrow G (L | K) \] with kernel \(H^{\mathfrak{m}} / P_{K}^{\mathfrak{m}}\) , where \(H^{\mathfrak{m}} = (N_{L|K}J_{L}^{\mathfrak{m}})P_{K}^{\mathfrak{m}}\) , and we have an exact commutative diagram \[ \begin{array}{c} 1 \longrightarrow N _ {L | K} C _ {L} \longrightarrow C _ {K} \xrightarrow {(\text { , } L | K)} G (L | K) \longrightarrow 1 \\ \Big \downarrow \qquad \qquad \qquad \Big \downarrow \qquad \qquad \qquad \Big \downarrow_ {\mathrm{id}} \\ 1 \longrightarrow H ^ {\mathfrak {m}} / P _ {K} ^ {\mathfrak {m}} \longrightarrow C l _ {K} ^ {\mathfrak {m}} \xrightarrow {\left(\underline {{L | K}}\right)} G (L | K) \longrightarrow 1. \end{array} \]

Corollary (7.2)

FC09-C06-U077 · Chapter VI, §7, source L17243 · not formalized

(7.2) Corollary. The Artin symbol \(\left(\frac{L|K}{\mathfrak{a}}\right)\) , for \(\mathfrak{a} \in J_K^\mathfrak{m}\) , only depends on the class \(\mathfrak{a} \bmod P_K^\mathfrak{m}\) . It defines an isomorphism \[ \left(\frac {L | K}{\text { }}\right): J _ {K} ^ {\mathfrak {m}} / H ^ {\mathfrak {m}} \xrightarrow {\sim} G (L | K). \]

Definition / construction

FC09-C06-U078 · Chapter VI, §7, source L17249 · after FC09-C06-U056 · not formalized

The group \(H^{\mathfrak{m}} = (N_{L|K} J_{L}^{\mathfrak{m}}) P_{K}^{\mathfrak{m}}\) is called the “ideal group defined mod m” belonging to the extension L|K. From the existence theorem (6.1), we see that the correspondence \(L \mapsto H^{m}\) is 1–1 between subextensions of the ray class field mod m and subgroups of \(J_{K}^{m}\) containing \(P_{K}^{m}\) .

Theorem (7.3)

FC09-C06-U079 · Chapter VI, §7, source L17253 · not formalized

(7.3) Theorem (Decomposition Law). Let \(L|K\) be an abelian extension of degree \(n\) , and let \(\mathfrak{p}\) be an unramified prime ideal. Let \(\mathfrak{m}\) be a module of definition for \(L|K\) that is not divisible by \(\mathfrak{p}\) (for instance the conductor), and let \(H^{\mathfrak{m}}\) be the corresponding ideal group. If \(f\) is the order of \(\mathfrak{p} \mod H^{\mathfrak{m}}\) in the class group \(J_K^{\mathfrak{m}} / H^{\mathfrak{m}}\) , i.e., the smallest positive integer such that \[ \mathfrak {p} ^ {f} \in H ^ {\mathfrak {m}}, \] then \(\mathfrak{p}\) decomposes in \(L\) into a product \[ \mathfrak {p} = \mathfrak {P} _ {1} \dots \mathfrak {P} _ {r} \] of \(r = n / f\) distinct prime ideals of degree \(f\) over \(\mathfrak{p}\) .

Corollary (7.4)

FC09-C06-U080 · Chapter VI, §7, source L17281 · not formalized

(7.4) Corollary. The prime ideals of \(K\) which split completely in the Hilbert class field are precisely the principal prime ideals.

Theorem (7.5)

FC09-C06-U081 · Chapter VI, §7, source L17285 · not formalized

(7.5) Theorem. In the Hilbert class field every ideal \(\mathfrak{a}\) of \(K\) becomes a principal ideal.

Theorem (7.6)

FC09-C06-U082 · Chapter VI, §7, source L17307 · not formalized

(7.6) Theorem. Let \(G\) be a finitely generated group, \(G'\) its commutator subgroup, and \(G''\) the commutator subgroup of \(G'\) . If \((G: G') < \infty\) , then the transfer \[ \operatorname{Ver}: G / G ^ {\prime} \longrightarrow G ^ {\prime} / G ^ {\prime \prime} \] is the trivial homomorphism.

Lemma (7.7)

FC09-C06-U083 · Chapter VI, §7, source L17323 · not formalized

(7.7) Lemma. For every subgroup \(H\) of finite index in \(G\) , one has a commutative diagram \[ \begin{array}{c c c} G / G ^ {\prime} & \xrightarrow {\text {Ver}} & H / H ^ {\prime} \\ \delta \Big \downarrow \cong & & \delta \Big \downarrow \cong \\ I _ {G} / I _ {G} ^ {2} & \xrightarrow {S} & (I _ {H} + I _ {G} I _ {H}) / I _ {G} I _ {H}, \end{array} \] where the homomorphisms \(\delta\) are induced by \(\sigma\mapsto\delta\sigma=\sigma-1\) , and the homomorphism S is given by \[ S (x \bmod I _ {G} ^ {2}) = x \sum_ {\rho \in R} \rho \bmod I _ {G} I _ {H}, \] for a system of representatives of the left cosets \(R \ni 1\) of G/H.

Definition / construction

FC09-C06-U084 · Chapter VI, §7, source L17441 · not formalized

A problem which is closely related to the principal ideal theorem and which was first put forward by PHILIPP FURTWÄNGLER is the problem of the class field tower. This is the question whether the class field tower \[ K = K _ {0} \subseteq K _ {1} \subseteq K _ {2} \subseteq K _ {3} \subseteq \dots , \] where \(K_{i+1}\) is the Hilbert class field of \(K_{i}\) , stops after a finite number of steps. A positive answer would have the implication that the last field in the tower had class number 1 so that in it not only the ideals of K, but in fact all its ideals become principal. This perspective naturally generated the greatest interest. But the problem, after withstanding for a long time all attempts to solve it, was finally decided in the negative by the Russian mathematicians E.S. GOLOD and I.R. ŠAFAREVIČ in 1964 (see [48], [24]).

Theorem (8.1)

FC09-C06-U085 · Chapter VI, §8, source L17499 · not formalized

(8.1) Theorem. For \(a, b \in K^{*}\) one has \[ \prod_ {\mathfrak {p}} \left(\frac {a , b}{\mathfrak {p}}\right) = 1. \]

Not formalized. The project has quadratic local Hilbert-symbol formulas and Mathlib has Jacobi/Legendre reciprocity, but this row is a general n-th Hilbert product/power-residue/global reciprocity statement not implied by those quadratic ingredients.

Definition (8.2)

FC09-C06-U086 · Chapter VI, §8, source L17531 · not formalized

(8.2) Definition. For every ideal \(\mathfrak{b} = \prod_{\mathfrak{p}\nmid n}\mathfrak{p}^{\nu_{\mathfrak{p}}}\) prime to \(n\) , and every number a prime to \(\mathfrak{b}\) , we define the \(n\) -th power residue symbol by \[ \left(\frac {a}{\mathfrak {b}}\right) = \prod_ {\mathfrak {p} \nmid n} \left(\frac {a}{\mathfrak {p}}\right) ^ {\nu_ {\mathfrak {p}}}. \] Here \(\left(\frac{a}{\mathfrak{p}}\right)^{\nu_{\mathfrak{p}}} = 1\) when \(\nu_{\mathfrak{p}} = 0\) .

Convention / notation

FC09-C06-U087 · Chapter VI, §8, source L17539 · not formalized

The power residue symbol \(\left(\frac{a}{b}\right)\) is obviously multiplicative in both arguments. If b is a principal ideal (b), we write for short \(\left(\frac{a}{b}\right)=\left(\frac{a}{b}\right)\) . We now prove the general reciprocity law for the n-th power residues.

Theorem (8.3)

FC09-C06-U088 · Chapter VI, §8, source L17541 · not formalized

(8.3) Theorem. If \(a, b \in K^{*}\) are prime to each other and to \(n\) , then \[ \left(\frac {a}{b}\right) \left(\frac {b}{a}\right) ^ {- 1} = \prod_ {\mathfrak {p} | n \infty} \left(\frac {a , b}{\mathfrak {p}}\right). \]

Gauss’s Reciprocity Law (8.4)

FC09-C06-U089 · Chapter VI, §8, source L17569 · in Mathlib

(8.4) Gauss’s Reciprocity Law. Let \(K = \mathbb{Q}\) , \(n = 2\) , and let \(a\) and \(b\) be odd, relatively prime integers. Then one has \[ \left(\frac {a}{b}\right) \left(\frac {b}{a}\right) = (- 1) ^ {\frac {a - 1}{2} \frac {b - 1}{2}} (- 1) ^ {\frac {\operatorname{sgn} a - 1}{2} \frac {\operatorname{sgn} b - 1}{2}}, \] and for positive odd integers b, we have the two “supplementary theorems” \[ \left(\frac {- 1}{b}\right) = (- 1) ^ {\frac {b - 1}{2}}, \quad \left(\frac {2}{b}\right) = (- 1) ^ {\frac {b ^ {2} - 1}{8}}. \]

Formalized. Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean::def jacobiSym, protected theorem neg, theorem at_neg_one, theorem at_two, theorem quadratic_reciprocity; Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean::χ₄_eq_neg_one_pow — Apply jacobiSym.quadratic_reciprocity to |a|,|b|; moving negative numerators with jacobiSym.neg produces the extra sign factor when both signed generators are negative. at_neg_one plus χ₄_eq_neg_one_pow gives (-1/b)=(-1)^((b-1)/2) for positive odd b, and at_two with the explicit χ₈ character gives (+2/b)=(-1)^((b²-1)/8). Thus the native Jacobi API closes all clauses of (8.4).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C06-U090 · Chapter VI, §8, source L17587 · in Mathlib

The symbol \(\left(\frac{a}{b}\right)\) is called the Jacobi symbol, or also the quadratic residue symbol (although, for b not a prime number, the condition that the symbol \(\left(\frac{a}{b}\right)=1\) is no longer equivalent to the condition that a is a quadratic residue modulo b).

Formalized. Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean::def jacobiSym, theorem legendreSym.to_jacobiSym — jacobiSym a b is defined as the product of Legendre symbols over the prime factors of b with multiplicity, exactly the Jacobi/quadratic-residue symbol used in the preceding reciprocity law; the file also records that value 1 is not a square criterion for composite denominators.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d