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

FC10 — Serre, Local Fields.

This chapter contains 2 theorems, 4 propositions, 3 lemmas, 2 corollaries and 2 conventions.

Of the 13 statements checked against Lean, 0 are formalized somewhere and 13 are not.

Status	Statements	Share	What it means
not formalized	13	100%	A documented search found no Lean statement of it anywhere.
checked in total	13

Which versions of Lean and Mathlib were searched

• Canonical source block: FC10 Serre Chapter 12, “Brauer Group of a Local Field”, FC10-C12-U001–FC10-C12-U013, 13 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 C12: mathlib 0, project-existing 0, package-import 0, reference-port 0, unmatched 13.

Theorem 1

FC10-C12-U001 · Chapter XII, source L6522 · after FC10-C10-U022 · not formalized

Theorem1. Suppose that the residue feld \(\pmb { \mathrm { R } }\) is perfect. Then each element of the Brauer group \(\mathbf { B _ { K } }\) f \(\kappa\) is split by a finiteunramified extension of \(\mathbf { \delta K }\)

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Corollary: Corollary.The Brauer group of \(\mathbf { K }\) may be identified with…

FC10-C12-U002 · Chapter XII, source L6528 · after FC10-C10-U020, FC10-C10-U022, FC10-C12-U001 · not formalized

Corollary.The Brauer group of \(\mathbf { K }\) may be identified with \(\mathbb { H } ^ { 2 } ( \mathbb { K } _ { n \times \ell } / \mathbb { K } ) .\)

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Proposition 1

FC10-C12-U003 · Chapter XII, source L6572-L6576 · not formalized

Proposition 1 a)Forall \(x \in \mathbb { K } ^ { * }\) \(w ( x ) = \{ n / d \} v \{ x \} .\) b) \(w \{ x + y \} \geq \operatorname { I n f } ( w \{ x \} , w \{ y \} )\) ,and \(\mathbb { w } ( \mathbb { x } y \} = \mathbb { w } ( x ) + \mathbb { w } ( y ) .\) （24号 c) Let a be any real number strictly between O and 1. Setting \(\| x _ { 1 } ^ { \dag } \{ _ { \mathrm { D } } = a ^ { \mathrm { w } \{ x \} }\) givesa norm on D;the topology defined by this norm is the product topology (identifyingDwith \(\mathbb { K } ^ { \ast } ]\) d） For an element \(\boldsymbol { x } \in \mathbf { D }\) to be integral over A,it is necessary and suffcient that \(w \{ x \} \ b e \ge 0\) ThesetBof such elements isa subringofD.

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Lemma 1

FC10-C12-U004 · Chapter XII, source L6580 · not formalized

Lemma 1. Suppose \(\bar { \bf K }\) is perfect and \(n \geq 2\) Then there is a commutative subfieldLofD,containing K,that is unramified overK and distinct from K.

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Proposition 2

FC10-C12-U005 · Chapter XII, source L6596 · not formalized

Proposition 2. Suppose \(\pmb { \mathrm { R } }\) is perfect.Then there is a maximal subfeld of D that isunramified overK.

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Convention / notation

FC10-C12-U006 · Chapter XII, source L6620 · after FC10-C04-U015 · not formalized

Asin Chap.IV,denote by \(\mathbf { U } _ { \mathbf { L } } ^ { n }\) the subgroup of \(\mathbf { U _ { L } }\) consisting of those \(a \in \mathrm { { U } _ { k } ^ { \frac { q } { k } } }\) such that \(v _ { \{ 1 \} } ^ { i } - a \} \geq n .\)

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Lemma 2

FC10-C12-U007 · Chapter XII, source L6622 · after FC10-C12-U006 · not formalized

Lemma 2. For all \(q \geq 1 , \mathrm { H } ^ { q } ( \mathfrak { g } , \mathrm { U } _ { 1 } ^ { 1 } ) = \mathfrak { g } .\)

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Lemma 3

FC10-C12-U008 · Chapter XII, source L6626 · not formalized

Lemma 3. Let \(\mathfrak { g }\) be a finite group, M a \(\mathfrak { g }\) modulefitered by a decreasing sequence \(\mathbf { M } _ { n }\) \(n \geq \ddagger\) ofsubmodules,with \(\mathbf { M _ { 1 } } = \mathbf { M }\) Suppose that Mis completeHausdorff in the topology defined by the \(\mathbf { M } _ { n }\) Fix an integer \(q \geq 0 .\) \(\mathrm { H } ^ { q } ( \mathfrak { g } , \mathbf { M } _ { n } / \mathbf { M } _ { n + 1 } ) = 0\) for all \(n \geq \frac { 4 } { 2 }\) ,then \({ \bf H } ^ { q } ( { \mathfrak { g } } , { \bf M } ) = 0 .\)

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Proposition 3

FC10-C12-U009 · Chapter XII, source L6674 · after FC10-C12-U002 · not formalized

Proposition 3. The group \(\mathtt { B _ { K } }\) is the union of the subgroups \(\mathbf { H } ^ { 2 } ( \mathbf { L } / \mathbf { K } )\) asL runs through the family of finite unramified Galois extensions ofK.

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Proposition 4

FC10-C12-U010 · Chapter XII, source L6692-L6696 · after FC10-C12-U009 · not formalized

Proposition 4. Let \(L / { \bf K }\) beafinite unramified Galois extension with Galois groupg.Then there is \(\pmb { a }\) split exact sequence \[ 0 \to \mathbb { H } ^ { q } ( \mathbb { L } / \mathbb { K } ) \to \mathbb { H } ^ { q } ( \mathbb { L } / \mathbb { K } ) \to \mathbb { H } ^ { q } ( { \mathfrak { g } } , \mathbb { Z } ) \to 0 , \qquad q \geq 1 . \]

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Corollary

FC10-C12-U011 · Chapter XII, source L6700-L6704 · after FC10-C12-U010 · not formalized

Corollary.Let \(\mathfrak { g }\) be the Galois group of \({ \sf K } _ { n r } / { \sf K }\) There is \(\pmb { a }\) split exact sequence \[ \begin{array} { r l r l r } { 0 \to \mathbb { H } ^ { q } ( } & { { } / \mathbb { K } ) \to \mathbb { H } ^ { q } ( \mathbb { K } _ { n r } / \mathbb { K } ) \to \mathbb { H } ^ { q } ( \mathfrak { g } , \mathbb { Z } ) \to 0 , } & { } & { q \geq 1 . } \end{array} \]

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Convention / notation

FC10-C12-U012 · Chapter XII, source L6720 · not formalized

For a profinite group \(\mathfrak g\), denote by \(X(\mathfrak g)=\operatorname{Hom}_{\mathrm{cont}}(\mathfrak g,\mathbf Q/\mathbf Z)\) its character group, equivalently the Pontryagin dual of \(\mathfrak g/\mathfrak g^{\prime}\).

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.

Theorem 2

FC10-C12-U013 · Chapter XII, source L6722-L6726 · after FC10-C12-U009, FC10-C12-U012 · not formalized

Theorem2.LetK bea fieldthatis completeunder \(\pmb { a }\) discrete valuation and hasperfectresidue fieldR.Let \(\mathfrak { g }\) be the Galois group of the algebraic closure f \(\pmb { \mathrm { R } }\) over \(\pmb { \mathrm { R } }\) and let \(\mathbf { X } ( { \mathfrak { g } } )\) be its character group.Then there is a split exact sequence \[ 0 \to { \bf B } _ { \overrightarrow { \bf K } } \to { \bf B } _ { \overrightarrow { \bf K } } \to { \bf X } ( { \bf g } ) \to 0 . \]

Not formalized. No checked source-complete local Brauer-group classification/invariant theorem was found; Mathlib currently has Brauer definitions but not the local-field structure theorem.