FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 4 definitions, 2 theorems, 11 propositions, 13 lemmas, 13 corollaries and 3 conventions.
Of the 46 statements checked against Lean, 0 are formalized somewhere and 46 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 46 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 46 |
- Canonical source block: FC10 Serre Chapter 5, “The Norm”,
FC10-C05-U001–FC10-C05-U046, 46 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 atH=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 ata40561e249ebf45d2870f5d9d45bc2eb4d80b242(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 C05:
mathlib0,project-existing0,package-import0,reference-port0,unmatched46.
Convention / notation
Notation.Ifuis a non-negativereal number, \(\mathrm { \bf U } _ { \mathrm { L } } ^ { v }\) denotes the group \(\dot { \mathrm { \bf ~ U } } _ { \mathrm { \bf ~ I } } ^ { n } ,\) wheren is the smallest integer \(\geq v\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 1
Lemma 1. Let \[ \begin{array} { c } { { 0 \to \mathrm { A } ^ { \prime } \to \mathrm { A } \to \mathrm { A } ^ { \prime \prime } \to 0 } } \\ { { \{ ^ { \prime } \} \qquad \{ \downarrow \quad \uparrow ^ { \prime \prime } \} } } \\ { { 0 \to \mathrm { B } ^ { \prime } \to \mathrm { B } \to \mathrm { B } ^ { \prime \prime } \to 0 } } \end{array} \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 2
Lemma 2. Let A (resp. \(\mathbf { A } ^ { \prime }\) ) be an abelian group provided with a decreasing sequence of subgroups \(\mathbf { A } _ { \# }\) (resp. \(\mathbf { A } _ { n } ^ { \prime } .\) Suppose that \(\mathbf { A } _ { 0 } = \mathbf { A }\) \(\mathbf { A } _ { 0 } ^ { \prime } = \mathbf { A } ^ { \prime }\) ,and that Aand \(\mathbf { A } ^ { \prime }\) are complete Hausdorf spaces in the topologies defined by \(A _ { n }\) and \(A _ { n } ^ { \prime }\) (in other words,the canonical homomorphisms \(\mathbf { A } \to \{ \mathrm { i m } \mathbf { A } / \mathbf { A } _ { \eta }\) and $ ^ { } $ lim \(A ^ { \prime } / A _ { n } ^ { \prime }\) are bijective).Let \(u \colon \mathbf { A } \mathbf { A } ^ { \prime }\) bea homomorphism sending \(\Lambda _ { \eta }\) into \(A _ { n } ^ { \prime }\) foralln.Ifthe homomorphisms \[ \textstyle { u _ { n } } \colon \mathrm { A } _ { n } / \mathrm { A } _ { n + 1 } \to \mathrm { A } _ { n } ^ { \prime } / \mathrm { A } _ { n + 1 } ^ { \prime } \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 1
Proposition 1. 1f \(L / \mathbb { K }\) is unramified,then \(\aleph\) maps \(\mathrm { \Delta E _ { L } ^ { \it n } }\) into \({ \dot { \mathrm { ~ U ~ } } } _ { \mathbb { K } } ^ { n }\) for all n
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 2
Proposition 2.Suppose \(L / \mathbb { X }\) isunramified.Then i）Themap \(\ N _ { 0 } : \mathfrak { T } ^ { * } \to \mathfrak { K } ^ { * }\) is just the norm in the residue extension \(I / R\) ii For \(n \geq 1\) ,themap \(\aleph _ { n } \colon \overline { { { \sf L } } } \otimes _ { \bf K } \varOmega _ { \bf K } ^ { n } \varOmega _ { \bf K } ^ { n }\) is just the map \(\mathbb { T r } _ { \mathbf { f } _ { \mathbf { f } } / \overline { { \mathbf { K } } } } \otimes \mathbf { f }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 3
Proposition 3 a) \(\ N \{ \mathrm { U } _ { \ell _ { 1 } } ^ { n } \} = \mathrm { U } _ { \ell } ^ { n }\) forall \(n \geq 1\) b) \(\mathrm { U } _ { \kappa } / \mathrm { N } \mathrm { U } _ { \mathrm { L } }\) is isomorphic to \(\mathbb { K } ^ { \ast } / \mathbb { N } \mathbb { L } ^ { \ast }\) ： c） \(\hslash ^ { * } / \hslash \mathrm { \sf V L } ^ { * }\) is isomorphic to \(\mathbf { Z } / f \mathbf { Z } \times { \bar { \mathbf { K } } } ^ { * } / { \mathbf { N } } { \bar { \mathbf { L } } } ^ { * }\) ,where \(f = [ \mathbf { L } ; \mathbb { K } ] = [ \bar { \mathbf { L } } ; \bar { \mathbf { K } } ]\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary: Corollary.The three following conditions are equivalent
Corollary.The three following conditions are equivalent: (1） \(\{ { \mathbb { K } } ^ { * } : { \mathbb { N } } { \mathbb { L } } ^ { * } \} = f .\) (2） \(\mathrm { U } _ { \kappa } = \aleph \mathfrak { U } _ { \mathtt { L } }\) ，(3) \(\bar { \mathsf { K } } ^ { * } = \mathsf { N } \bar { \mathsf { L } } ^ { * }\) ，
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 3
Lemma 3.Thedifferent \(\mathfrak { T }\) of theextension \(L / \mathbb { K }\) is \(\mathfrak { R } _ { \mathfrak { L } } ^ { m }\) where \(m = \{ t + 1 \} ( \{ \} - \{ \} ) .\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 4
Lemma 4. For erery integer \(n \geq \ell .\) \(\mathfrak { T r } ( \mathfrak { p } _ { \mathrm { L } } ^ { \eta } ) = \mathfrak { p } _ { \mathtt { K } } ^ { \ r }\) ,where \(r = [ ( m + n ) / \lbrace ]\) and \(m = ( t + 1 ) ( \vec { t } - 1 ) ,\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 5
Lemma 5. 1f \(\boldsymbol { x } \in \mathfrak { p } _ { \mathrm { L } } ^ { n }\) ,then \[ \mathbb { N } ( 1 + x ) \equiv 1 + \mathbb { T r } ( x ) + \mathbb { N } ( x ) \bmod { . } \operatorname { T r } ( \mathfrak { p } _ { \mathtt { L } } ^ { 2 n } ) . \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Convention / notation
For a cyclic Galois group written exponentially, write \(x^s\) for the transform of \(x\) by \(s\); then \(N(1+x)=\prod_{s\in G}(1+x^s)\).
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 1
Corollary1.The homomorphism \(\Nu _ { n }\) is injective for all n except for \(n = l ,\) in which case there is an exact sequence: \[ \begin{array} { r } { 0 \to \mathbb { G } \stackrel { \beta _ { 1 } } { \to } \mathbb { U } _ { 1 } ^ { t } / \mathbb { U } _ { 1 } ^ { t + 1 } \stackrel { \mathbb { N } _ { t } } { \to } \mathbb { U } _ { \mathbb { K } } ^ { t } / \mathbb { U } _ { \mathbb { K } } ^ { t + 1 } . } \end{array} \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 2
Corollary2.The homomorphism \(\mathbf { N } _ { \mathfrak { n } }\) is surjective for \(\pmb { \mathscr { n } } > \pmb { \mathscr { t } } _ { : }\) and,if \(\pmb { \mathrm { \cal K } }\) is perfect, for \(n < t .\) \(\vec { \bf K }\) isalgebraicallyclosed,it issurjectiveforall \(\pmb { n }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 3
Corollary 3. We have \(\mathbb { N } \{ \mathbb { U } _ { \mathbb { L } } ^ { * ( n ) } \} = \mathbb { U } _ { \mathbb { K } } ^ { * }\) for \(n > t _ { i }\) and \(\mathbb { N } ( \mathbb { U } _ { \mathrm { L } } ^ { \psi ( \ast ) + 1 } ) = \mathbb { U } _ { \mathrm { K } } ^ { \mathsf { n } + 1 }\) for \(n \geq t .\) When \(\pmb { \mathrm { R } }\) isalgebraically closed,theseequalitieshold forall \(\pmb { \mathscr { n } }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 4
Proposition 4.For every integer \(\mathbf { \widetilde { \Gamma } } n \geq 0 , \mathbf { N } ( \mathbf { U } _ { \mathrm { L } } ^ { \psi ( n ) } ) \subset \mathbf { U } _ { \mathrm { K } } ^ { n } a n d \mathbf { N } ( \mathbf { U } _ { \mathrm { L } } ^ { \psi ( n ) + 1 } ) \subset \mathbf { U } _ { \mathrm { K } } ^ { n + 1 } .\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 5
Proposition 5. i） For \(n \equiv \mathbb { 0 } .\) the map \(\ N _ { 0 } \colon \bar { \mathbf { K } } ^ { * } \bar { \mathbf { K } } ^ { * }\) is given by \(N _ { 0 } \{ \xi \} = \xi ^ { f }\) \(\{ f \} \neq 0\) (where \(t\) is the last index for which the correspondingramification group is non-trivial,this map is injective;if \(t = 0\) itskernel iscyclic of orderl,and is equal to the image of G under the map \(\theta _ { 0 } { : \bf G } \to \mathrm { U } _ { \mathrm { L } } / \mathrm { U } _ { \mathrm { L } } ^ { 1 }\) (defined in Chapter IV, \(\ S 2\) prop.7).
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 4
Corollary4.We have \(\mathbb { N } \{ \mathrm { U } _ { \mathrm { L } } ^ { i \ell ( v ) } \} = \mathbb { U } _ { \mathsf { K } } ^ { v } i f i \ell\) is a real number \(> \mathfrak { f }\) 0r \(i f K\) is algebraicallyclosed.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 5
Corollary 5. 1f \(\{ { \bf \Phi } = 0 \} .\) Coker \([ \mathbf { N } _ { t } \} = \bar { \mathbf { K } } ^ { * } / \bar { \mathbf { K } } ^ { * t }\) 1f \(\ell \neq \ell ,\) Coker \(( N _ { t } )\) is isomorphic t0 \(R / \{ \zeta \} \{ \bar { \mathsf { K } } \} .\) with \(\wp ( \zeta ) = \zeta ^ { p } - \zeta\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 6
Corollary 6. 1f \(\breve { \mathbb { K } }\) isperfect, \(\Nu : \mathrm { U } _ { \mathrm { U } } / \mathrm { U } _ { \mathrm { L } } ^ { n } \to \mathrm { U } _ { \mathrm { K } } / \mathrm { U } _ { \mathrm { K } } ^ { n }\) is an isomorphism for all \(n \leq { \mathfrak { k } }\) ，
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 7
Corollary 7. 1f \(\Re\) is perfect,the following three canonical homomorphism are isomorphisms: \[ \mathrm { C o k e r ( N _ { t } ) \gets U _ { K } ^ { \dag } / N ( U _ { t } ^ { \dag } ) \to U _ { K } / N U _ { L } \to K ^ { \ast } / N L ^ { \ast } } \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 6
Lemma 6.Suppose that \(\mathbf { L }\) is a field that is the union of an increasing directed family of subfields \(\{ \mathbf { L } _ { i } \} _ { i \in \{ 1 \} }\) andletMbea finiteextension of \(\mathtt { L }\) of degree n. Then there exists an index \(i \in \mathbb { I }\) and an extension \(\mathbf { M } _ { i }\) of \(L _ { j }\) that has degree \(n\) and is linearly disjoint from L over \(\mathbf { L } _ { i }\) such that \(\mathbf { M } _ { \mathrm { i } } \mathbf { L } = \mathbf { M }\) \(\mathbf { M } _ { i }\) and \(\mathbf { M } _ { j }\) both satisfy these conditions,then there is an index \(k \geq i , j\) such that $ _ { i } _ { k } $ \(M _ { j } L _ { k }\) IfMisseparable (resp.Galois), \(\mathbf { M } _ { i }\) can be chosen to be separable (resp.Galois) over \(\mathbf { L } _ { j }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 7
Lemma 7.Let K bea field complete under a discrete valuation,having perfect residue field \(\pmb { K }\) Let \(\mathbf { K } _ { n r }\) be the maximal unramified extension of \(\kappa\) andlet E bea finite extension of \(\mathbb { K } _ { n r }\) of degreen.Then there exist a finite subextension \(\kappa\) f \(K _ { n r }\) and an extension \(\mathbf { E } ^ { \prime } / \mathbf { K } ^ { \prime }\) ofdegreen,linearlydisjoint from \(\mathbb { K } _ { \mathfrak { m } }\) over \(\aleph ^ { \prime }\) ,such that \(\mathbf { E } = \mathbf { E ^ { \prime } } \mathbf { K } _ { n r }\) .The extension \(\mathbb { E } ^ { \prime } / \mathbb { K } ^ { \prime }\) is then totally ramified,and E canbe identified with \(\mathbf { E } _ { n r } ^ { \prime }\) IfEis separable(resp.Galois), then \(\mathbf { E ^ { \prime } } / \mathbf { K } ^ { \prime }\) can be chosen likewise.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 6
Proposition 6.With the hypotheses above,let \(x \in \mathbb { K } ^ { * }\) Then there exists an extension \(\bar { \bf K } ^ { \prime } \bar { \bf K }\) of degree \(\leq l ,\) such that \(x\) is \(a\) norm in the corresponding extended extension \(L ^ { \prime } / \aleph ^ { \prime }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary: Corollary
Corollary. With the hypotheses above, \(N(L_{nr}^{*})=K_{nr}^{*}\).
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 7
Proposition7.Let K be a field complete under a discrete valuation,with perfect residue field \(\pmb { \bar { \kappa } }\) Let \({ \bf K } _ { n r }\) be the maximal unramified extension of \(\kappa\) and let \(\mathbf { F } \supset \mathbf { E } \supset \mathbf { K } _ { n }\) be two finite extensions of \(\mathtt { K } _ { \mathtt { m } \mathtt { r } }\) ,with \(\mathbf { f } \operatorname { \mathrm { / } E }\) separable.Then \(\mathsf { N } \{ \mathsf { F } ^ { * } \} = \mathsf { E } ^ { * }\) ，
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Definition / construction
A polynomial \(P\in k[X]\) is multiplicative when \(P(XY)=P(X)P(Y)\) and \(P(1)=1\).
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Definition / construction
If a multiplicative polynomial has degree \(h=h_0p^r\) with \((h_0,p)=1\), its separable degree is \(d_s(P)=h_0\).
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Definition / construction
A polynomial \(P\) is called additive if \(P(X+Y) = P(X) + P(Y)\). If \(k\) has characteristic zero then \(P(X) = aX\) for some \(a \in k\); if \(k\) has positive characteristic \(p\), then \(P\) is a linear combination of monomials \(X^{p^{h}}\). If \(P \neq 0\) it can be written uniquely, for \(k\) perfect, as \[ P = X^{p^{s}} \circ P', \qquad P' = a_{0}X + \cdots + a_{k}X^{p^{k}}, \quad a_{0}, a_{k} \neq 0. \] The degree \(d(P)\) is \(p^{s+k}\), and \(p^{k}\) is called the separable degree of \(P\), written \(d_{s}(P)\).
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Convention / notation
The degree \(d \{ { \bf P } \}\) of \(\mathbf { p }\) is equal to \(p ^ { \hbar + k }\) ; the integer \(p ^ { k }\) is called the separable degree of \(\mathbf { P }\) and isdenoted \(d _ { s } \{ \pmb { \ P } \}\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 8
Proposition 8.For every integer \(n \geq 0 , \mathrm { N } ( \mathrm { U } _ { \mathrm { L } } ^ { \psi _ { 1 } ^ { \prime } n ) } ) \subset \mathrm { U } _ { \aleph } ^ { n }\) and \(\mathbb { N } \{ \mathrm { U } _ { \mathtt { L } } ^ { \psi ( \# ) + 1 } \} \subset \mathrm { U } _ { \mathtt { K } } ^ { \mathtt { N } + \mathtt { i } }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 9
Proposition 9. For \(n = 0\) (resp. \(n \neq 0\) thehomomorphism \(\Nu _ { n }\) is induced by \(\pmb { a }\) multiplicatice (resp.additive) non-constant polynomial \({ \bf { P } } _ { \pmb { \pi } }\) such that \[ d \{ \mathrm { P } _ { n } \} = \mathrm { C a r d } ( \mathrm { G } _ { \psi ( n ) } ) \quad a n d \quad d _ { s } ( \mathrm { P } _ { n } ) = ( \mathrm { G } _ { \psi ( n ) } ; \mathrm { G } _ { \psi ( n ) + 1 } ) = \psi _ { d } ^ { \prime } ( n ) / \psi _ { q } ^ { \prime } ( n ) , \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 3
Corollary 3.We have \(\mathbb { N } ( \mathbb { U } _ { 1 } ^ { \psi ( n ) } ) = \mathbb { U } _ { \mathbb { K } } ^ { n }\) if \(\mathbf { G } _ { \psi ( \pi ) } = \{ \mathfrak { h } \}\) ,and \(\mathbb { N } ( \mathbb { U } _ { \mathrm { L } } ^ { \psi ( r ) + 1 } ) = \mathbb { U } _ { \mathbb { K } } ^ { n + 1 }\) \(i f \ G _ { \psi ( n + 1 ) } \approx \{ 1 \}\) When \(\bar { \bf K }\) isalgebraicallyclosed,theseequalities hold forall \(n \geq 0 .\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 4
Corollary 4. Let \(v\) be a non-negative real number.Then \(\mathbb { N } ( \mathbb { U } _ { \mathrm { L } } ^ { \ast \ell \left( v \right) } \} = \mathbb { U } _ { \mathrm { K } } ^ { v }\) i either \(\mathrm { G } _ { \psi ( v ) } = \{ \mathfrak { l } \}\) orifKisalgebraically closed.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Definition / construction
When the residue field is finite, the polynomials \(P_n\) attached to Proposition 9 have a unique choice invariant under residue extensions; these are called the canonical polynomials.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 10
Proposition 10. Suppose \(\pmb { \mathrm { R } }\) is perfect,and let \(x \in \mathbf { K } ^ { * }\) Then there exists an extension \(\vec { \bf K } / \vec { \bf K }\) of degree \(\leq [ \mathbf { L } ; \mathbf { K } ] ,\) such that \(\pmb { x }\) is a norm in the extended extension \(L ^ { \prime } / 8 ^ { \prime }\) corresponding to \(\sqrt { 5 }\) ：
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Theorem 1
Theorem1.Let K be a field complete undera discrete valuation,and letL be a finiteabelian extension of K,with Galois group \(\pmb { \ G }\) ;suppose that the residue extension \(E / R\) is separable.If \(\mathfrak { P }\) is \(\pmb { \alpha }\) jump in thefiltration \(\{ \mathbf G ^ { * } \}\) of \(G ,\) then \(\mathfrak { v }\) is an integer.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 1
Corollary 1. \(\aleph _ { \ast }\) is injective \(i f\) and only if \(\mathbf { G } _ { \psi ( n ) } = \mathbf { G } _ { \psi ( n ) + 1 }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Corollary 2
Corollary 2. \(\mathbb { N } _ { \pi }\) is surjective in each of the following three cases: i \(\pmb { K }\) isalgebraically closed, ii)Kis perfect,and G(n）=G(n）+1 i \(\mathbf { G } _ { \psi ( \mathfrak { n } ) } = \{ \mathfrak { k } \}\) ，
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Theorem 1’
Theorem 1’.With the hypotheses of theorem 1,if \(\mu\) is an integer such that \(\mathrm { G } _ { \mathfrak { x } } \not \equiv \mathrm { G } _ { \mathfrak { x } + \mathfrak { t } }\) then \(\varphi _ { \ell , \ell \mathsf { K } } \{ \mu \}\) is an integer.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Proposition 11
Proposition 11. Let \(L / \mathbb { K }\) bea cyclic,totally ramified extension,with Galois group G,and let \(\mu\) be the largest integer such that \(\mathbf { G } _ { \mu } \neq \{ \mathbf { f } \}\) Then \(\phi _ { 1 , r } \kappa ( \mu )\) is aninteger.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 8
Lemma 8.The group \(\mathrm { v } / \mathrm { w }\) is cyclic.
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 9
Lemma 9.Form sufficiently large, \(\mathrm { V } _ { \mathfrak { m } } = \mathrm { W } _ { \mathfrak { m } }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 10
Lemma 10. 1f \(\varphi ( m )\) is an integer and if \(\mathrm { G } _ { \mathfrak { m } } = \mathrm { G } _ { \mathfrak { m } + 1 }\) ,then \(\mathbf { V } _ { m } = \mathbf { V } _ { m + 1 }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 11
Lemma11.Let mbea positive integer.Ifthe image of \(\mathbb { W } _ { m } \ i n \ \mathrm { U } _ { \mathtt { L } } ^ { m } / \mathrm { U } _ { \mathtt { L } } ^ { m + 1 }\) is non-trivialthenthatimageisequaltolof \(\mathrm { U } _ { \mathrm { L } } ^ { m } / \mathrm { U } _ { \mathrm { L } } ^ { m + 1 }\) ，
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 12
Lemma 12.Let n be an integer such that \(\mathbf { G } _ { \psi ( n + 1 ) } = \{ \{ \} \}\) Letm be an integer such that \[ n < \varphi ( m ) < n + 1 . \]
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.
Lemma 13
Lemma 13.Let m be an integer, and let \(\pi + 1\) be the smallest intege \({ \vec { r } } \geq \varphi \{ m \} .\) \(\Zeta _ { \mathcal { A } _ { \varphi ; \pi + 1 } } ^ { \mathcal { \dot { x } } } = \{ \{ \} \}\) then \(\mathbb { V } _ { m } = \mathbb { W } _ { m }\)
Not formalized. No checked compatible source supplies Serre’s full local norm-filtration/Herbrand norm statement; nearby ideal or field norm APIs are only ingredients.