FC10 — Jean-Pierre Serre, Local Fields (1979)

FC10 — Serre, Local Fields.

This chapter contains 14 definitions, 2 theorems, 6 propositions, 4 lemmas, 1 corollary, 2 examples, 4 conventions and 6 other statements.

Of the 39 statements checked against Lean, 4 are formalized somewhere and 35 are not.

Status	Statements	Share	What it means
not formalized	35	90%	A documented search found no Lean statement of it anywhere.
in another Lean project	4	10%	Some other Lean development has it; using it means porting that code.
checked in total	39

Which versions of Lean and Mathlib were searched

• Canonical source block: FC10 Serre Chapter 11, “Class Formations”, FC10-C11-U001–FC10-C11-U039, 39 units, in exact canonical order from Foundational corpus units FC10 Serre Local Fields.
• Project code baseline: A=3b2239e161592472b34e02ad3b7da308f9ce7280. The live repository moved only documentation/coordination files after A during this audit; no Lean source changed, so A is the semantic project baseline.
• Pinned Mathlib: P=db584cd6d46c92f209a44c0f1c829460d327499d; current Mathlib checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Strict bundle semantics were used: partial ingredients never earn a route.
• External CFT reference where cited: ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0). Open Mathlib class-formation reference where cited: PR #42687 at a40561e249ebf45d2870f5d9d45bc2eb4d80b242 (Apache-2.0).
• Current Mathlib still marks higher ramification groups in lower numbering as TODO. Open/current local class-field-theory work does not supply a finished reciprocity/existence layer; unresolved/sorry-tainted downstream claims were not credited.
• Route totals for C11: mathlib 0, project-existing 0, package-import 0, reference-port 4, unmatched 35.

Definition / construction

FC10-C11-U001 · Chapter XI, source L5916-L5920 · not formalized

The family \(\{G_E\}_{E\in X}\) of finite-index subgroups is required to be closed under finite intersections, to contain every overgroup of one of its members, and to be stable under conjugation in \(G\).

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Example / comparison

FC10-C11-U002 · Chapter XI, source L5922 · not formalized

ExAMPLEs.1.LetE bea field, \(\pmb { \Omega }\) a Galois extension ofE,and let \(\mathbf { X }\) be the set of subfields of \(\pmb { \Omega }\) that are finite extensions ofE.Take \(\mathbf { G }\) to be the Galois topological group \(\mathbf { G } ( \Omega / \mathbb { E } ) .\) and for \(\mathbf { G } _ { \mathbf { \overline { { F } } } }\) take the subgroup \(\mathbf { G } \{ \Omega / \Gamma \}\) Then properties a),b), c) are a consequence of Galois theory.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U003 · Chapter XI, source L5882 · after FC10-C11-U001 · not formalized

For \(\textbf { G }\) and \(\{ \mathbf { G } _ { \Xi } \} _ { \Xi \in \mathbf { X } }\) satisfying the above conditions, we willtransfer to X the terminology of Galois theory.The elements of \(\mathbf { x }\) will be called“fields” We write \({ \mathfrak { E } } \subset { \mathfrak { F } }\) if \(G _ { \Xi } \supset G _ { \mathfrak { F } }\) we say \(\mathbf { \ddot { F / E } }\) isa Galois extension”if \(\mathbf { G } _ { \mathfrak { F } }\) is a normal subgroup of \(\mathbb { G } _ { \mathtt { E } }\) ,and we call the quotient group \(\mathbf { G } _ { \mathbf { E } } / \mathbf { G } _ { \mathbf { F } }\) (also denoted \(G _ { f ^ { \prime } f ^ { \prime } } )\) “the Galois group \(G \{ \mathbf { F } / \mathbf { E } \} ^ { \prime \prime }\) In the situation of condition a),we call \(\mathbf { F }\)”the composite” of the \(\boldsymbol { \mathsf { F } } _ { i }\) ,and write \(\mathbf { F } = \prod \mathbf { F } _ { i }\) in the situation of c),we write \(F ^ { r } = s ( F )\) or simply \(\pmb { s F }\) It makes sense to speak of “abelian extensions, solvable extensions”,etc.Note that every extension \(\mathbf { F } / \mathbf { E }\) is contained in a Galois extension:namely,since \(\mathbf { G } _ { \mathtt { F } }\) has finite index in \(\mathbf { G _ { E } }\) it only has finitely many conjugates \(s . \mathbb { G } _ { F } . s ^ { - 1 }\) and their intersection has the form \(\mathbf { G } _ { \mathtt { F } ^ { \prime } }\) ,with \(F ^ { \prime } \in X\) ; then \(\mathbf { \vec { F } ^ { \prime } } / \mathbf { \vec { E } }\) is Galois and contains \(\mathbf { F }\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U004 · Chapter XI, source L5890 · after FC10-C11-U001, FC10-C11-U003 · in another Lean project

A formation is a system \((G,\{G_E\}_{E\in X},A)\) satisfying the stated field-indexing axioms and the stabilizer condition; write \(A_E=A^{G_E}=H^0(G_E,A)\).

Formalized. Mathlib/NumberTheory/CFT/ClassFormation/Basic.lean::CategoryTheory.Formation — The open CFT work gives the modern Galois-category/sheaf formulation of Serre’s formation data and stabilizer-fixed sections.

Searched: OCF=a40561e249ebf45d2870f5d9d45bc2eb4d80b242 (open Mathlib PR #42687, Apache-2.0)

Convention / notation

FC10-C11-U005 · Chapter XI, source L5898 · after FC10-C11-U004 · not formalized

For a Galois extension \(F/E\) in a formation, write \(H^q(F/E)\), \(H_q(F/E)\), and \(\widehat H^n(F/E)\) for the cohomology, homology, and Tate cohomology of \(G(F/E)\) with coefficients in \(A_F\).

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U006 · Chapter XI, source L5906 · after FC10-C11-U005 · in another Lean project

For \(F^{\prime}\supset F\supset E\) with both relevant extensions Galois, the canonical map \(H^q(F/E)\to H^q(F^{\prime}/E)\) is called inflation.

Formalized. Mathlib/NumberTheory/CFT/ClassFormation/Basic.lean::Formation.inflation — The PR implements the canonical inflation morphism between the formation cohomology objects.

Searched: OCF=a40561e249ebf45d2870f5d9d45bc2eb4d80b242 (open Mathlib PR #42687, Apache-2.0)

Definition / construction

FC10-C11-U007 · Chapter XI, source L5944 · not formalized

iv)Suppose \(\mathbf { F } / \mathbf { E }\) is Galois,and let \(\mathfrak { s e G }\) The map \(t \mapsto s ^ { - 1 } t s\) is an isomorphism \({ \cal G } ( s \mathbf { F } / s \mathbf { E } ) { \cal G } ( \mathrm { F } j \mathbf { E } )\) .The map \(a \mapsto s , a\) is an isomorphism of \(\Lambda _ { F }\) with \(\mathbf { A } _ { \mathbf { s F } }\) These two maps are compatible, hence they define (by transport of structure) isomorphisms \[ s^{*} \colon \widehat{H}^{n}(F/E) \to \widehat{H}^{n}(sF/sE), \qquad n \in \mathbb{Z}. \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Axiom I

FC10-C11-U008 · Chapter XI, source L5962 · after FC10-C11-U005 · in another Lean project

AxiomI.For every Galois extension \({ \cal F } / { \cal E } , ~ { \cal H } ^ { 1 } ( { \bf F } / { \bf E } ) = \boldsymbol { \mathrm { 0 } } .\)

Formalized. Mathlib/NumberTheory/CFT/ClassFormation/Basic.lean::FieldFormation — FieldFormation imposes precisely the H¹-vanishing axiom at every finite Galois object.

Searched: OCF=a40561e249ebf45d2870f5d9d45bc2eb4d80b242 (open Mathlib PR #42687, Apache-2.0)

Axiom: Axiom I’. \(\mathbb { H } ^ { 1 } ( \mathbb { F } / \mathbb { E } ) = 0\) for…

FC10-C11-U009 · Chapter XI, source L5966 · after FC10-C11-U008 · not formalized

Axiom I’. \(\mathbb { H } ^ { 1 } ( \mathbb { F } / \mathbb { E } ) = 0\) for every cyclic extension of prime degree.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Convention / notation

FC10-C11-U010 · Chapter XI, source L5978-L5984 · after FC10-C11-U005 · not formalized

Before stating axiom II,we introduce the notation \(H ^ { q } f _ { \mathrm { ~ \mu ~ } } / \mathrm { E } )\) for the direct limit of the \(H ^ { q } ( F / E ) ,\) as \(\pmb { \ F }\) runs through the set of Galois extensions of E；if \(\mathbf { F } ^ { \prime } \supset \mathbf { F } \supset \mathbf { E }\) thehomomorphisms \[ \mathrm { H } ^ { q } ( \mathrm { F / E } ) \mathrm { H } ^ { q } \{ \mathrm { F / E } \} \] in this directed system are the inflation homomorphisms (cf. \(\ S \Im\) .For \(q = 2\) these homomorphisms are injective: that follows from axiom Iand prop.5 of Chap.VII, \(\ S 6 .\) The group \(\tilde { \mathbf { H } } ^ { 2 } \{ \quad / \mathbf { E } \}\) is therefore the union of the \(H ^ { 2 } \{ \Gamma / \ E \}\) ,so the situation is entirely analogous to that of the Brauer group.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Axiom

FC10-C11-U011 · Chapter XI, source L5988-L5996 · after FC10-C11-U010 · in another Lean project

Axiom II a）The homomorphism \(\dot { \bar { \mathfrak { s m } } } \mathfrak { v } _ { \mathfrak { E } }\) is injective,and maps \(\mathbb { H } ^ { 2 } \{ \mathbb { F } / \mathbb { E } \}\) onto the unique subgroup of \(\mathbf { Q } / \mathbf { Z }\) of order equal to [F:E]. b) For any extension \(\mathbf { E } ^ { \prime } / \mathbf { E } ,\) we have \[ \operatorname* { i n v } _ { \mathtt { E ^ { \star } } } \circ \mathbb { R e s } _ { \mathtt { E / E ^ { \star } } } = [ \mathtt { E ^ { \prime } } ; \mathtt { E } ] \cdot \operatorname* { i n v } _ { \mathtt { E } } , \]

Formalized. Mathlib/NumberTheory/CFT/ClassFormation/Basic.lean::ClassFormation — ClassFormation packages a compatible fundamental H² class of exact order [F:E], the finite-level formulation of Serre’s invariant axiom. Reciprocity/corestriction are not credited downstream.

Searched: OCF=a40561e249ebf45d2870f5d9d45bc2eb4d80b242 (open Mathlib PR #42687, Apache-2.0)

Proposition 1

FC10-C11-U012 · Chapter XI, source L5998-L6020 · not formalized

Proposition 1 i）For every extension \(\mathbf { { \vec { E } } } / \mathbf { { \vec { E } } }\) thehomomorphism \[ \begin{array} { r l } { \operatorname { \mathbb { R e s } } _ { \operatorname { E / E } ^ { \cdot } } : \operatorname { \mathbf { H } } ^ { 2 } \left\{ \mathrm { ~ ~ \omega ~ } / \operatorname { \mathbb { E } } \right\} \to \operatorname { \mathbf { H } } ^ { 2 } \left( \mathrm { ~ ~ \omega ~ } / \operatorname { E } ^ { \prime } \right) } \end{array} \] is surjective. ii） For every extension \(\mathbf { E } ^ { \prime } / \mathbf { E } ,\) the homomorphism \[ { \mathrm { C o r } } _ { { \mathrm { E } } ^ { \prime } / { \boldsymbol { \Sigma } } } : { \mathrm { H } } ^ { 2 } \{ \quad / { \boldsymbol { \Sigma } } ^ { \prime } \} \to { \mathrm { H } } ^ { 2 } ( \quad / { \boldsymbol { \Sigma } } ) \] is injective, and \(\mathbf { i n v _ { E } } \circ \mathbf { C o r _ { E ^ { \prime } / E } } = \mathbf { i n v _ { E } } ,\) ii For every \(\mathfrak { s } \in \mathbf { G } .\) if \(s ^ { * }\) denotes the isomorphism \(\begin{array} { r l } { \mathbf { H } ^ { 2 } \big ( } & { { } / \mathbf { E } \big ) \mathbf { H } ^ { 2 } \big ( } \end{array}\) /s defined bypassing tothe limit the homomorphisms of \(\ S 1\) ,then \[ \begin{array} { r } { \operatorname* { i n v } _ { s \mathbf { E } } \circ s ^ { * } = \operatorname* { i n v } _ { \mathbf { E } } . } \end{array} \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Convention / notation

FC10-C11-U013 · Chapter XI, source L6056 · after FC10-C11-U004, FC10-C11-U011 · not formalized

For a Galois extension \(F/E\), write \(G_{F/E}^{a}=G_{F/E}/G_{F/E}^{\prime}\) for the abelianization; under class-formation duality it is identified with \(A_E/N_{F/E}A_F\).

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U014 · Chapter XI, source L6074 · after FC10-C11-U013 · not formalized

The inverse of \(\theta:G_{F/E}^{a}\to A_E/N_{F/E}A_F\) is the reciprocity isomorphism, written \(a\mapsto\{a,F/E\}\).

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Proposition 2

FC10-C11-U015 · Chapter XI, source L6082-L6086 · not formalized

Proposition 2. Let \(\chi \in \operatorname { H o m } ( \mathbf { G } _ { \mathbb { F } / \Xi } , \mathbf { Q } / \mathbf { Z } )\) beacharacter of degree 1 of the group \(\mathbf { G } _ { \mathbf { F } / \mathbf { E } }\) (or,what amounts to the same thing,of the group \(\mathbf { G } _ { \mathbb { F } / \mathbb { E } } ^ { \sigma } )\) .For any \(\beta \in \mathbb { G } _ { \mathbb { F } / \mathbb { E } } ^ { a }\) ,put \[ \langle \chi , s \rangle = \chi ( s ) \in \mathbf { Q } / \mathbf { Z } . \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Theorem 1

FC10-C11-U016 · Chapter XI, source L6120-L6124 · not formalized

Theorem 1. For every Galois extension \(\mathbf { F } / \mathbf { E }\) and every integer \(n _ { s }\) the homomorphism \[ \theta ^ { n } ( \mathrm { F } / \mathrm { E } ) : \hat { \mathrm { H } } ^ { n } ( \mathrm { G } _ { \mathrm { F } / \mathrm { E } } , \mathrm { Z } ) \hat { \mathrm { H } } ^ { n + 2 } ( \mathrm { G } _ { \mathrm { F } / \mathrm { E } } , \mathrm { A } _ { \mathrm { F } } ) = \hat { \mathrm { H } } ^ { n + 2 } ( \mathrm { F } / \mathrm { E } ) \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U017 · Chapter XI, source L6200 · after FC10-C11-U014 · not formalized

Thecommutativity ofdiagram(4)allows us to pass to the limit over increasing extensions \(\hbar / \operatorname { E }\) ,where E remains fixed.More precisely,define \(\Im \{ \mathrm { f } \} \mathrm { E } \}\) to be the projective limit of the \(\mathbb { G } _ { \mathbb { F } / \mathbb { E } } ^ { a }\) as \(\pmb { \ F }\) runs through the directed set of Galois extensions of E. In the case of the actual Galois theory, \(\mathfrak { A } \{ \mathbf { E } \}\) is the Galois topological group of the maximal abelian extension of the field E.If \(a \in \mathsf { A } _ { \mathbb { E } }\) the commutativity of diagram (4) shows that the \(\{ a , \ F / \operatorname { E } \}\) are coherent,and therefore define an element of \(\mathfrak { A } ( \mathbb { E } )\) to be denoted \(\{ a , \mathbf { \nabla } ^ { * } / \mathbf { E } \}\) In this way we obtain acanonical homomorphism \[ A_{E} \to \mathfrak{A}(E). \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U018 · Chapter XI, source L6240-L6246 · after FC10-C11-U014 · not formalized

One consequence of this proposition is that the norm groups define a topology on \(\mathbf { A } _ { \mathbf { E } }\) Denoting by \(\hat { \bf A } _ { \bf E }\) the Hausdorff completion of \(\mathbf { A } _ { \mathbf { E } }\) in this topology,we have (bydefinition) \[ \hat { \mathsf { A } } _ { \mathrm { E } } = \mathrm { \operatorname* { l i m } { A } _ { \mathrm { E } } / \mathrm { I } \quad ( \mathrm { I ~ r u n n i n g ~ t h r o u g h ~ t h e ~ n o r m ~ g r o u p s ) } } \] and the symbol \(\{ a , { \bar { \star } } / { \mathrm { E } } \}\) defines an isomorphism of \(\hat { \bf A } _ { \bf E }\) with the topological group \(\Im \{ E \}\) of \(\ S 3\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U019 · Chapter XI, source L6248 · after FC10-C11-U018 · not formalized

The topology just defined on \(\mathbf { A } _ { \mathbf { E } }\) is sometimes caled the“norm” topology, to distinguish it from the one which occurs in the existence theorem.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Axiom: Axiom II-1.For every extension \(\mathbb { F } / \mathbb { E } ,\) thenorm…

FC10-C11-U020 · Chapter XI, source L6256-L6260 · not formalized

Axiom II-1.For every extension \(\mathbb { F } / \mathbb { E } ,\) thenorm homomorphism \[ N _ { \mathtt { F } / \mathtt { E } } : \mathbb { A } _ { \mathtt { F } } \to \mathbb { A } _ { \mathtt { E } } \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U021 · Chapter XI, source L6268-L6274 · after FC10-C11-U004 · not formalized

For an extension \(E^{\prime}/E\) in a formation, the transfer construction defines a norm homomorphism \(N_{E^{\prime}/E}:A_{E^{\prime}}\to A_E\); in the Galois case this agrees with the usual norm.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition: Definition

FC10-C11-U022 · Chapter XI, source L6276 · after FC10-C11-U021 · not formalized

Definition. \(A\) subgroup lof \(\mathbf { A } _ { \ E }\) is called a norm group \(i f\) there exists an extension \(\mathbf { E } ^ { \prime } { \mathbb { E } }\) such that \(\begin{array} { r } { \tilde { \mathbf { I } } = \mathbb { N } _ { \mathbf { E } ^ { \prime } / \mathbf { E } } \{ \mathbf { A } _ { \mathbf { E } ^ { \prime } } \} } \end{array}\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Proposition 3

FC10-C11-U023 · Chapter XI, source L6286-L6290 · after FC10-C11-U021 · not formalized

Proposition 3. Let \(\mathbf { E } ^ { \prime } / \mathbf { E }\) be any extension,and let \(\mathbf { E ^ { \prime \prime } }\) be the largest abelian extension ofE contained in \(\mathbf { E ^ { \prime } }\) Then \[ \ N _ { \mathbb { E } ^ { \prime } ; \mathbb { E } } ( \mathbf { A } _ { \mathrm { E } ^ { \prime } } ) = \mathrm { N } _ { \mathbb { E } ^ { \prime \prime } ; \mathbb { E } } ( \mathbf { A } _ { \mathrm { E } ^ { \prime \prime } } ) . \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Corollary: Corollary

FC10-C11-U024 · Chapter XI, source L6308 · after FC10-C11-U022 · not formalized

Corollary. The norm group \(\mathbf { N } _ { \mathbf { E } ^ { \prime } ; \mathbf { E } } \mathbf { A } _ { \mathbf { E } ^ { \prime } }\) has finite index in \(\mathbf { A } _ { \mathbf { E } }\) ;this index divides \([ \mathbf { E } : \mathbf { E } ] ,\) and is equal to it \(i f\) and onlyif \(\mathbf { E ^ { \prime } }\) is an abelian extension of E.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Proposition 4

FC10-C11-U025 · Chapter XI, source L6318 · not formalized

Proposition 4.The map \(\vec { \mathbf { F } } \mathbf { \check { \mathbf { t } _ { \mathbf { F } } } }\) isa bijection of the set of abelian extensions ofE onto the set of norm groups of \(\mathbf { A } _ { \Eup }\) ;this correspondence reverses inclusion . The universal norm group of \(E\), denoted \(D_{E}\), is the intersection of all the norm groups of \(A_{E}\).

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition: Definition

FC10-C11-U026 · Chapter XI, source L6320 · after FC10-C11-U022 · not formalized

Definition. The universal norm group of E(denoted \(\pmb { \mathrm { D } } _ { \pmb { \mathrm { E } } }\) isthe intersection of all the norm groups of \(\mathbf { A } _ { \mathbf { E } }\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Proposition 5

FC10-C11-U027 · Chapter XI, source L6324 · not formalized

Proposition 5. For every extension \(\mathbf { F } / \mathbf { E }\) we have \(\Nu _ { \tt F _ { \it f E } } \mathrm { D } _ { \tt F } = \tt D _ { \tt E }\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Axiom

FC10-C11-U028 · Chapter XI, source L6334-L6336 · not formalized

Axiom IIl-2.For every prime number \(p\) there exists a field \(\widehat { \Sigma } _ { \mathfrak { p } }\) such that, for \(\mathbf { E } \ni \mathbf { E } _ { \mathfrak { p } }\) themap \({ \mathfrak { G } } _ { p } : { \mathfrak { X } } \mapsto { \mathfrak { P } } . { \mathfrak { X } }\) qf \(\mathsf { A } _ { \mathbb { E } }\) into itself satisfies the condition: i） The kernel of \(\phi _ { p }\) is compact,and its image contains \(\mathbf { D _ { \widehat { E } } }\) [This is the only axiom whose verification is difficult in practice.]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Proposition 6

FC10-C11-U029 · Chapter XI, source L6338 · after FC10-C11-U026 · not formalized

Proposition 6.For every fieldE,the group \(\mathfrak { D } _ { \mathtt { F } }\) is divisibleand equal to \(\bigcap \mu _ { i } A _ { E }\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Axiom III-3

FC10-C11-U030 · Chapter XI, source L6342 · not formalized

AxiomIIl-3.There exists a compact subgroup \(\mathbf { U _ { E } }\) f \(\mathbf { A } _ { \mathbf { E } }\) such that every closed subgroupof finite index in \(\mathbf { A _ { E } }\) that contains \(\theta _ { \textup { \bf F } }\) is \(\pmb { \mathcal { L } }\) norm group.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Theorem 2

FC10-C11-U031 · Chapter XI, source L6344 · after FC10-C11-U018, FC10-C11-U020, FC10-C11-U022, FC10-C11-U028, FC10-C11-U030 · not formalized

Theorem 2. Suppose axioms III-1,IIl-2, I-3 hold. For a subgroup of \(\mathbf { A } _ { \mathbf { E } }\) tobea norm group,itis necessary and sufficient that itbe closed and of finite index.

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Example / comparison

FC10-C11-U032 · Chapter XI, source L6362-L6366 · not formalized

ExAMPLe.In the case of local class field theory,we take \(\mathbf { A } _ { \mathbf { E } } = \mathbf { E } ^ { * }\) and we provide \(\mathbf { E } ^ { * }\) with the topology induced fromE,which makes it into a locally compact group.Axiom IIl- \(\textbf { \cdot } \mathbf { j }\) is trivial.In axiom Il-3, take \(\mathbf { U } _ { \mathcal { E } }\) to be the group of units;the exact sequence \[ 0 \to \mathrm { U } _ { \tt E } \to \mathbb { E } ^ { * } \to \mathbf { Z } \to 0 \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U033 · Chapter XI, source L6374 · not formalized

where \(\pmb { \hat { z } }\) denotes the completion of \(\mathbf { z }\) for the topology defined by the nZ (it is the product of the additive groups \(\mathbf { Z } _ { p }\) over all primes \(p ]\) .Wewill return to this in Chapter XIV, \(\ S 6\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Definition / construction

FC10-C11-U034 · Chapter XI, source L6410 · not formalized

and,for \(s \in G\) ,denote by \(\dot { \mathfrak { k } } _ { s }\) the element \(s \gets 1\) of 1.Then \(\{ \overline { { \hat { i } } } _ { s } \} _ { 0 } \in \hat { \mathrm { H } } ^ { - 1 } \{ \mathrm { G } , \mathfrak { i } \} ,\) \(\mathcal { \mathbf { L } } \mathfrak { e } \mathfrak { t } \ \overline { { s } } \in \hat { \mathbb { H } } ^ { - 2 } ( \mathbf { G } , \mathbf { Z } )\) be such that \(d \overline { { s } } = \{ \overline { { i } } _ { s } \} _ { 0 }\) .The map \(s \mapsto { \overline { { s } } }\) defines by passage to the quotient the canonical isomorphism of \(\mathbf { G } / \mathbf { G } ^ { \prime }\) onto \(\hat { \mathbf { H } } ^ { - z } \{ \mathbf { G } , \mathbf { \mathcal { Z } } \}\) (cf Chap. Vil, \(\ S 4 _ { , }\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Lemma 3

FC10-C11-U035 · Chapter XI, source L6412-L6416 · not formalized

Lemma 3.Let B be a G-module and \(f : \mathbf { G } \mathbf { B }\) a 1-cocycle, \(\vec { f } \in \mathbb { H } ^ { \mathfrak { i } } \{ \mathbb { G } , \mathfrak { B } \}\) its cohomology classThen for every \(\bar { s } \in G\) \[ \overline { { { s } } } . \overline { { { f } } } = \overline { { { f ( s ) } } } _ { 0 } i n \widehat { \bf H } ^ { - 1 } ( { \bf G } , \ B ) . \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Convention / notation

FC10-C11-U036 · Chapter XI, source L6442 · not formalized

Notation. G denotes a finite group, and A, B,.. are G-modules. If a is an element of A fixed by \(\mathbf { G }\) (resp. such that \(\mathbb { N } a = \mathbb { 0 } )\) ,denote by \(\overline { { a } } ^ { 0 }\) (resp. \(\vec { a } _ { 0 } \}\) its canonical image in \(\hat { \mathbf { H } } ^ { 0 } \mathbf { ( G , \bar { A } ) }\) (resp. \(\hat { \mathbf { H } } ^ { - 1 } ( \mathbf { G } , \mathbf { A } )\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Lemma 1

FC10-C11-U037 · Chapter XI, source L6444-L6450 · not formalized

Lemma 1. Given \(\mathbf { G }\) modulesA,Band \(a \in \mathbf { A } ^ { \mathbf { G } } .\) let \(f _ { a } \colon \mathbf { Z } \to \mathbf { A }\) be the G-homomorphism such that \(f _ { a } ( 1 ) = a\) Let \(x \in { \hat { \mathbf { H } } } ^ { n } \{ \mathbf { G } , \mathbf { B } \} .\) Then the cup product \[ \overline { { { a } } } ^ { 0 } , x \in \hat { \mathbf { H } } ^ { n } ( \mathbf { G } , \mathbf { A } ) \otimes \mathbf { B } ) \] is equal to the image of \(x\) under the homomorphism \(f _ { a } \otimes \mathbf { i } : \mathbf { B } \mathbf { A } \otimes \mathbf { B }\)

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Lemma 2

FC10-C11-U038 · Chapter XI, source L6466 · after FC10-C07-U009, FC10-C11-U036 · not formalized

Lemma 2. Let \(a\in A\) satisfy \(Na=0\), and let \(f\) be a \(1\)-cocycle of \(G\) with values in \(B\), with cohomology class \(\bar f\in H^1(G,B)\). Then \(\bar a^{\,0}\cdot\bar f=\bar c^{\,0}\) in \(\widehat H^0(G,A\otimes B)\), where \(c=-\sum_{t\in G}ta\otimes f(t)\).

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.

Lemma 4

FC10-C11-U039 · Chapter XI, source L6482-L6486 · not formalized

Lemma 4. Let B be a G-module, \(u : { \bf G } \times { \bf G } { \bf B }\) a 2-cocycle, \(\overline { { u } } \in \mathbb { H } ^ { 2 } \{ \mathbf { G } , \mathbf { B } \}\) its cohomology class.Then forall \(\pmb { S } \in \pmb { G }\) \[ \overline { { s } } , \overline { { u } } = \overline { { a } } ^ { 0 } , w i t h a = \sum _ { t \in \mathbf { G } } u ( t , s ) . \]

Not formalized. Open class-formation work provides definitions and the finite-level axioms only; reciprocity, norm-group classification, and the existence axioms in this row remain unproved/incomplete.