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

FC10 — Serre, Local Fields.

This chapter contains 1 definition, 2 theorems, 6 propositions, 12 corollaries, 2 examples and 2 conventions.

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

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

Which versions of Lean and Mathlib were searched

• Canonical source block: FC10 Serre Chapter 15, “Ramification”, FC10-C15-U001–FC10-C15-U025, 25 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 C15: mathlib 0, project-existing 0, package-import 0, reference-port 0, unmatched 25.

Proposition 1

FC10-C15-U001 · Chapter XV, source L8066 · not formalized

Proposition 1.Let N be the kernel of \(\pmb { \mathrm { p } }\) in \(k _ { s }\) .1f \(x \in k ,\) let \(y \in k _ { s }\) be \(\pmb { a }\) solution to the equation \(\mathbb { P } \{ y \} = x ,\) and let \({ \pmb z } = { \pmb F } { \pmb y } - { \pmb y }\) Then \(z \in \mathbb { N }\) ,and the image \(\sharp\) of zin \(N / ( \mathrm { F } - 1 ) \mathrm { N }\) does not depend on the choice of \(y ; i f\) we set \(\delta _ { p } ( x ) = \Xi ,\) then the map \(\delta _ { \perp }\) defines by passage to the quotient an isomorphism of \(k / P ( k )\) onto \(\mathbf { N } / \{ \mathbf { F } - 1 \} \mathbf { N } .\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Proposition 2

FC10-C15-U002 · Chapter XV, source L8086 · not formalized

Proposition 2. Let \(\mathbf { P } = \mathbf { X } ^ { n }\) with \(n \geq 1\) and let \(\aleph\) be the kernel of \(\mathbb { P } : k _ { s } ^ { * } \to k _ { s } ^ { * }\) \(l f _ { \mathbf { \delta } } x \in k ,\) let \(y \in k _ { s } ^ { * }\) be a solution to the equation \(\mathbf { p } _ { \left\{ y \right\} } = { \boldsymbol { x } } ,\) and let \(z = y ^ { { \boldsymbol { \mathsf { F } } } - { \boldsymbol { \mathsf { 1 } } } }\) Then \(z \in \mathbb { N }\) and the image \(\widetilde { z }\) of \(\pmb { z }\) in \(\mathbb { N } / \mathbb { N } ^ { \ F - 1 }\) does not depend on the choice of \(y ; i f\) we put \(\delta _ { \mathbb { P } } ( x ) = { \overline { { z } } } ,\) then the map \(\delta _ { \mathsf { P } }\) definesby passage to the quotient an isomorphism of \(k ^ { * } / \mathbb { P } ( k ^ { * } )\) onto \(\mathbf { N } / \mathbf { N } ^ { \mathbf { F } - \mathbf { i } }\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Convention / notation

FC10-C15-U003 · Chapter XV, source L8088 · after FC10-C15-U002 · not formalized

(To keep the analogy with the additive case,we have used the exponential notation: \(y ^ { \mathbf { F } } = \operatorname { F } \{ y \} .\) 1

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 1

FC10-C15-U004 · Chapter XV, source L8092 · after FC10-C15-U002 · not formalized

Corollary1. If N is contained in \(k ^ { * }\) ,then the map \(\delta _ { \mathsf { P } }\) is an isomorphism of \(k ^ { \ast } / P ( k ^ { \ast } )\) onto N.

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 2

FC10-C15-U005 · Chapter XV, source L8094 · not formalized

Corollary 2. The order of \(k ^ { * } / \mathbf { P } ( k ^ { * } )\) is finite； it is \(\pmb { \alpha }\) divisor of the separable degree \(d _ { s } ( P )\) of \(\mathbf { P }\) andis equal to the latter \(i f\) and only if \(\aleph\) is contained in \(k ^ { * }\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 3

FC10-C15-U006 · Chapter XV, source L8096 · not formalized

Corollary 3.The kernel and cokernel of \(\pmb { \mathrm { P } } : \pmb { k } ^ { * } \pmb { k } ^ { * }\) are finite groups of the same order.

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Example / comparison

FC10-C15-U007 · Chapter XV, source L8100 · not formalized

ExAMPLE.Suppose \(\pmb { n }\) is prime to the characteristic of \(\mathbf { k }\) and assume that \(k ^ { * }\) contains the group \(\mu _ { n }\) of all nth roots of unity.Then \(\Nu _ { \ l } = \mu _ { \nparallel }\) and the isomorphism \(\delta _ { \mathrm { P } } : k ^ { * } / k ^ { * n } \to \mu _ { n }\) is the isomorphism \(\mathbf { P } _ { n }\) of Chap. XIV, \(\ S 3\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 1

FC10-C15-U008 · Chapter XV, source L8136 · not formalized

Corollary 1. 1f \(\pmb { \mathrm { N } }\) is contained in \(k ,\) the map \({ \delta } _ { \mathbf { p } }\) is an isomorphism of \(k / \mathbb { P } ( k )\) onto \(\aleph\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 2

FC10-C15-U009 · Chapter XV, source L8140 · not formalized

Corollary 2. The order of \(k / { \mathbb { P } } ( k )\) is finite;it isa divisorof the separable degree \(d _ { s } \{ \ P \}\) of \(\mathbf { P } .\) and isequal to the latter \(i f\) andonlyifNiscontained in \(k\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 3

FC10-C15-U010 · Chapter XV, source L8144 · not formalized

Corollary 3. The kernel and cokernel of \(\pmb { \operatorname { \pmb { P } } } : \pmb { k } \pmb { k }\) are finite groups of the same order.

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Example / comparison

FC10-C15-U011 · Chapter XV, source L8154 · not formalized

ExAMPLEs.1.Assume the characteristic is \(p \neq 0\) and take \(\mathfrak { P }\) to be the polynomial \(\wp ( \mathbf { X } ) = \mathbf { X } ^ { p } - \mathbf { X }\) Then \(\begin{array} { r } { \mathbb { N } = \mathbb { Z } / p \mathbb { Z } , } \end{array}\) and the isomorphism \(\delta _ { \mathfrak { p } } : k / _ { \mathfrak { p } } ( k ) \to\) \(Z / p Z\) is the isomorphism S of Chap.XIV, \(\ S 5\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Proposition 3

FC10-C15-U012 · Chapter XV, source L8192 · after FC10-C04-U015 · not formalized

Proposition 3. The group \(\mathrm { U } _ { \mathrm { K } } ^ { n } / \mathrm { U } _ { \mathrm { K } } ^ { n + 1 } \mathrm { N U } _ { \mathrm { L } } ^ { \psi ( n ) }\) is isomorphic to \(\mathrm { G } _ { \psi ( n ) } / \mathrm { G } _ { \psi ( n ) + \frac { 1 } { 2 } }\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 1

FC10-C15-U013 · Chapter XV, source L8196 · not formalized

Corollary 1. \(\{ \mathrm { U } _ { \mathbb { K } } ^ { \pi } : \mathrm { U } _ { \mathbb { K } } ^ { n + 1 } \mathrm { N U } _ { \mathbb { L } } ^ { \psi ( \pi ) } \} = \hbar _ { \pi }\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 2

FC10-C15-U014 · Chapter XV, source L8200-L8206 · after FC10-C05-U030 · not formalized

Corollary 2. The group \(\mathbb { N } \mathbb { U } _ { \mathrm { L } } ^ { \psi ( n ) }\) isa subgroup of finite index of \(\lim _ { \mathbf { K } } , ~ f f ~ v _ { n }\) denotes this index,then \(v _ { \mathfrak { r } } = \mathbf { 1 }\) forsufficiently large \(\pmb { \mathscr { n } }\) ; moreover, \(v _ { n }\) divides \(v _ { n + 1 } h _ { n }\) ,withequality takingplace ifand only \(i f\) thecanonical homomorphism \[ \mathrm { U } _ { \mathsf { K } } ^ { n + 1 } / \mathrm { N U } _ { \mathsf { L } } ^ { \psi ( n + 1 ) } \mathrm { U } _ { \mathsf { K } } ^ { n } / \mathrm { N U } _ { \mathsf { L } } ^ { \psi ( n ) } \] is injective.

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 3

FC10-C15-U015 · Chapter XV, source L8216 · not formalized

Corollary 3.The integer \(v _ { 0 } = \{ \mathrm { U _ { K } } ; \mathrm { N U _ { L } } \} = \{ \mathrm { K ^ { * } } ; \mathrm { N L ^ { * } } \}\) divides the product of the \(h _ { \eta }\) ，

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Theorem 1

FC10-C15-U016 · Chapter XV, source L8222-L8226 · after FC10-C04-U037, FC10-C13-U026 · not formalized

Theorem 1. SupposeG is abelian.Then: a) \(\mathrm { { G } } _ { m } = \mathrm { { G } } _ { m + 1 } \ i f \ \varphi ( m )\) is not an integer. b） \(v _ { n } = v _ { n + 1 } h _ { n }\) forall n. c) The canonical map of \(\mathbb { U } _ { \mathbb { K } } ^ { \pi } / \mathbb { N } \mathbb { U } _ { 1 , } ^ { \psi ( n ) }\) into \(\mathbb { K } ^ { \star _ { / \mathbb { N } \mathbb { L } ^ { \star } } }\) is injective.

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Proposition 4

FC10-C15-U017 · Chapter XV, source L8276 · after FC10-C15-U016 · not formalized

Proposition 4. \(\omega _ { n } ( \alpha ) = \delta _ { n } ( \alpha ^ { - 1 } )\) for all \(\alpha \in \mathbb { U } _ { \mathbb { K } } ^ { n } / \mathbb { U } _ { \mathbb { K } } ^ { n + 1 } \mathbb { N } \mathbb { U } _ { \downarrow } ^ { \psi ( n ) } .\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 1

FC10-C15-U018 · Chapter XV, source L8292 · after FC10-C15-U017 · not formalized

Corollary1. The groups \(\mathrm { U } _ { \mathbb { K } } ^ { \pi } / \mathrm { N U } _ { \mathbb { L } } ^ { \psi ( \pi ) }\) formadecreasing filtration of \(\mathbb { K } ^ { \ast } / \mathbb { N } \mathbb { L } ^ { \ast }\) \(W e\) have \(\mathbf { U } _ { \mathbf { K } } ^ { n } / \mathbf { N } \mathbf { U } _ { \mathbf { L } } ^ { \psi ( n ) } = 0\) ifand onlyif \(\mathbf { G } ^ { \pi } = \lbrace \mathbb { 1 } \rbrace\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 2

FC10-C15-U019 · Chapter XV, source L8296 · not formalized

Corollary 2. Let c be the largest integer for which \(\mathbf G _ { \epsilon } \neq \{ \mathfrak { f } \}\) and let \(f =\) \(\varphi \{ c \} + 1\) Then \(\mathrm { U } _ { \mathbb { k } } ^ { f } \subset \mathbb { N } \mathbb { L } ^ { * }\) ,and \(f\) is the least integer enjoying this property.

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Definition / construction

FC10-C15-U020 · Chapter XV, source L8298 · after FC10-C06-U025, FC10-C15-U016 · not formalized

[The ideal \(\mathfrak { p } _ { \mathrm { K } } ^ { f }\) is called the conductor of the extension \(L / \mathbb { K }\) ; when \(L / \hbar\) is the cyclic extension defined by a character \(\chi\) of degree 1 of \(\mathrm { G } ( \mathbb { K } _ { s } / \mathbb { K } )\) the corollary to prop.6 of Chap.VI shows that \({ \mathfrak { p } } _ { \bf k } ^ { f }\) coincides with the Artin conductor \(f ( \chi )\) of x]

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Corollary 3

FC10-C15-U021 · Chapter XV, source L8302 · after FC10-C13-U026, FC10-C15-U016 · not formalized

Corollary 3.The reciprocity map \(\omega : \mathbb { K } ^ { * } / \mathbb { N } ^ { * } \to \mathbb { G }\) transforms the filtration \(b y\) the \(\mathrm { U } _ { \mathbb { K } } ^ { n } / \mathrm { N } \mathrm { U } _ { \mathbb { L } } ^ { \psi ( n ) }\) intothefiltration by the \(\mathbf { G } ^ { n }\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Theorem 2

FC10-C15-U022 · Chapter XV, source L8316 · after FC10-C15-U021 · not formalized

Theorem 2. Let \(L / \mathbb { K }\) be an abelian extension,with Galois group G.Then the image of \(\mathrm { U } _ { \mathrm { K } } ^ { n }\) under the reciprocity map \(\omega \colon \mathbb { K } ^ { * } \to \mathbb { G }\) is dense in \(\mathbf { G } ^ { \mathfrak { n } }\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Proposition 5

FC10-C15-U023 · Chapter XV, source L8334-L8338 · not formalized

Proposition 5. Let \(L / K\) be a cyclic totally ramified extension of prime degree \(p\) equaltothecharacteristic of \(\bar { \bf K }\) ;letG be its Galois group,and let sbea generator ofG;lett be the largest integer forwhich \(\mathbf { G } _ { \ell } \neq \{ 1 \}\) Let \(\pmb { \pi }\) uniformize \(\pmb { \downarrow }\) and set \(\mathbf { M } = s \{ \pi \} / \pi - 1\) Let \(x \in \mathrm { { U } } _ { \mathbf { K } } ^ { t }\) ,and let \(c ( \boldsymbol { x } ) = ( \boldsymbol { x } - 1 ) / \mathrm { T r } ( \mathrm { M } )\) Then \(c ( x )\) belongs to the valuation ring of \(\mathbf { K }\) ,andif(x) denotes its image in \(\vec { \bf K }\) we have \[ \{ x , \mathbf { L } / \mathbf { K } \} = s ^ { \mathrm { { S } ( \varepsilon ( x ) ) } } . \]

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Proposition 6

FC10-C15-U024 · Chapter XV, source L8352-L8356 · not formalized

Proposition 6. Suppose that K (resp. \(\bar { \bf K }\) ）has_characteristic zero (resp. \(p !\) ,and that \(\kappa\) contains the group \(\mu _ { p }\) of all pthrootsofunity.Let w bea generator of \(\mu _ { p }\) Let \(e = v _ { \mathrm { K } } ( p )\) bethe absolute ramification index of \(\mathbf { \check { x } }\) and let \(t \cong e p / ( p \sim 1 ) ,\) which isan integer.If \(\alpha \in \mathbb { K } ^ { * }\) and \(\pmb { b } \in \mathbf { U } _ { \mathbf { K } } ^ { \pmb { \imath } }\) then \[ ( a , b ) _ { v } = w ^ { v _ { K } ( a ) . m ( b ) } , w i t h m ( b ) = \mathrm { S } \bigg ( \frac { b - 1 } { p ( w - 1 ) } \bigg ) . \]

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.

Convention / notation

FC10-C15-U025 · Chapter XV, source L8358 · not formalized

[We write \(\mathbb { S } ( c )\) instead of \(\mathbb { S } ( \overline { { c } } )\) if \(c \in \mathsf { A } _ { \mathbf { K } } . \bigr \}\)

Not formalized. This row depends on local reciprocity and/or higher ramification filtrations; current Mathlib leaves the latter lower-numbering theory unimplemented and checked CFT candidates are incomplete.