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

FC09 — Neukirch, Algebraic Number Theory.

This chapter contains 29 definitions, 5 theorems, 27 propositions, 2 lemmas, 1 corollary, 10 examples, 6 conventions and 3 other statements.

Of the 83 statements checked against Lean, 23 are formalized somewhere and 60 are not.

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

Which versions of Lean and Mathlib were searched

Canonical source block: FC09 Neukirch Chapter IV, FC09-C04-U001–FC09-C04-U083, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 83 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/IdealProfiniteCompletion.lean, LeanCategories/ForMathlib/AdicCompletionTopology.lean, and LeanCategories/ForMathlib/DenseIntegralCompletion.lean provide explicit ideal-adic inverse-limit infrastructure. Only U019 closes as project-existing: it reuses the already validated FC09-C02 ℤ_p inverse-limit equivalence. The project has no class-formation/reciprocity or Herbrand layer.
Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native C04 coverage includes absolute/infinite Galois groups, Krull topology and infinite Galois correspondence, categorical TopCat limits/colimits, profinite groups and profinite completion, multiplicative/Noether Hilbert 90, low-degree group cohomology, the Tate long exact sequence, and coinduced representations/Shapiro.
Current Mathlib was checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. It still has no periodicTateCohomology, herbrandQuotient, or merged Mathlib/NumberTheory/CFT/ClassFormation/Basic.lean. Open Mathlib PR #42687 was inspected at O=a40561e249ebf45d2870f5d9d45bc2eb4d80b242: it defines modern Formation, FieldFormation, and ClassFormation structures, but contains no reciprocity theorem/norm-residue isomorphism, and its proposed local class-formation instance in Local.lean remains sorried. Consequently it does not close Neukirch U043–U078.
External Lean discovery found kbuzzard/ClassFieldTheory at R=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0), whose root package pins Mathlib 26245e682c354e86f2a4a300812fe4673ae107dc. The exact no-sorry files used here prove cyclic Tate periodicity, the explicit H^-1 ≃ H^1 comparison, Tate-acyclicity of induced representations plus the normal-basis identification, and the Herbrand quotient theorems. Because that package is pinned to a distinct Mathlib revision and was not validated as a drop-in dependency at P, these are conservatively recorded as reference-port, not package-import.
Strict bundle semantics was enforced. Finite-field Frobenius APIs do not earn U002 or U022 without the absolute-Galois/profinite-integer identification; generic TopCat limits do not earn U012–U016, which require compatible topological-group structures or exactness; the adic valuation-ring inverse limit does not earn U020 because that row also asserts the full unit-group inverse limit; profinite completion does not by itself earn the explicit \widehat{ℤ}=lim ℤ/nℤ and procyclic classifications U021–U024; cyclic Kummer APIs do not earn the abstract/general-abelian Kummer bundles U035–U039; and local ramification/valuation APIs do not earn Neukirch’s abstract class-field axioms or reciprocity/existence theorems.
Short derivations are credited only where the checked interfaces close the full row. U006 translates between Mathlib’s compact-totally-disconnected model and Neukirch’s open-normal-neighborhood model; U008–U011 use the categorical encoding of directed systems and TopCat’s explicit limit/colimit constructions; U037 transports Tate-acyclicity across the external normal-basis induced-representation isomorphism; U079 takes the six relevant consecutive terms of Mathlib’s Tate long exact sequence; U082 translates left/right covariance by inversion; and U083 combines external 2-periodicity with pinned Shapiro in ordinary degrees 2 and 1.
All mathlib targets were path/token validated against P, the U019 project targets against A, every reference-port target against R with sorry excluded in the cited files, and current/open negative checks against H/O.
Route totals for C04: mathlib 17, project-existing 1, package-import 0, reference-port 5, unmatched 60.

Definition / construction

FC09-C04-U001 · Chapter IV, §1, source L11264 · in Mathlib

Every field k is equipped with a distinguished Galois extension: the separable closure \(\bar{k}|k\) . Its Galois group \(G_{k}=G(\bar{k}|k)\) is called the absolute Galois group of k. As a rule, this extension will have infinite degree. It does, however, have the advantage of collecting all finite Galois extensions of k. This is why it is reasonable to try to give it a prominent place in Galois theory. But such an attempt faces the difficulty that the main theorem of Galois theory does not remain true for infinite extensions. Let us explain this in the following example: the absolute Galois group \(G_{\mathbb{F}_{p}} = G(\overline{\mathbb{F}}_{p}|\mathbb{F}_{p})\) contains the Frobenius automorphism \(\varphi\), and the subgroup it generates is a proper subgroup with the same fixed field, so the Galois correspondence fails without a topology.

Formalized. Mathlib/FieldTheory/AbsoluteGaloisGroup.lean::def absoluteGaloisGroup — Field.absoluteGaloisGroup K is AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K, the standard absolute Galois group; the algebraic closure contains representatives of all finite separable/Galois extensions.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Example / comparison

FC09-C04-U002 · Chapter IV, §1, source L11266 · not formalized

Example: The absolute Galois group \(G_{\mathbb{F}_{p}} = G(\overline{\mathbb{F}}_{p} | \mathbb{F}_{p})\) of the field \(F_{p}\) with p elements contains the Frobenius automorphism \(\varphi\) which is given by \[ x ^ {\varphi} = x ^ {p} \quad \text { for all } \quad x \in \overline {{\mathbb {F}}} _ {p}. \] The subgroup \((\varphi)=\{\varphi^{n}\mid n\in\mathbb{Z}\}\) has the same fixed field \(F_{p}\) as the whole of \(G_{F_{p}}\) . But contrary to what we are used to in finite Galois theory, we find \((\varphi)\neq G_{\mathbb{F}_{p}}\) . In order to check this, let us construct an element \(\psi\in G_{F_{p}}\) which does not belong to \((\varphi)\) . We choose a sequence \(\{a_{n}\}_{n\in\mathbb{N}}\) of integers satisfying \[ a _ {n} \equiv a _ {m} \bmod m \] whenever \(m|n\) , but such that there is no integer \(a\) satisfying \(a_{n} \equiv a \mod n\) for all \(n \in \mathbb{N}\) . An example of such a sequence is given by \(a_{n} = n'x_{n}\) , where we write \(n = n'p^{v_{p}(n)}\) , \((n', p) = 1\) , and \(1 = n'x_{n} + p^{v_{p}(n)}y_{n}\) . Now put \[ \psi_ {n} = \varphi^ {a _ {n}} | _ {\mathbb {F} _ {p ^ {n}}} \in G (\mathbb {F} _ {p ^ {n}} | \mathbb {F} _ {p}). \] If \(\mathbb{F}_{p^m} \subseteq \mathbb{F}_{p^n}\) , then \(m|n\) , so that \(a_n \equiv a_m \mod m\) , and therefore \[ \psi_ {n} | _ {\mathbb {F} _ {p ^ {m}}} = \varphi^ {a _ {n}} | _ {\mathbb {F} _ {p ^ {m}}} = \varphi^ {a _ {m}} | _ {\mathbb {F} _ {p ^ {m}}} = \psi_ {m}. \] Observe that \(\varphi|_{\mathbb{F}_{p^m}}\) has order \(m\) . Therefore the \(\psi_n\) define an automorphism \(\psi\) of \(\overline{\mathbb{F}}_p = \bigcup_{n=1}^{\infty} \mathbb{F}_{p^n}\) . Now \(\psi\) cannot belong to ( \(\varphi\) ) because \(\psi = \varphi^a\) , for \(a \in \mathbb{Z}\) , would imply \(\psi|_{\mathbb{F}_{p^n}} = \varphi^{a_n}|_{\mathbb{F}_{p^n}} = \varphi^a|_{\mathbb{F}_{p^n}}\) and hence \(a_n \equiv a \mod n\) for all \(n\) , which is what we ruled out by construction.

Not formalized. Pinned/current Mathlib has absolute Galois groups, Krull topology and infinite Galois correspondence, but this source unit adds a finite-field Frobenius-density construction or another bundled assertion not exported by a checked compatible owner.

Definition / construction

FC09-C04-U003 · Chapter IV, §1, source L11292 · in Mathlib

The example does not mean, however, that we have to chuck the main theorem of Galois theory altogether in the case of infinite extensions. We just have to amend it using the observation that the Galois group \(G = G(\Omega|k)\) of any Galois extension \(\Omega|k\) carries a canonical topology. This topology is called the Krull topology and is obtained as follows. For every \(\sigma \in G\) we take the cosets \[ \sigma G (\Omega | K) \] as a basis of neighbourhoods of \(\sigma\) , with K|k ranging over finite Galois subextensions of \(\Omega|k\) . The multiplication and the inverse map \[ G \times G \longrightarrow G, (\sigma , \tau) \longmapsto \sigma \tau , \quad \text { and } \quad G \longrightarrow G, \sigma \longmapsto \sigma^ {- 1}, \] are continuous maps, since the preimage of a fundamental open neighbourhood \(\sigma\tau G(\Omega|K)\) , resp. \(\sigma^{-1}G(\Omega|K)\) , contains the open neighbourhood \(\sigma G(\Omega|K)\times\tau G(\Omega|K)\) , resp. \(\sigma G(\Omega|K)\) . Thus G is a topological group which satisfies the following property, proposition (1.1): for every finite or infinite Galois extension \(\Omega|k\), the Galois group \(G = G(\Omega|k)\) is compact Hausdorff in the Krull topology.

Formalized. Mathlib/FieldTheory/KrullTopology.lean::krullTopology, krullTopology_mem_nhds_one_iff_of_normal — krullTopology is the topology on algebra automorphisms generated at the identity by fixing subgroups of finite subextensions; translation gives Neukirch’s coset neighborhood basis, and the supplied topological-group instance gives continuity of multiplication/inverse.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (1.1)

FC09-C04-U004 · Chapter IV, §1, source L11306 · in Mathlib

(1.1) Proposition. For every (finite or infinite) Galois extension \(\Omega|k\) the Galois group \(G = G(\Omega|k)\) is compact Hausdorff with respect to the Krull topology.

Formalized. Mathlib/FieldTheory/Galois/Profinite.lean::CompactSpace Gal(K/k); Mathlib/FieldTheory/KrullTopology.lean::krullTopology_t2 — Pinned Mathlib proves every infinite Galois group compact in the Krull topology and proves that topology T2, exactly the compact-Hausdorff assertion.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (1.2)

FC09-C04-U005 · Chapter IV, §1, source L11332 · in Mathlib

(1.2) Theorem. Let \(\Omega|k\) be a (finite or infinite) Galois extension. Then the assignment \[ K \mapsto G (\Omega | K) \] is a 1–1-correspondence between the subextensions \(K|k\) of \(\Omega|k\) and the closed subgroups of \(G(\Omega|k)\) . The open subgroups of \(G(\Omega|k)\) correspond precisely to the finite subextensions of \(\Omega|k\) .

Formalized. Mathlib/FieldTheory/Galois/Infinite.lean::IntermediateFieldEquivClosedSubgroup, isOpen_iff_finite — IntermediateFieldEquivClosedSubgroup is the infinite Galois correspondence, and isOpen_iff_finite identifies the open fixing subgroups precisely with finite intermediate extensions.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (1.3)

FC09-C04-U006 · Chapter IV, §1, source L11360 · in Mathlib

(1.3) Definition. A profinite group is a topological group G which is Hausdorff and compact, and which admits a basis of neighbourhoods of \(1 \in G\) consisting of normal subgroups.

Formalized. Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean::structure ProfiniteGrp; Mathlib/Topology/Algebra/ClopenNhdofOne.lean::exist_openNormalSubgroup_sub_open_nhds_of_one — Mathlib packages profinite groups as compact totally disconnected Hausdorff topological groups. Its clopen-neighborhood theorem supplies an open normal subgroup inside every identity neighborhood; conversely a normal-subgroup neighborhood basis separates components, giving Neukirch’s equivalent definition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C04-U007 · Chapter IV, §2, source L11400 · not formalized

Writing \(i \leq j\) if \(X_{j} \subseteq X_{i}\) (resp. \(X_{i} \subseteq X_{j}\) ) makes the indexing set I into a directed system, i.e., an ordered set in which, for every pair i, j, there exists a k such that \(i \leq k\) and \(j \leq k\) . In the case at hand, such a k is given by \(X_{k} = X_{i} \cap X_{j}\) (resp. \(X_{k} = X_{i} \cup X_{j}\) ). For \(i \leq j\) we denote the inclusion \(X_{j} \hookrightarrow X_{i}\) (resp. \(X_{i} \hookrightarrow X_{j}\) ) by \(f_{ij}\) and obtain a system \(\{X_{i}, f_{ij}\}\) of sets and maps. The operations of intersection and union are now generalized by replacing the inclusions \(f_{ij}\) with arbitrary maps.

Not formalized. Pinned/current Mathlib has categorical limits/colimits, profinite-group limits and profinite completion, and the project has explicit adic inverse-limit completions. This full source row additionally requires a topological-group exactness theorem, a units inverse limit, profinite integers/procyclic theory, a finite-field absolute-Galois identification, cyclotomic inverse-limit identification, or Pontryagin-dual profinite theorem not closed by the checked interfaces.

Definition (2.1)

FC09-C04-U008 · Chapter IV, §2, source L11402 · in Mathlib

(2.1) Definition. Let \(I\) be a directed system. A projective, resp. inductive system over \(I\) is a family \(\{X_i, f_{ij} \mid i, j \in I, i \leq j\}\) of topological spaces \(X_i\) and continuous maps \[ f _ {i j}: X _ {j} \longrightarrow X _ {i}, \quad \text { resp. } \quad f _ {i j}: X _ {i} \longrightarrow X _ {j}, \] such that one has \(f_{ii} = \mathrm{id}_{X_i}\) and \[ f _ {i k} = f _ {i j} \circ f _ {j k}, \quad \text { resp. } \quad f _ {i k} = f _ {j k} \circ f _ {i j}, \] when \(i \leq j \leq k\) .

Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::structure Functor; Mathlib/Topology/Category/TopCat/Basic.lean::structure TopCat — A functor from the directed preorder (or its opposite for inverse systems) to TopCat is exactly the family of spaces and continuous transition maps with identity/composition laws in Definition 2.1.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (2.2)

FC09-C04-U009 · Chapter IV, §2, source L11418 · in Mathlib

(2.2) Definition. The projective limit \[ X = \varprojlim_ {i \in I} X _ {i} \] of the projective system \(\{X_i, f_{ij}\}\) is defined to be the subset \[ X = \left\{(x _ {i}) _ {i \in I} \in \prod_ {i \in I} X _ {i} \mid f _ {i j} (x _ {j}) = x _ {i} \quad \text { for } \quad i \leq j \right\} \] of the product \(\prod_{i\in I}X_i\)

Formalized. Mathlib/Topology/Category/TopCat/Limits/Basic.lean::def limitCone, def limitConeIsLimit — TopCat.limitCone is explicitly the subtype of tuples u : ∀ j, F.obj j satisfying every transition compatibility, with the induced topology and coordinate projections, exactly Neukirch’s inverse-limit construction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.3)

FC09-C04-U010 · Chapter IV, §2, source L11440 · in Mathlib

(2.3) Proposition. The projective limit \(X = \varprojlim_{i} X_i\) of nonempty compact spaces \(X_i\) is itself nonempty and compact.

Formalized. Mathlib/Topology/Category/TopCat/Limits/Konig.lean::nonempty_limitCone_of_compact_t2_cofiltered_system; Mathlib/Topology/Category/CompHaus/Basic.lean::CompHaus.hasLimits, def limitCone, def limitConeIsLimit — The topological König theorem gives nonemptiness for cofiltered systems of nonempty compact Hausdorff spaces; CompHaus has explicit limits, so the same compatible-family limit is compact Hausdorff. This is Neukirch’s Proposition 2.3 under the standard compact=compact-Hausdorff convention used here.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (2.4)

FC09-C04-U011 · Chapter IV, §2, source L11444 · in Mathlib

(2.4) Definition. The inductive limit \[ X = \varinjlim_ {i \in I} X _ {i} \] of an inductive system \(\{X_i, f_{ij}\}\) is defined to be the quotient \[ X = \left(\coprod_ {i \in I} X _ {i}\right) / \sim \] of the disjoint union \(\coprod_{i\in I}X_i\) , where we consider two elements \(x_{i}\in X_{i}\) and \(x_{j}\in X_{j}\) equivalent if there exists a \(k\geq i,j\) such that \[ f _ {i k} (x _ {i}) = f _ {j k} (x _ {j}). \]

Formalized. Mathlib/CategoryTheory/Limits/Types/ColimitType.lean::def ColimitTypeRel, def ColimitType; Mathlib/Topology/Category/TopCat/Limits/Basic.lean::isColimitCoconeOfForget, topCat_hasColimits — Functor.ColimitType is the quotient of the sigma/disjoint union by the transition relation; in a directed preorder its generated equivalence is eventual equality at a common upper bound. TopCat equips this type with the colimit/final topology.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C04-U012 · Chapter IV, §2, source L11462 · not formalized

In the applications, the projective and inductive systems \(\{X_{i}, f_{ij}\}\) that occur will not just be systems of topological spaces and continuous maps, but the \(X_{i}\) will usually be topological groups, rings or modules, etc., and the \(f_{ij}\) will be continuous homomorphisms. In what follows, we will deal explicitly only with projective and inductive systems \(\{G_{i}, g_{ij}\}\) of topological groups. But since everything works exactly the same way for systems of rings or modules, these cases may be thought of tacitly as being treated as well. Let \(\{G_i, g_{ij}\}\) be a projective, resp. inductive system of topological groups. Then the projective, resp. inductive limit \[ G = \varprojlim_ {i \in I} G _ {i}, \quad \text { resp. } \quad G = \varinjlim_ {i \in I} G _ {i} \] is a topological group as well. The multiplication in the projective limit is induced by the componentwise multiplication in the product \(\prod_{i\in I}G_{i}\) . In the case of the inductive limit, given two equivalence classes \(x,y\in G=\varliminf_{i\in I}G_{i}\) , one has to choose representatives \(x_{k}\) and \(y_{k}\) in the same \(G_{k}\) in order to define \[ x y = \text { equivalence class of } x _ {k} y _ {k}. \] We leave it to the reader to check that this definition is independent of the choice of representatives, and that the operation thus defined makes G into a group. The projections \(p_{i} : \prod_{i \in I} G_{i} \to G_{i}\) , resp. the inclusions \(\iota_{i} : G_{i} \to \coprod_{i \in I} G_{i}\) , induce a family of continuous homomorphisms \[ g _ {i}: G \longrightarrow G _ {i}, \quad \text { resp. } \quad g _ {i}: G _ {i} \longrightarrow G \] such that \(g_{i} = g_{ij} \circ g_{j}\) , resp. \(g_{i} = g_{j} \circ g_{ij}\) , for \(i \leq j\) . This family has the following universal property.

Proposition (2.5)

FC09-C04-U013 · Chapter IV, §2, source L11488 · not formalized

(2.5) Proposition. If \(H\) is a topological group and \[ h _ {i}: H \longrightarrow G _ {i}, \quad \text { resp. } \quad h _ {i}: G _ {i} \longrightarrow H \] is a family of continuous homomorphisms such that \[ h _ {i} = g _ {i j} \circ h _ {j}, \quad r e s p. \quad h _ {i} = h _ {j} \circ g _ {i j} \] for \(i \leq j\) , then there exists a unique continuous homomorphism \[ h: H \longrightarrow G = \varprojlim_ {i} G _ {i}, \quad \text { resp. } \quad h: G = \varinjlim_ {i} G _ {i} \longrightarrow H \] satisfying \(h_i = g_i \circ h\) , resp. \(h_i = h \circ g_i\) , for all \(i \in I\) .

Definition / construction

FC09-C04-U014 · Chapter IV, §2, source L11508 · not formalized

Passing to the limit of a projective, resp. inductive, system is functorial: a morphism \((f_{i})_{i \in I}\) of systems induces a map on the limits. A particularly important property of this functor is its exactness. For the inductive limit \(\varinjlim\) exactness holds without restrictions, which is proposition (2.6); for the projective limit \(\varprojlim\) it requires compactness, which is proposition (2.7).

Proposition (2.6)

FC09-C04-U015 · Chapter IV, §2, source L11528 · not formalized

(2.6) Proposition. Let \(\alpha : \{G_i', g_{ij}'\} \to \{G_i, g_{ij}\}\) and \(\beta : \{G_i, g_{ij}\} \to \{G_i'', g_{ij}''\}\) be morphisms between inductive systems of topological groups such that the sequence \[ G _ {i} ^ {\prime} \xrightarrow {\alpha_ {i}} G _ {i} \xrightarrow {\beta_ {i}} G _ {i} ^ {\prime \prime} \] is exact for every \(i \in I\) . Then the induced sequence \[ \varinjlim_ {i \in I} G _ {i} ^ {\prime} \stackrel {{\alpha}} {{\longrightarrow}} \varinjlim_ {i \in I} G _ {i} \stackrel {{\beta}} {{\longrightarrow}} \varinjlim_ {i \in I} G _ {i} ^ {\prime \prime} \] is also exact.

Proposition (2.7)

FC09-C04-U016 · Chapter IV, §2, source L11558 · not formalized

(2.7) Proposition. Let \(\alpha : \{G_i', g_{ij}'\} \to \{G_i, g_{ij}\}\) and \(\beta : \{G_i, g_{ij}\} \to \{G_i'', g_{ij}''\}\) be morphisms between projective systems of compact topological groups such that the sequence \[ G _ {i} ^ {\prime} \xrightarrow {\alpha_ {i}} G _ {i} \xrightarrow {\beta_ {i}} G _ {i} ^ {\prime \prime} \] is exact for every \(i \in I\) . Then \[ \varprojlim_ {i} G _ {i} ^ {\prime} \stackrel {{\alpha}} {{\longrightarrow}} \varprojlim_ {i} G _ {i} \stackrel {{\beta}} {{\longrightarrow}} \varprojlim_ {i} G _ {i} ^ {\prime \prime} \] is again an exact sequence of compact topological groups.

Proposition (2.8)

FC09-C04-U017 · Chapter IV, §2, source L11576 · in Mathlib

(2.8) Proposition. If \(G\) is a profinite group, and if \(N\) varies over the open normal subgroups of \(G\) , then one has, algebraically as well as topologically, that \[ G \cong \varprojlim_ {N} G / N. \] If conversely \(\{G_i, g_{ij}\}\) is a projective system of finite (or even profinite) groups, then \[ G = \varprojlim_ {i} G _ {i} \] is a profinite group.

Formalized. Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean::isoLimittoFiniteQuotientFunctor; Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean::limitCone, limitConeIsLimit — isoLimittoFiniteQuotientFunctor identifies a profinite group with the limit of its finite quotients by open normal subgroups; the explicit limit cone in ProfiniteGrp proves conversely that limits of finite/profinite groups are profinite.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Example / comparison

FC09-C04-U018 · Chapter IV, §2, source L11614 · after FC09-C04-U017 · in Mathlib

Example 1: The Galois group \(G = G(\Omega | k)\) of a Galois extension \(\Omega | k\) is a profinite group with respect to the Krull topology. This was already stated in §1. If \(K | k\) varies over the finite Galois subextensions of \(\Omega | k\) , then, by definition of the Krull topology, \(G(\Omega | K)\) varies over the open normal subgroups of \(G\) . In view of the identity \(G(K | k) = G(\Omega | k) / G(\Omega | K)\) and of (2.8), we therefore obtain the Galois group \(G(\Omega | k)\) as the projective limit \[ G (\Omega | k) \cong \varprojlim G (K | k) \] of the finite Galois groups \(G(K|k)\) .

Formalized. Mathlib/FieldTheory/Galois/Profinite.lean::profiniteGalGrp, profiniteGalGrpIsoLimit — profiniteGalGrpIsoLimit is the categorical isomorphism from the Krull Galois group to the limit of the finite Galois groups of finite Galois subextensions.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Example / comparison

FC09-C04-U019 · Chapter IV, §2, source L11622 · in lean-categories

Example 2: If \(p\) is a prime number, then the rings \(\mathbb{Z} / p^n\mathbb{Z}\) , \(n \in \mathbb{N}\) , form a projective system with respect to the projections \(\mathbb{Z} / p^n\mathbb{Z} \to \mathbb{Z} / p^m\mathbb{Z}\) , for \(n \geq m\) . The projective limit \[ \mathbb {Z} _ {p} = \varprojlim_ {n} \mathbb {Z} / p ^ {n} \mathbb {Z} \] is the ring of \(p\) -adic integers (see chap. II, §1).

Formalized. LeanCategories/ForMathlib/DenseIntegralCompletion.lean::quotientPowEquivAdicCompletionIntegers, adicCompletionEquivAdicCompletionIntegers, adicCompletionHomeomorphAdicCompletionIntegers; Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean::adicCompletionIntegers.padicIntEquiv, primesEquiv — This is the already validated FC09-C02 inverse-limit route: the project identifies the height-one adic inverse limit and completed valuation ring compatibly at every quotient power; specializing R=ℤ, K=ℚ gives ℤ_p ≅ lim_n ℤ/p^nℤ.

Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d

Example / comparison

FC09-C04-U020 · Chapter IV, §2, source L11630 · not formalized

Example 3: Let \(\mathcal{O}\) be the valuation ring in a \(\mathfrak{p}\) -adic number field \(K\) and \(\mathfrak{p}\) its maximal ideal. The ideals \(\mathfrak{p}^n\) , \(n \in \mathbb{N}\) , make up a basis of neighbourhoods of the zero element 0 in \(\mathcal{O}\) . \(\mathcal{O}\) is Hausdorff and compact, and so is a profinite ring. The rings \(\mathcal{O} / \mathfrak{p}^n\) , \(n \in \mathbb{N}\) , are finite and we have a topological isomorphism \[ \mathcal {O} \cong \varprojlim_ {n} \mathcal {O} / \mathfrak {p} ^ {n}, \quad a \longmapsto \prod_ {n \in \mathbb {N}} (a \bmod \mathfrak {p} ^ {n}). \] The group of units \(U = \mathcal{O}^*\) is closed in \(\mathcal{O}\) , hence Hausdorff and compact, and the subgroups \(U^{(n)} = 1 + \mathfrak{p}^n\) form a basis of neighbourhoods of \(1 \in U\) . Thus \[ U \cong \varprojlim_ {n} U / U ^ {(n)} \] is also a profinite group. In fact, we have seen all this already in chap. II, §4.

Example / comparison

FC09-C04-U021 · Chapter IV, §2, source L11644 · not formalized

Example 4: The rings \(\mathbb{Z}/n\mathbb{Z}\) , \(n \in \mathbb{N}\) , form a projective system with respect to the projections \(\mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/m\mathbb{Z}\) , \(n|m\) , where the ordering on \(\mathbb{N}\) is now given by divisibility, \(n|m\) . The projective limit \[ \widehat {\mathbb {Z}} = \varprojlim_ {n} \mathbb {Z} / n \mathbb {Z} \] was originally called the Prüfer ring, whereas nowadays it has become customary to refer to it by the somewhat curt abbreviation “zed-hat” (or “zee-hat”). This ring is going to occupy quite an important position in what follows. It contains Z as a dense subring. The groups \(n\widehat{Z}, n \in N\) , are precisely the open subgroups of \(\widehat{Z}\) , and it is easy to verify that \[ \widehat {\mathbb {Z}} / n \widehat {\mathbb {Z}} \cong \mathbb {Z} / n \mathbb {Z}. \] Taking, for each natural number n, the prime factorization \(n = \prod_{p} p^{\nu_{p}}\) , the Chinese remainder theorem implies the decomposition \[ \mathbb {Z} / n \mathbb {Z} \cong \prod_ {p} \mathbb {Z} / p ^ {\nu_ {p}} \mathbb {Z}, \] and passing to the projective limit, \[ \widehat {\mathbb {Z}} \cong \prod_ {p} \mathbb {Z} _ {p}. \] This takes the natural embedding of \(\mathbb{Z}\) into \(\widehat{\mathbb{Z}}\) to the diagonal embedding \(\mathbb{Z} \to \prod_p \mathbb{Z}_p\) , \(a \mapsto (a, a, a, \ldots)\) .

Example / comparison

FC09-C04-U022 · Chapter IV, §2, source L11670 · not formalized

Example 5: For the field \(F_{q}\) with q elements, we get isomorphisms \[ G (\mathbb {F} _ {q ^ {n}} | \mathbb {F} _ {q}) \cong \mathbb {Z} / n \mathbb {Z}, \] one for every \(n \in N\) , by mapping the Frobenius automorphism \(\varphi_{n}\) to 1 mod \(nZ\) . Passing to the projective limit gives an isomorphism \[ G (\overline {{{\mathbb {F}}}} _ {q} | \mathbb {F} _ {q}) \cong \widehat {\mathbb {Z}} \] which sends the Frobenius automorphism \(\varphi \in G(\overline{\mathbb{F}}_q|\mathbb{F}_q)\) to \(1\in \widehat{\mathbb{Z}}\) , and the subgroup \((\varphi) = \{\varphi^n |n\in \mathbb{Z}\}\) onto the dense (but not closed) subgroup \(\mathbb{Z}\) of \(\widehat{\mathbb{Z}}\) . Given this, it is now clear, in the example at the beginning of this chapter, how we were able to construct an element \(\psi \in G(\overline{\mathbb{F}}_q|\mathbb{F}_q)\) which did not belong to \((\varphi)\) . In fact, looking at it via the isomorphism \(G(\overline{\mathbb{F}}_q|\mathbb{F}_q)\cong \widehat{\mathbb{Z}}\) , what we did amounted to writing down the element \[ (\ldots , 0, 0, 1 _ {p}, 0, 0, \ldots) \in \prod_ {\ell} \mathbb {Z} _ {\ell} = \widehat {\mathbb {Z}}, \] which does not belong to \(\mathbb{Z}\) .

Example / comparison

FC09-C04-U023 · Chapter IV, §2, source L11690 · not formalized

Example 6: Let \(\widetilde{\mathbb{Q}}|\mathbb{Q}\) be the extension obtained by adjoining all roots of unity. Its Galois group \(G(\widetilde{\mathbb{Q}}|\mathbb{Q})\) is then canonically isomorphic (as a topological group) to the group of units \(\widehat{\mathbb{Z}}^* \cong \prod_p \mathbb{Z}_p^*\) of \(\widehat{\mathbb{Z}}\) , \[ G (\widetilde {\mathbb {Q}} | \mathbb {Q}) \cong \widehat {\mathbb {Z}} ^ {*}. \] This isomorphism is obtained by passing to the projective limit from the canonical isomorphisms \[ G (\mathbb {Q} (\mu_ {n}) | \mathbb {Q}) \cong (\mathbb {Z} / n \mathbb {Z}) ^ {*}, \] where \(\mu_{n}\) denotes the group of n-th roots of unity.

Example / comparison

FC09-C04-U024 · Chapter IV, §2, source L11704 · after FC09-C04-U016 · not formalized

Example 7: The groups \(\mathbb{Z}_p\) and \(\widehat{\mathbb{Z}}\) are (additive) special cases of the class of procyclic groups. These are profinite groups \(G\) which are topologically generated by a single element \(\sigma\) ; i.e., \(G\) is the closure \((\overline{\sigma})\) of the subgroup \((\sigma) = \{\sigma^n \mid n \in \mathbb{Z}\}\) . The open subgroups of a procyclic group \(G = (\overline{\sigma})\) are all of the form \(G^n\) . Indeed, \(G^n\) is closed, being the image of the continuous map \(G \to G\) , \(x \mapsto x^n\) , and the quotient group \(G / G^n\) is finite, because it contains the finite group \(\{\sigma^\nu \bmod G^n \mid 0 \leq \nu < n\}\) as a dense subgroup, and is therefore equal to it. Conversely, if \(H\) is a subgroup of \(G\) of index \(n\) , then \(G^n \subseteq H \subseteq G\) and \(n = (G:H) \leq (G:G^n) \leq n\) , so that \(H = G^n\) . Every procyclic group \(G\) is a quotient of the group \(\widehat{\mathbb{Z}}\) . In fact, if \(G = (\overline{\sigma})\) , then we have for every \(n\) the surjective homomorphism \[ \mathbb {Z} / n \mathbb {Z} \rightarrow G / G ^ {n}, \quad 1 \bmod n \mathbb {Z} \mapsto \sigma \bmod G ^ {n}, \] and in view of (2.7), passing to the projective limit yields a continuous surjection \(\widehat{\mathbb{Z}}\to G\) .

Example / comparison

FC09-C04-U025 · Chapter IV, §2, source L11714 · not formalized

Example 8: Let A be an abelian torsion group. Then the Pontryagin dual \[ \chi (A) = \operatorname{Hom} (A, \mathbb {Q} / \mathbb {Z}) \] is a profinite group. For one has \[ A = \bigcup_ {i} A _ {i}, \] where \(A_{i}\) varies over the finite subgroups of A, and thus \[ \chi (A) = \varprojlim_ {i} \chi (A _ {i}) \] with finite groups \(\chi(A_i)\) . If for instance, \[ A = \mathbb {Q} / \mathbb {Z} = \bigcup_ {n \in \mathbb {N}} \frac {1}{n} \mathbb {Z} / \mathbb {Z}, \] then \(\chi (\frac{1}{n}\mathbb{Z} / \mathbb{Z}) = \mathbb{Z} / n\mathbb{Z}\) , so that \[ \chi (\mathbb {Q} / \mathbb {Z}) \cong \varprojlim_ {n} \mathbb {Z} / n \mathbb {Z} = \widehat {\mathbb {Z}}. \]

Example / comparison

FC09-C04-U026 · Chapter IV, §2, source L11744 · in Mathlib

Example 9: If \(G\) is any group and \(N\) varies over all normal subgroups of finite index, then the profinite group \[ \widehat {G} = \varprojlim_ {N} G / N \] is called the profinite completion of \(G\) . The profinite completion of \(\mathbb{Z}\) , for example, is the group \(\widehat{\mathbb{Z}} = \varprojlim_{n} \mathbb{Z} / n\mathbb{Z}\) .

Formalized. Mathlib/Topology/Algebra/Category/ProfiniteGrp/Completion.lean::def finiteGrpDiagram, def completion — ProfiniteCompletion.completion G is defined literally as the limit of the finite quotient diagram indexed by finite-index normal subgroups, exactly Neukirch’s profinite completion.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C04-U027 · Chapter IV, §3, source L11796 · not formalized

We denote the closed subgroups of G by \(G_{K}\) , and call these indices K “fields”; K will be called the fixed field of \(G_{K}\) . The field k such that \(G_{k} = G\) is called the base field, and \(\bar{k}\) denotes the field satisfying \(G_{\bar{k}} = \{1\}\) . The field belonging to the closure \((\overline{\sigma})\) of the cyclic group \((\sigma) = \{\sigma^{k} \mid k \in \mathbb{Z}\}\) generated by an element \(\sigma \in G\) is simply called the fixed field of \(\sigma\) .

Not formalized. Pinned/current Mathlib has Galois modules, ordinary/Tate cohomology, cyclic Kummer ingredients and Hilbert 90, but this row belongs to Neukirch’s abstract fixed-subgroup/Kummer formalism or asserts an additive/general Kummer statement not exported as one compatible owner. The external ClassFieldTheory code was credited only where an exact proved theorem-level port was found.

Definition / construction

FC09-C04-U028 · Chapter IV, §3, source L11798 · not formalized

We write formally \(K \subseteq L\) or \(L|K\) if \(G_{L} \subseteq G_{K}\) , and we call the pair \(L|K\) a field extension. \(L|K\) is called a finite extension, if \(G_{L}\) is open, i.e., of finite index in \(G_{K}\) , and this index \[ [ L: K ] := (G _ {K}: G _ {L}) \] will be called the degree of \(L|K\) . \(L|K\) is said to be normal or Galois if \(G_{L}\) is a normal subgroup of \(G_{K}\) . If this is the case, we define the Galois group of \(L|K\) by \[ G (L | K) = G _ {K} / G _ {L}. \]

Definition / construction

FC09-C04-U029 · Chapter IV, §3, source L11810 · not formalized

If \(N \supseteq L \supseteq K\) are Galois extensions of \(K\) , we define the restriction of an element \(\sigma \in G(N|K)\) to \(L\) by \[ \sigma \mid_ {L} = \sigma \bmod G (N | L) \in G (L | K). \] This gives a homomorphism \[ G (N | K) \longrightarrow G (L | K), \quad \sigma \longmapsto \sigma | _ {L}, \]

Convention / notation

FC09-C04-U030 · Chapter IV, §3, source L11822 · not formalized

The extension L|K is called cyclic, abelian, solvable, etc., if the Galois group \(G(L|K)\) has these properties. We put \[ K = \bigcap_ {i} K _ {i} \quad \left(" \text { intersection }"\right) \] if \(G_{K}\) is topologically generated by the subgroups \(G_{K_i}\) , and \[ K = \prod_ {i} K _ {i} \quad \left(" \text { composite }"\right) \] if \(G_K = \bigcap_i G_{K_i}\) . If \(G_{K'} = \sigma^{-1}G_K\sigma\) for \(\sigma \in G\) , we write \(K' = K^\sigma\) .

Definition / construction

FC09-C04-U031 · Chapter IV, §3, source L11862 · not formalized

For every extension \(L|K\) we have \(A_K \subseteq A_L\) , and if \(L|K\) is finite, then we have the norm map \[ N _ {L | K}: A _ {L} \longrightarrow A _ {K}, \quad N _ {L | K} (a) = \prod_ {\sigma} a ^ {\sigma}, \] where \(\sigma\) varies over a system of representatives of \(G_{L} \backslash G_{K}\) . If \(L|K\) is Galois, then \(A_{L}\) is a \(G(L|K)\) -module and one has \[ A _ {L} ^ {G (L | K)} = A _ {K}. \] At the center of class field theory there is the norm residue group \[ H ^ {0} \big (G (L | K), A _ {L} \big) = A _ {K} / N _ {L | K} A _ {L}. \] We also consider the group \[ H ^ {- 1} \big (G (L | K), A _ {L} \big) = _ {N _ {L | K}} A _ {L} / I _ {G (L | K)} A _ {L}, \] where \[ { } _ { N _ { L | K } } A _ { L } = \left\{ a \in A _ { L } \mid N _ { L | K } ( a ) = 1 \right\} \] is the “norm-one group” and \(I_{G(L|K)}A_{L}\) is the subgroup of \(N_{L|K}A_{L}\) which is generated by all elements \[ a ^ {\sigma - 1} := a ^ {\sigma} a ^ {- 1}, \] with \(a \in A_L\) , and \(\sigma \in G(L|K)\) . If \(G(L|K)\) is cyclic and \(\sigma\) is a generator, then \(I_{G(L|K)}A_L\) is simply the group \[ A _ {L} ^ {\sigma - 1} = \left\{a ^ {\sigma - 1} \mid a \in A _ {L} \right\}. \]

Axiom (3.1)

FC09-C04-U032 · Chapter IV, §3, source L11908 · not formalized

(3.1) Axiom. One has \(H^{-1}(G(L|K), A_{L}) = 1\) for all finite cyclic extensions L|K.

Definition / construction

FC09-C04-U033 · Chapter IV, §3, source L11910 · not formalized

The theory we are about to develop makes reference to a surjective \(G\) -homomorphism \[ \wp : A \longrightarrow A, \quad a \longmapsto a ^ {\wp}, \] with finite cyclic kernel \(\mu_{\wp}\) . The order \(n = \# \mu_{\wp}\) is called the exponent of the operator \(\wp\) . The case of prime interest to us is when \(\wp\) is the n-th power map \(a \mapsto a^{n}\) , and \(\mu_{\wp} = \mu_{n} = \{\xi \in A \mid \xi^{n} = 1\}\) is the group of “n-th roots of unity” in A.

Definition / construction

FC09-C04-U034 · Chapter IV, §3, source L11918 · not formalized

We now fix a field \(K\) such that \(\mu_{\wp} \subseteq A_K\) . For every subset \(B \subseteq A\) , let \(K(B)\) denote the fixed field of the closed subgroup \[ H = \left\{\sigma \in G _ {K} \mid b ^ {\sigma} = b \text { for all } b \in B \right\} \] of \(G_{K}\) . If B is \(G_{K}\) -invariant, then \(K(B)|K\) is obviously Galois. A Kummer extension (with respect to \(\wp\) ) is by definition an extension of the form \[ K \left(\wp^ {- 1} (\Delta)\right) | K, \] where \(\Delta\subseteq A_{K}\) . A Kummer extension \(K(\wp^{-1}(\Delta))|K\) is always Galois, and its Galois group is abelian of exponent n. Indeed, for an extension \(K(\wp^{-1}(a))|K\) , we have the injective homomorphism \[ G\left(K(\wp^{-1}(a))|K\right) \hookrightarrow \mu_{\wp}, \quad \sigma \mapsto \alpha^{\sigma-1}, \] where \(\alpha \in \wp^{-1}(a)\).

Proposition (3.2)

FC09-C04-U035 · Chapter IV, §3, source L11946 · not formalized

(3.2) Proposition. If \(L|K\) is an abelian extension of exponent \(n\) , then \[ L = K \left(\wp^ {- 1} (\Delta)\right) \quad \text { with } \quad \Delta = A _ {L} ^ {\wp} \cap A _ {K}. \] If in particular, \(L|K\) is cyclic, then we find \(L = K(\alpha)\) with \(\alpha^{\wp} = a \in A_K\) .

Theorem (3.3)

FC09-C04-U036 · Chapter IV, §3, source L11958 · not formalized

(3.3) Theorem. The correspondence \[ \Delta \longmapsto L = K \left(\wp^ {- 1} (\Delta)\right) \] is a 1-1-correspondence between the groups \(\Delta\) such that \(A_K^\wp \subseteq \Delta \subseteq A_K\) and the abelian extensions \(L|K\) of exponent \(n\) . If \(\Delta\) and \(L\) correspond to each other, then \(A_L^\wp \cap A_K = \Delta\) , and we have a canonical isomorphism \[ \Delta / A _ {K} ^ {\wp} \cong \operatorname{Hom} \left(G (L | K), \mu_ {\wp}\right), \quad a \bmod A _ {K} ^ {\wp} \longmapsto \chi_ {a}, \] where the character \(\chi_{a}: G(L|K) \to \mu_{\wp^{-}}\) is given by \(\chi_{a}(\sigma) = \alpha^{\sigma - 1}\) , for \(\alpha \in \wp^{-1}(a)\) .

Proposition (3.4)

FC09-C04-U037 · Chapter IV, §3, source L12032 · in another Lean project

(3.4) Proposition. For every cyclic finite field extension \(L|K\) , one has \(H^{-1}(G(L|K), L) = 1\) .

Formalized. kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/IndCoind/Finite.lean::def iso_ind₁; kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean::trivialTateCohomology_ind₁ — The external workshop proves that the additive Galois representation of a finite Galois extension is an induced trivial representation via the normal basis theorem, and that such induced representations have trivial Tate cohomology. Transporting degree −1 across iso_ind₁ gives Neukirch’s additive Hilbert 90.

Searched: R=ccc3323c6750abca25b49b35106f54eb3a398509 (Mathlib pin 26245e682c354e86f2a4a300812fe4673ae107dc, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (3.5)

FC09-C04-U038 · Chapter IV, §3, source L12040 · in Mathlib

(3.5) Theorem (Hilbert 90). For a cyclic field extension \(L|K\) one always has \[ H ^ {- 1} \big (G (L | K), L ^ {*} \big) = 1. \] In other words: An element \(\alpha \in L^{*}\) of norm \(N_{L|K}(\alpha) = 1\) is of the form \(\alpha = \beta^{\sigma - 1}\) , where \(\beta \in L^{*}\) and \(\sigma\) is a generator of \(G(L|K)\) .

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean::exists_div_of_norm_eq_one — exists_div_of_norm_eq_one states that for a generator of a finite cyclic Galois group, every norm-one element is a quotient of an element and its conjugate, equivalent (after the generator/inverse convention) to α=β^(σ-1).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Corollary (3.6)

FC09-C04-U039 · Chapter IV, §3, source L12060 · not formalized

(3.6) Corollary. Let \(n\) be a natural number which is relatively prime to the characteristic of the field \(K\) , and assume that \(\mu_n \subseteq K\) . Then the abelian extensions \(L|K\) of exponent \(n\) correspond 1-1 to the subgroups \(\Delta \subseteq K^*\) which contain \(K^{*n}\) , via the rule \[ \Delta \mapsto L = K \left(\sqrt [ n ]{\Delta}\right), \] and we have \[ G (L | K) \cong \operatorname{Hom} (\Delta / K ^ {* n}, \mu_ {n}). \]

Definition / construction

FC09-C04-U040 · Chapter IV, §3, source L12092 · in Mathlib

The functions \(f_{a}\) are called 1-coboundaries and form a subgroup \(B^{1}(G,A)\) of \(Z^{1}(G,A)\). One defines \[ H^{1}(G,A) = Z^{1}(G,A)/B^{1}(G,A), \] and obtains as a first result about this group proposition (3.7): if \(G\) is cyclic, then \(H^{1}(G,A) \cong H^{-1}(G,A)\).

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::def IsMulCocycle₁, def IsMulCoboundary₁, def cocycles₁, def coboundaries₁, abbrev H1, def H1Iso — The low-degree cohomology API defines multiplicative 1-cocycles/coboundaries and the additive cocycle/coboundary submodules; H1 with H1Iso realizes their quotient, matching Neukirch’s definition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.7)

FC09-C04-U041 · Chapter IV, §3, source L12100 · in another Lean project

(3.7) Proposition. If \(G\) is cyclic, then \(H^1(G, A) \cong H^{-1}(G, A)\) .

Formalized. kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::def periodicTateCohomology; kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean::def tateHNeg1LinearEquivH1; Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::isoGroupCohomology — tateHNeg1LinearEquivH1 is exactly the degree −1 to degree 1 cyclic Tate-periodicity isomorphism, built from the proved periodicTateCohomology and Mathlib’s positive-degree comparison.

Searched: R=ccc3323c6750abca25b49b35106f54eb3a398509 (Mathlib pin 26245e682c354e86f2a4a300812fe4673ae107dc, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.8)

FC09-C04-U042 · Chapter IV, §3, source L12124 · in Mathlib

(3.8) Proposition. For a finite Galois field extension \(L|K\) , one has that \[ H ^ {1} \big (G (L | K), L ^ {*} \big) = 1. \]

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean::H1ofAutOnUnitsUnique — H1ofAutOnUnitsUnique makes the first cohomology of the automorphism action on Lˣ a unique type for every finite extension, exactly the H¹-vanishing statement.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C04-U043 · Chapter IV, §4, source L12192 · not formalized

The further development will now be based on a fixed choice of a surjective continuous homomorphism \[ d: G \longrightarrow \widehat {\mathbb {Z}} \] from the profinite group \(G\) onto the procyclic group \(\widehat{\mathbb{Z}} = \varprojlim \mathbb{Z} / n\mathbb{Z}\) (see §2, example 4). This homomorphism will produce a theory which is an abstract reflection of the ramification theory of \(\mathfrak{p}\) -adic number fields. Indeed, in the case where \(G\) is the absolute Galois group \(G_{k} = G(\bar{k} | k)\) of a \(\mathfrak{p}\) -adic number field \(k\) , such a surjective homomorphism \(d: G \to \widehat{\mathbb{Z}}\) arises via the maximal unramified extension \(\tilde{k} | k\) : if \(\mathbb{F}_q\) is the residue class field of \(k\) , then, by chap. II, §9, p. 173 and example 5 in §2, we have canonical isomorphisms \[ G (\tilde {k} | k) \cong G (\overline {{{\mathbb {F}}}} _ {q} | \mathbb {F} _ {q}) \cong \widehat {\mathbb {Z}} \] which associate to the element \(1 \in \widehat{\mathbb{Z}}\) the Frobenius automorphism \(\varphi \in G(\tilde{k} | k)\) . It is defined by \[ a ^ {\varphi} \equiv a ^ {q} \bmod \tilde {\mathfrak {p}} \quad \text { for } \quad a \in \tilde {\mathcal {O}}, \] where \(\tilde{O}\) , resp. \(\tilde{p}\) , denote the valuation ring of \(\tilde{k}\) , resp. its maximal ideal. The homomorphism \(d: G \to \widehat{Z}\) in question is then given, in this concrete case, as the composite \[ G \longrightarrow G (\tilde {k} | k) \stackrel {\sim} {\longrightarrow} \widehat {\mathbb {Z}}. \] In the abstract situation, the initial choice of a surjective homomorphism \(d: G \to \widehat{Z}\) mimics the p-adic case, but the applications of the theory are by no means confined to p-adic number fields. The kernel I of d has a certain fixed field \(\tilde{k}|k\) , and d induces an isomorphism \(G(\tilde{k}|k) \cong \widehat{\mathbb{Z}}\) .

Not formalized. This row is part of Neukirch’s abstract class-field structure (degree map to profinite integers, abstract valuation/norm axioms, reciprocity map, norm topology, or existence theorem). Current Mathlib and the open class-formations PR provide cohomological formation infrastructure but no checked source-complete owner for this explicit bundle or its reciprocity/existence conclusion.

Convention / notation

FC09-C04-U044 · Chapter IV, §4, source L12218 · not formalized

More generally, for any field K we denote by \(I_{K}\) the kernel of the restriction \(d: G_{K} \to \widehat{Z}\) , and call it the inertia group over K. Since \[ I _ {K} = G _ {K} \cap I = G _ {K} \cap G _ {\tilde {k}} = G _ {K \tilde {k}}, \] the fixed field \(\widetilde{K}\) of \(I_K\) is the composite \[ \widetilde {K} = K \widetilde {k}. \]

Definition / construction

FC09-C04-U045 · Chapter IV, §4, source L12230 · not formalized

We call \(\widetilde{K}|K\) the maximal unramified extension of \(K\) . We put \[ f _ {K} = \left(\widehat {\mathbb {Z}}: d (G _ {K})\right), \quad e _ {K} = (I: I _ {K}) \] and obtain, when \(f_{K}\) is finite, a surjective homomorphism \[ d _ {K} = \frac {1}{f _ {K}} d: G _ {K} \longrightarrow \widehat {\mathbb {Z}} \] with kernel \(I_K\) , and an isomorphism \[ d _ {K}: G (\widetilde {K} | K) \stackrel {\sim} {\longrightarrow} \widehat {\mathbb {Z}}. \]

Definition (4.1)

FC09-C04-U046 · Chapter IV, §4, source L12248 · not formalized

(4.1) Definition. The element \(\varphi_K \in G(\widetilde{K}|K)\) such that \(d_K(\varphi_K) = 1\) is called the Frobenius over \(K\) . For a field extension \(L|K\) we define the inertia degree \(f_{L|K}\) and the ramification index \(e_{L|K}\) by \[ f _ {L \mid K} = \left(d (G _ {K}): d (G _ {L})\right) \quad \text { and } \quad e _ {L \mid K} = (I _ {K}: I _ {L}). \]

Proposition (4.2)

FC09-C04-U047 · Chapter IV, §4, source L12262 · not formalized

(4.2) Proposition. For every extension \(L|K\) we have the “fundamental identity” \[ [ L: K ] = f _ {L | K} e _ {L | K}. \]

Definition / construction

FC09-C04-U048 · Chapter IV, §4, source L12282 · not formalized

\(L|K\) is called unramified if \(e_{L|K} = 1\) , i.e., if \(L \subseteq \widetilde{K}\) . \(L|K\) is called totally ramified if \(f_{L|K} = 1\) , i.e., if \(L \cap \widetilde{K} = K\) . In the unramified case, we have the surjective homomorphism \[ G (\widetilde {K} | K) \to G (L | K) \] and, if \(f_{K} < \infty\) , we call the image \(\varphi_{L|K}\) of \(\varphi_{K}\) the Frobenius automorphism of \(L|K\) .

Proposition (4.3)

FC09-C04-U049 · Chapter IV, §4, source L12304 · not formalized

(4.3) Proposition. If \(f_{K}\) and \(f_{L}\) are finite, then \(f_{L|K} = f_{L} / f_{K}\) , and we have the commutative diagram \[ \begin{array}{c c c} G _ {L} & \xrightarrow {d _ {L}} & \widehat {\mathbb {Z}} \\ \Big \downarrow & & \Big \downarrow f _ {L | K} \\ G _ {K} & \xrightarrow {d _ {K}} & \widehat {\mathbb {Z}}. \end{array} \] In particular, one has \(\varphi_L|_{\tilde{K}} = \varphi_K^{f_{L|K}}\) .

Proposition (4.4)

FC09-C04-U050 · Chapter IV, §4, source L12320 · not formalized

(4.4) Proposition. For a finite Galois extension \(L|K\) the mapping \[ \operatorname{Frob} (\widetilde {L} | K) \longrightarrow G (L | K), \quad \sigma \longmapsto \sigma | _ {L}, \] is surjective.

Proposition (4.5)

FC09-C04-U051 · Chapter IV, §4, source L12338 · not formalized

(4.5) Proposition. Let \(\tilde{\sigma} \in \operatorname{Frob}(\widetilde{L}|K)\) , and let \(\Sigma\) be the fixed field of \(\tilde{\sigma}\) . Then we have: \[ \text {(i)} \quad f _ {\Sigma | K} = d _ {K} (\tilde {\sigma}), \text {(ii)} \quad [ \Sigma : K ] < \infty , \text {(iii)} \quad \widetilde {\Sigma} = \widetilde {L}, \text {(iv)} \quad \tilde {\sigma} = \varphi_ {\Sigma}. \]

Definition (4.6)

FC09-C04-U052 · Chapter IV, §4, source L12368 · not formalized

(4.6) Definition. A henselian valuation of \(A_{k}\) with respect to \(d: G \to \widehat{\mathbb{Z}}\) is a homomorphism \[ v: A _ {k} \to \widehat {\mathbb {Z}} \] satisfying the following properties: (i) \(v(A_{k}) = Z\supseteq \mathbb{Z}\) and \(Z / nZ\cong \mathbb{Z} / n\mathbb{Z}\) for all \(n\in \mathbb{N}\) , (ii) \(v(N_{K|k}A_K) = f_K Z\) for all finite extensions \(K|k\) .

Proposition (4.7)

FC09-C04-U053 · Chapter IV, §4, source L12382 · not formalized

(4.7) Proposition. For every field \(K\) which is finite over \(k\) , the formula \[ v _ {K} = \frac {1}{f _ {K}} v \circ N _ {K | k}: A _ {K} \longrightarrow Z \] defines a surjective homomorphism satisfying the following properties: (i) \(v_{K} = v_{K^{\sigma}} \circ \sigma\) for all \(\sigma \in G\) . (ii) For every finite extension \(L|K\) , one has the commutative diagram \[ \begin{array}{c c c} A _ {L} & \xrightarrow {v _ {L}} & \widehat {\mathbb {Z}} \\ N _ {L | K} \Big \downarrow & & \Big \downarrow f _ {L | K} \\ A _ {K} & \xrightarrow {v _ {K}} & \widehat {\mathbb {Z}}. \end{array} \]

Definition (4.8)

FC09-C04-U054 · Chapter IV, §4, source L12410 · not formalized

(4.8) Definition. A prime element of \(A_K\) is an element \(\pi_K \in A_K\) such that \(v_K(\pi_K) = 1\) . We put \[ U _ {K} = \left\{u \in A _ {K} \mid v _ {K} (u) = 0 \right\}. \]

Convention / notation

FC09-C04-U055 · Chapter IV, §5, source L12456 · not formalized

In the following we introduce the convention that the letter K, whenever it occurs without embellishments or commentary to the contrary, will always denote a field of finite degree over k. We furthermore impose the following axiomatic condition, which will be systematically assumed in the sequel.

Axiom (5.1)

FC09-C04-U056 · Chapter IV, §5, source L12458 · not formalized

(5.1) Axiom. For every unramified finite extension \(L|K\) one has \[ H ^ {i} \big (G (L | K), U _ {L} \big) = 1 \quad \text { for } \quad i = 0, - 1. \]

Definition / construction

FC09-C04-U057 · Chapter IV, §5, source L12464 · not formalized

For an infinite extension \(L|K\) we set \[ N _ {L | K} A _ {L} = \bigcap_ {M} N _ {M | K} A _ {M}, \] with \(M|K\) varying over the finite subextensions of \(L|K\) .

Definition / construction

FC09-C04-U058 · Chapter IV, §5, source L12472 · not formalized

Our goal is to define a canonical homomorphism \[ r _ {L | K}: G (L | K) \longrightarrow A _ {K} / N _ {L | K} A _ {L} \] for every finite Galois extension \(L|K\) . To this end, we pass from \(L|K\) to the extension \(\widetilde{L}|K\) and define first a mapping on the semigroup \[ \operatorname{Frob} (\widetilde {L} | K) = \left\{\sigma \in G (\widetilde {L} | K) \mid d _ {K} (\sigma) \in \mathbb {N} \right\}. \]

Definition (5.2)

FC09-C04-U059 · Chapter IV, §5, source L12484 · not formalized

(5.2) Definition. The reciprocity map \[ r _ {\tilde {L} | K}: \operatorname{Frob} (\widetilde {L} | K) \longrightarrow A _ {K} / N _ {\tilde {L} | K} A _ {\tilde {L}} \] is defined by \[ r _ {\tilde {L} | K} (\sigma) = N _ {\Sigma | K} (\pi_ {\Sigma}) \bmod N _ {\tilde {L} | K} A _ {\tilde {L}}, \] where \(\Sigma\) is the fixed field of \(\sigma\) and \(\pi_{\Sigma} \in A_{\Sigma}\) is a prime element.

Definition / construction

FC09-C04-U060 · Chapter IV, §5, source L12520 · not formalized

Now we introduce the homomorphism \[ N = N _ {\tilde {L} | \tilde {K}}: A _ {\tilde {L}} \longrightarrow A _ {\tilde {K}} \] and prove two lemmas for it.

Lemma (5.3)

FC09-C04-U061 · Chapter IV, §5, source L12528 · not formalized

(5.3) Lemma. Let \(\varphi, \sigma \in \operatorname{Frob}(\widetilde{L}|K)\) with \(d_K(\varphi) = 1\) , \(d_K(\sigma) = n\) . If \(\Sigma\) is the fixed field of \(\sigma\) and \(a \in A_{\Sigma}\) , then \[ N _ {\Sigma | K} (a) = (N \circ \varphi_ {n}) (a) = (\varphi_ {n} \circ N) (a). \]

Lemma (5.4)

FC09-C04-U062 · Chapter IV, §5, source L12550 · not formalized

(5.4) Lemma. If \(x \in H_0(G(\widetilde{L}|\widetilde{K}), U_{\widetilde{L}})\) is fixed by an element \(\varphi \in G(\widetilde{L}|K)\) such that \(d_K(\varphi) = 1\) , i.e., \(x^\varphi = x\) , then \[ N (x) \in N _ {\tilde {L} | K} U _ {\tilde {L}}. \]

Proposition (5.5)

FC09-C04-U063 · Chapter IV, §5, source L12588 · not formalized

(5.5) Proposition. The reciprocity map \[ r _ {\widetilde {L} | K}: \operatorname{Frob} (\widetilde {L} | K) \longrightarrow A _ {K} / N _ {\widetilde {L} | K} A _ {\widetilde {L}} \] is multiplicative.

Proposition (5.6)

FC09-C04-U064 · Chapter IV, §5, source L12662 · not formalized

(5.6) Proposition. For every finite Galois extension \(L|K\) , there is a canonical homomorphism \[ r _ {L \mid K}: G (L \mid K) \longrightarrow A _ {K} / N _ {L \mid K} A _ {L} \] given by \[ r _ {L | K} (\sigma) = N _ {\Sigma | K} \left(\pi_ {\Sigma}\right) \bmod N _ {L | K} A _ {L}, \] where \(\Sigma\) is the fixed field of a preimage \(\tilde{\sigma} \in \mathrm{Frob}(\widetilde{L}|K)\) of \(\sigma \in G(L|K)\) and \(\pi_{\Sigma} \in A_{\Sigma}\) is a prime element. It is called the reciprocity homomorphism of \(L|K\) .

Proposition (5.7)

FC09-C04-U065 · Chapter IV, §5, source L12682 · not formalized

(5.7) Proposition. If \(L|K\) is an unramified extension, then the reciprocity map \[ r _ {L | K}: G (L | K) \longrightarrow A _ {K} / N _ {L | K} A _ {L} \] is given by \[ r _ {L | K} (\varphi_ {L | K}) = \pi_ {K} \bmod N _ {L | K} A _ {L}, \] and is an isomorphism.

Proposition (5.8)

FC09-C04-U066 · Chapter IV, §5, source L12706 · not formalized

(5.8) Proposition. Let \(L|K\) and \(L'|K'\) be finite Galois extensions, so that \(K \subseteq K'\) and \(L \subseteq L'\) , and let \(\sigma \in G\) . Then we have the commutative diagrams \[ \begin{array}{c c c} G (L ^ {\prime} | K ^ {\prime}) \xrightarrow {r _ {L ^ {\prime} | K ^ {\prime}}} A _ {K ^ {\prime}} / N _ {L ^ {\prime} | K ^ {\prime}} A _ {L ^ {\prime}} & G (L | K) \xrightarrow {r _ {L | K}} A _ {K} / N _ {L | K} A _ {L} \\ \Big \downarrow & \Big \downarrow_ {N _ {K ^ {\prime} | K}} & \Big \downarrow_ {\sigma^ {*}} \\ G (L | K) \xrightarrow {r _ {L | K}} A _ {K} / N _ {L | K} A _ {L} & G (L ^ {\sigma} | K ^ {\sigma}) \xrightarrow {r _ {L ^ {\sigma} | K ^ {\sigma}}} A _ {K ^ {\sigma}} / N _ {L ^ {\sigma} | K ^ {\sigma}} A _ {L ^ {\sigma}} \end{array} \] where the vertical arrows on the left are given by \(\sigma'\mapsto\sigma'|_{L}\) , resp. by the conjugation \(\tau\mapsto\sigma^{-1}\tau\sigma\) .

Definition / construction

FC09-C04-U067 · Chapter IV, §5, source L12726 · not formalized

Another very interesting functorial property of the reciprocity map is obtained via the transfer (Verlagerung in German). For an arbitrary group G, let \(G'\) denote the commutator subgroup and write \[ G ^ {a b} = G / G ^ {\prime} \] for the maximal abelian quotient group. If then \(H \subseteq G\) is a subgroup of finite index, we have a canonical homomorphism \[ \operatorname{Ver}: G ^ {a b} \longrightarrow H ^ {a b}, \] which is called transfer from G to H. This homomorphism is defined as follows (see [75], chap. IV, §1). Let \(R\) be a system of representatives for the left cosets of \(H\) in \(G\) , \(G = RH\) , \(1 \in R\) . If \(\sigma \in G\) we write, for every \(\rho \in R\) , \[ \sigma \rho = \rho^ {\prime} \sigma_ {\rho}, \quad \sigma_ {\rho} \in H, \quad \rho^ {\prime} \in R, \] and we define \[ \operatorname{Ver} \left(\sigma \bmod G ^ {\prime}\right) = \prod_ {\rho \in R} \sigma_ {\rho} \bmod H ^ {\prime}. \]

Proposition (5.9)

FC09-C04-U068 · Chapter IV, §5, source L12772 · not formalized

(5.9) Proposition. Let \(L|K\) be a finite Galois extension and \(K'\) an intermediate field. Then we have the commutative diagram \[ \begin{array}{c c c} G (L | K ^ {\prime}) ^ {a b} & \xrightarrow {r _ {L | K ^ {\prime}}} & A _ {K ^ {\prime}} / N _ {L | K ^ {\prime}} A _ {L} \\ \text {Ver} \Big \uparrow & & \Big \uparrow \\ G (L | K) ^ {a b} & \xrightarrow {r _ {L | K}} & A _ {K} / N _ {L | K} A _ {L}, \end{array} \] where the arrow on the right is induced by inclusion.

Class Field Axiom (6.1)

FC09-C04-U069 · Chapter IV, §6, source L12872 · not formalized

(6.1) Class Field Axiom. For every cyclic extension \(L|K\) one has \[ \# H ^ {i} \big (G (L | K), A _ {L} \big) = \left\{ \begin{array}{l l} [ L: K ] & \text {for i = 0 ,} \\ 1 & \text {for i = -1 .} \end{array} \right. \]

Proposition (6.2)

FC09-C04-U070 · Chapter IV, §6, source L12880 · not formalized

(6.2) Proposition. For a finite unramified extension \(L|K\) , one has \[ H ^ {i} \big (G (L | K), U _ {L} \big) = 1 \quad \text { for } \quad i = 0, - 1. \]

Definition / construction

FC09-C04-U071 · Chapter IV, §6, source L12896 · after FC09-C04-U069, FC09-C04-U070 · not formalized

By definition, a class field theory is a pair of homomorphisms \[ \left(d: G \to \widehat {\mathbb {Z}}, v: A \to \widehat {\mathbb {Z}}\right), \] where A is a G-module which satisfies axiom (6.1), d is a surjective continuous homomorphism, and v is a henselian valuation. From proposition (6.2) and §5, we obtain for every finite Galois extension \(L|K\) , the reciprocity homomorphism \[ r _ {L | K}: G (L | K) ^ {a b} \longrightarrow A _ {K} / N _ {L | K} A _ {L}. \]

Theorem (6.3)

FC09-C04-U072 · Chapter IV, §6, source L12910 · not formalized

(6.3) Theorem. For every finite Galois extension \(L|K\) , the homomorphism \[ r _ {L | K}: G (L | K) ^ {a b} \longrightarrow A _ {K} / N _ {L | K} A _ {L} \] is an isomorphism.

Definition / construction

FC09-C04-U073 · Chapter IV, §6, source L12956 · after FC09-C04-U066, FC09-C04-U068 · not formalized

The inverse of the mapping \(r_{L|K}: G(L|K)^{ab} \to A_K / N_{L|K} A_L\) gives, for every finite Galois extension L|K, a surjective homomorphism \[ (, L | K): A _ {K} \longrightarrow G (L | K) ^ {a b} \] with kernel \(N_{L|K}A_L\) . This map is called the norm residue symbol of \(L|K\) . From (5.8) and (5.9) we have the compatibility of proposition (6.4): for finite Galois extensions \(L|K\) and \(L'|K'\) with \(K \subseteq K'\) and \(L \subseteq L'\), and \(\sigma \in G\), the norm residue symbols fit into commutative diagrams.

Proposition (6.4)

FC09-C04-U074 · Chapter IV, §6, source L12964 · not formalized

(6.4) Proposition. Let \(L|K\) and \(L'|K'\) be finite Galois extensions such that \(K \subseteq K'\) and \(L \subseteq L'\) , and let \(\sigma \in G\) . Then we have the commutative diagrams \[ \begin{array}{c c} A _ {K ^ {\prime}} \xrightarrow {(\quad , L ^ {\prime} | K ^ {\prime})} G (L ^ {\prime} | K ^ {\prime}) ^ {a b} & A _ {K} \xrightarrow {(\quad , L | K)} G (L | K) ^ {a b} \\ N _ {K ^ {\prime} | K} \Biggl \downarrow & \sigma \Biggl \downarrow \\ A _ {K} \xrightarrow {(\quad , L | K)} G (L | K) ^ {a b}, & A _ {K ^ {\sigma}} \xrightarrow {(\quad , L ^ {\sigma} | K ^ {\sigma})} G (L ^ {\sigma} | K ^ {\sigma}) ^ {a b}, \end{array} \] and if \(K' \subseteq L\) , we have the commutative diagram \[ \begin{array}{c} A _ {K ^ {\prime}} \xrightarrow {(\quad , L | K ^ {\prime})} G (L | K ^ {\prime}) ^ {a b} \\ \Bigg \uparrow \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \Bigg \uparrow_ {\text {Ver}} \\ A _ {K} \xrightarrow {(\quad , L | K)} G (L | K) ^ {a b}. \end{array} \]

Proposition (6.5)

FC09-C04-U075 · Chapter IV, §6, source L12990 · not formalized

(6.5) Proposition. One has \[ (a, \widetilde {K} | K) = \varphi_ {K} ^ {v _ {K} (a)}, \quad \text { and thus } \quad d _ {K} \circ (\mathbf {\Omega}, \widetilde {K} | K) = v _ {K}. \]

Definition / construction

FC09-C04-U076 · Chapter IV, §6, source L13006 · not formalized

For every field K, we equip the group \(A_{K}\) with a topology by declaring the cosets \(aN_{L|K}A_{L}\) to be a basis of neighbourhoods of \(a \in A_{K}\) , where \(L|K\) varies over all finite Galois extensions of K. We call this topology the norm topology of \(A_{K}\) .

Proposition (6.6)

FC09-C04-U077 · Chapter IV, §6, source L13008 · not formalized

(6.6) Proposition. (i) The open subgroups of \(A_K\) are precisely the closed subgroups of finite index. (ii) The valuation \(v_{K}: A_{K} \to \widehat{\mathbb{Z}}\) is continuous. (iii) If \(L|K\) is a finite extension, then \(N_{L|K}: A_L \to A_K\) is continuous. (iv) \(A_{K}\) is Hausdorff if and only if the group \[ A _ {K} ^ {0} = \bigcap_ {L} N _ {L | K} A _ {L} \] of universal norms is trivial.

Theorem (6.7)

FC09-C04-U078 · Chapter IV, §6, source L13050 · after FC09-C04-U072 · not formalized

(6.7) Theorem. Associating \[ L \longmapsto \mathcal {N} _ {L} = N _ {L | K} A _ {L} \] sets up a 1–1-correspondence between the finite abelian extensions \(L|K\) and the open subgroups \(\mathcal{N}\) of \(A_{K}\) . Furthermore, 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 corresponding to the subgroup N of \(A_{K}\) is called the class field associated with N. By (6.3), it satisfies \[ G (L | K) \cong A _ {K} / \mathcal {N}. \]

Proposition (7.1)

FC09-C04-U079 · Chapter IV, §7, source L13424 · in Mathlib

(7.1) Proposition. If \(1 \to A \to B \to C \to 1\) is an exact sequence of \(G\) -modules, then we obtain an exact hexagon \[ \begin{array}{c} H ^ {0} (G, A) \xrightarrow {f _ {1}} H ^ {0} (G, B) \\ \left. \begin{array}{c} f _ {6} \\ H ^ {- 1} (G, C) \end{array} \right. \xrightarrow {f _ {5}} H ^ {- 1} (G, B) \xleftarrow {f _ {4}} H ^ {- 1} (G, A) \xleftarrow {f _ {3}} H ^ {0} (G, C) \end{array} \]

Formalized. Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::TateCohomology.δ, lemma exact₃, lemma exact₁ — Mathlib constructs the connecting map and proves the long exact Tate sequence for every short exact sequence of representations. Taking the six consecutive terms in degrees −1 and 0 gives Neukirch’s exact hexagon.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (7.2)

FC09-C04-U080 · Chapter IV, §7, source L13434 · in another Lean project

(7.2) Definition. The Herbrand quotient of the \(G\) -module \(A\) is defined to be \[ h (G, A) = \frac {\# H ^ {0} (G , A)}{\# H ^ {- 1} (G , A)}, \] provided that both orders are finite.

Formalized. kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Defs.lean::def herbrandQuotient — The workshop definition Representation.herbrandQuotient is literally Nat.card TateH0 / Nat.card TateHNeg1; under Neukirch’s finiteness hypothesis this is exactly #H⁰/#H⁻¹.

Searched: R=ccc3323c6750abca25b49b35106f54eb3a398509 (Mathlib pin 26245e682c354e86f2a4a300812fe4673ae107dc, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (7.3)

FC09-C04-U081 · Chapter IV, §7, source L13444 · in another Lean project

(7.3) Proposition. If \(1 \to A \to B \to C \to 1\) is an exact sequence of \(G\) -modules, then one has \[ h (G, B) = h (G, A) h (G, C) \] in the sense that, whenever two of these quotients are defined, so is the third and the identity holds. For a finite \(G\) -module \(A\) , one has \(h(G, A) = 1\) .

Formalized. kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/SES.lean::herbrandQuotient_eq_of_shortExact; kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Finite.lean::herbrandQuotient_of_finite — herbrandQuotient_eq_of_shortExact proves multiplicativity for a short exact sequence whenever the three quotients are defined/nonzero, with companion lemmas proving the third is defined when two are; herbrandQuotient_of_finite gives value 1 for finite modules.

Searched: R=ccc3323c6750abca25b49b35106f54eb3a398509 (Mathlib pin 26245e682c354e86f2a4a300812fe4673ae107dc, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C04-U082 · Chapter IV, §7, source L13474 · in Mathlib

If G is an arbitrary group and g a subgroup, then to any g-module B, we may associate the so-called induced G-module \[ A = \operatorname{Ind} _ {G} ^ {g} (B). \] It consists of all functions \(f: G \to B\) such that \(f(x\tau) = f(x)^{\tau}\) for all \(\tau \in g\) . The operation of \(\sigma \in G\) is given by \[ f ^ {\sigma} (x) = f (\sigma x). \] If \(g = \{1\}\) , we write \(\operatorname{Ind}_G(B)\) instead of \(\operatorname{Ind}_G^g (B)\) . We have a canonical \(g\) -homomorphism \[ \pi : \operatorname{Ind} _ {G} ^ {g} (B) \longrightarrow B, \quad f \longmapsto f (1), \] which maps the \(g\) -submodule \[ B ^ {\prime} = \left\{f \in \operatorname{Ind} _ {G} ^ {g} (B) \mid f (x) = 1 \text { for } x \notin g \right\} \] isomorphically onto \(B\) . We identify \(B'\) with \(B\) . If \(g\) is of finite index, we find \[ \operatorname{Ind}_{G}^{g}(B) = \prod_{\sigma \in G/g} B^{\sigma}, \] where \(\sigma\) runs over a system of left coset representatives.

Formalized. Mathlib/RepresentationTheory/Coinduced.lean::def coindV, def coind, def resCoindHomEquiv — Neukirch’s all-functions model is the modern coinduced module: coindV consists of equivariant functions on the ambient group and coind acts by translation. Inverting the argument converts Mathlib’s left-covariance convention to Neukirch’s right-covariance convention; resCoindHomEquiv is the evaluation-at-1 adjunction and yields the displayed canonical subgroup/evaluation identification.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (7.4)

FC09-C04-U083 · Chapter IV, §7, source L13516 · in another Lean project

(7.4) Proposition. Let \(G\) be a finite cyclic group, \(g\) a subgroup and \(B\) a \(g\) -module. Then we have canonically \[ H ^ {i} \big (G, \operatorname{Ind} _ {G} ^ {g} (B) \big) \cong H ^ {i} (g, B) \quad f o r \quad i = 0, - 1. \]

Formalized. kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509/ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::def periodicTateCohomology; Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean::def coindIso; Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::isoGroupCohomology; Mathlib/RepresentationTheory/Coinduced.lean::def coindV — For a finite cyclic group, external 2-periodicity identifies Tate H⁰ with ordinary H² and Tate H⁻¹ with ordinary H¹. Pinned Shapiro for the same coinduced function-space model gives the subgroup isomorphisms in degrees 2 and 1, hence exactly Neukirch’s i=0,−1 statement.

Searched: R=ccc3323c6750abca25b49b35106f54eb3a398509 (Mathlib pin 26245e682c354e86f2a4a300812fe4673ae107dc, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d