FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 8 definitions, 2 theorems, 15 propositions, 1 lemma, 11 corollaries, 2 examples and 4 conventions.
Of the 43 statements checked against Lean, 0 are formalized somewhere and 43 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 43 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 43 |
- Canonical source block: FC10 Serre Chapter 13, “Local Class Field Theory”,
FC10-C13-U001–FC10-C13-U043, 43 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 C13:
mathlib0,project-existing0,package-import0,reference-port0,unmatched43.
Proposition 1
Proposition 1. Let \(\mathbf { A } ^ { \prime }\) bethe subgroup of A consisting of those \(a \in \mathbb { A }\) for which there is a positive integernsatisfying \(\{ 1 + \mathfrak { F } + \cdots + \mathfrak { F } ^ { n - 1 } ) a = 0 ,\) Then \[ \mathbf { H } ^ { \mathbf { i } } ( \mathfrak { g } , \mathbf { A } ) = \mathbf { A } ^ { \prime } / ( \mathbf { F } - \mathbf { 1 } ) \mathbf { A } . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary: Corollary
Corollary. The character group \(\mathbf { X ( 9 ) }\) of \(\mathfrak { g }\) can be identified with \(\mathbf { Q } / \mathbf { Z }\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 2
Proposition 2.If A is either a divisible group or a torsion group,then \(\mathrm { H } ^ { 2 } \{ { \mathfrak { g } } , \mathrm { A } \} = 0 .\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Convention / notation
Finally,suppose A is divisible.If \(n \geq \sharp\) ,denote by \(\pmb { n } ^ { \hat { \pmb { A } } }\) the kernel of multiplication by n on A.The exact sequence \[ 0 \to {}_{n}A \to A \xrightarrow{\ n\ } A \to 0 \] is then available.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
We denote by \(z\) the completion of \(\mathbf { z }\) for the topology of subgroups of finite index； it is a compact totally disconnected group,equal to the projective limit of the groups \(\mathbb { Z } / n \mathbb { Z } .\) By decomposing these groups into their \(p\) primary components,one sees that \(\pmb { \mathcal { Z } }\) is canonically isomorphic to the product \(\prod z _ { p }\) \(p\) running through the prime numbers).
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
Set \({ \mathfrak { g } } = { \hat { \mathbf { Z } } }\) and \({ \mathfrak { g } } _ { n } = n { \hat { \mathbf { Z } } }\) ; then \({ \mathfrak { g } } = { \mathrm { l i m } } { \mathfrak { g } } / { \mathfrak { g } } _ { n }\) and every open subgroup of \(\mathfrak { G }\) coincides with some \(\mathfrak { g } _ { \mathfrak { n } }\) LetA be topological \({ \mathfrak { g } }\) module (in the sense of Chap.X,$3). The canonical generator \({ \bf 1 \in Z }\) defines an automorphism \(\boldsymbol { \mathsf { F } }\) ofA;to say that A isa topological \(\mathfrak { g }\) -module then means that for each \(a \in \mathsf { A }\) there is a positive integer \(\pmb { n }\) such that \(\mathbb { F } ^ { n } a = a .\) Thus the group A is the union of its subgroups \(\mathsf { A } ^ { \mathfrak { g } _ { m } }\) ,the latter being \({ \mathfrak { g } } / { \mathfrak { g } } _ { n }\) modules.The cohomology groups \(\alpha f g\) with values in Aare defined by the formula \[ H^{q}(\mathfrak{g}, A) = \varinjlim_{n} H^{q}(\mathfrak{g}/\mathfrak{g}_{n}, A^{\mathfrak{g}_{n}}). \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Convention / notation
such that \(f _ { s } \{ 1 \} = s .\) If the group \(\mathfrak { g }\) is denoted multiplicatively,we will write \(s ^ { \nu }\) instead of \(f _ { s } ( \nu ) , \nu \in \hat { \mathcal { Z } }\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
A quasi-finite field structure on a field \(k\) consists of a chosen \(F\in G(k_s/k)\) such that \(k\) is perfect and the map \(\widehat{\mathbf Z}\to G(k_s/k)\), \(\nu\mapsto F^{\nu}\), is an isomorphism.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Example / comparison
ExAMPLES OF QUASI-FINITE FIELDS.a) Finite fields.If \(k\) has \(q\) elements,take \(\mathbf { F }\) to be the“Frobenius substitution” \(x \mapsto x ^ { q }\) (cf.Bourbaki,Alg.,Chap.V,$11).
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Example / comparison
b)Let \(\mathbf { c }\) be an algebraically closed field of characteristic zero,and let \(k = C ( \{ \tilde { \Pi } \} )\) ,the power series field in one variable.For every integer \(n \geq 1\) \(k _ { n } = C \{ ( { \mathbb { T } } ^ { 1 / n } ) \}\) isacyclic extension of degreenof \(k ,\) and the union \(k _ { s }\) ofthe \(k _ { \pi }\) is an algebraic closure of \(k\) (cf.Chap.IV,prop.8).A generator \(\mathbf { F } _ { \mathfrak { n } }\) of \(\mathrm { G } \{ \boldsymbol { k } _ { n } / k \}\) is defined by \(\mathbf { T } ^ { \downarrow / \pi } \mapsto a _ { n } \mathbf { T } ^ { 1 / n }\) where \(a _ { n }\) is a primitive nth root of unity. For the \({ \widehat { \mathbf { F } } } _ { \mathfrak { n } }\) to fit together and define an F,the \(\pmb { a } _ { \pmb { \pi } }\) must be chosen to satisfy \(\smash { ( a _ { m n } ) ^ { n } = a _ { m } }\) which ispossible (cf.Bourbaki,loc.cit.）；when \(\Gamma = \mathbf { C }\) one can take \(a _ { n } = \exp \{ 2 \pi i / n \}\) Thus \(k\) is quasi-finite.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 3
Proposition 3.Letk bea quasi-finite field,andletFbe the given free generator of its Galois group.Let \(k ^ { \prime } / k\) bea finite extension of degreen,and let \(\mathbf { F } ^ { \prime } = \mathbf { F } ^ { \prime \prime }\) Then \(\mathbb { F } ^ { \prime } \in \operatorname { G } \{ \mathbb { k } _ { s } / \mathbb { k } ^ { \prime } \} ,\) and \(\mathbf { F } ^ { \prime }\) provides \(k ^ { \prime }\) witha structure of quasi-finite feld.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 4
Proposition 4. Let \(k\) be a quasi-finite field,F the free generator of its Galois group \({ \mathfrak { g } } = { \mathrm { G } } ( { k _ { \mathrm { s } } } / { k } )\) a) \(H \ w \in K _ { s } ^ { \ast }\) is a root of unity,there exists \(y \in k _ { s } ^ { * }\) such that \(w = y ^ { { \mathsf { F } } - 1 }\) (i.e., \(w = \mathbf { F } \{ y \} / y \}\) b）if \(k\) has characteristic \(\neq 0\) thehomomorphism \(\mathfrak { F } - 1 : \mathfrak { k } _ { s } \to \mathfrak { k } _ { s }\) is surjective.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Convention / notation
be identified with \(\mathbf { Q } / \mathbf { Z }\) This givesa homomorphism \(\mathbf { \delta B _ { \mathbf { K } } } \to \mathbf { Q } / \mathbf { Z }\) which will be denoted \(\dot { \bar { \mathbf { u v } } } _ { \mathbf { x } }\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 5
Proposition 5.The Brauer group of a quasi-finite field is zero.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary: Corollary
Corollary. If \(k ^ { \prime }\) is \(^ a\) finiteextension of aquasi-finite field \(k _ { i }\) then the norm map \(N : k ^ { \prime \star } \to k ^ { * }\) is surjective.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 6
Proposition 6.The homomorphism \(\mathbf { i n v _ { \mathbf { K } } } : \mathbf { B _ { \mathbf { K } } } \to \mathbf { Q } / \mathbf { Z }\) is an isomorphism.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
The invariant map \(\operatorname{inv}_K:B_K\to\mathbf Q/\mathbf Z\) is the composite \(\gamma\circ\delta^{-1}\circ\beta\circ\alpha^{-1}\) arising from \(B_K\cong H^2(\mathfrak g,K_{nr}^*)\to H^2(\mathfrak g,\mathbf Z)\to H^1(\mathfrak g,\mathbf Q/\mathbf Z)\to\mathbf Q/\mathbf Z\).
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 7
Proposition 7. Let L bea finite extensionof \(\mathbf { \check { K } }\) of degreen, and let $ _ { / } : _ { } $ \(\ B _ { \mu }\) be the canonical homomorphism of \(\mathbf { B _ { K } }\) into \(\mathbf { B _ { \lambda } }\) (cf. Chap. X, \(\ S 4\) aswell as Chap. XI, \(\ S \ S \ S , 2 )\) .Then \[ \mathbf { i n v _ { k } } \circ \mathbf { R e s } _ { \mathbf { k } / \mathbf { k } } = n , \mathbf { i n v _ { k } } . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary 1
Corollary 1.Keeping the hypotheses and notation of prop.7,a necessary and sufficient condition foran element \(\pmb { a } \in \mathbb { B } _ { \mathbb { K } }\) to be split byLis \(n a = 0 .\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary 2
Corollary 2. Suppose \(L / \mathsf { K }\) is Galois.Then the isomorphism \(\mathbf { i n v _ { K } } : \mathbf { B _ { K } } \to \mathbf { Q } / \mathbf { Z }\) maps the subgroup \(\mathbb { H } ^ { 2 } ( \mathbb { I } _ { - } / \mathbb { K } )\) f \(\mathfrak { B } _ { \mathtt { K } }\) onto the subgroup \(( \mathbf { f } / n ) \mathbf { Z } / \mathbf { Z }\) f \(\mathbf { Q } / \mathbf { Z }\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary 3
Corollary 3.Let \(\mathbf { D }\) beacentral division algebra over \(\mathbf { \delta K }\) ofrank \(n ^ { 2 }\) andlet \(a \in \mathbb { B } _ { \mathbb { K } }\) bethe corresponding element of the Brauer group.Thena has order \(\pmb { n }\) in \(\mathbf { B _ { K } }\) ,and everyextension of \(\mathbf { K }\) ofdegreencanbeembedded in D.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Theorem 1
Theorem 1.The preceding formation, together with the \(\dot { \mathfrak { s m } } \mathfrak { v } _ { \mathtt { E } }\) is a class formation (cf.Chap.X1,$2).
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 8
Proposition 8.For every integer n, the cup product with \(u _ { \mathrm { F } ; \mathrm { E } }\) defines an isomorphism \[ \hat { \mathbf { H } } ^ { n } ( \mathbf { G } _ { \mathrm { F / E } } , \mathbf { Z } ) \to \hat { \mathbf { H } } ^ { n + 2 } ( \mathbf { G } _ { \mathrm { F / E } } , \mathbf { F } ^ { * } ) . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary: Corollary，The cup product with \(\boldsymbol { u } { \mathbb { F } / \Xi }\)…
Corollary，The cup product with \(\boldsymbol { u } _ { \mathbb { F } / \Xi }\) defines an isomorphism \[ \theta _ { \mathrm { F } i \mathrm { E } } \colon \mathbf { G } _ { \mathrm { F } j \mathrm { E } } ^ { a } \to \mathrm { E } ^ { * } / \mathrm { N F } ^ { * } \quad ( \mathrm { N } \ d e n o t i n g \ t h e \ n o r m \ i n \ \mathrm { F } / \mathrm { E } ) . \] Inparticular, \(( \mathrm { E } ^ { * } \colon \mathrm { N F } ^ { * } ) = \left[ \mathrm { F } \colon \mathrm { E } \right] i f \mathrm { ~ F } / \mathrm { E }\) is an abelian extension.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 9
Proposition9.If F/E is a finite separable extension,then \(\mathbf { N F ^ { * } }\) has finite index in \(\mathbf { E } ^ { * }\) ；thisindexdivides[F:E],andisequal toit ifand onlyifF/Eis abelian.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
For a finite abelian extension \(F/E\), let \(\theta_{F/E}:G_{F/E}\to E^*/N_{F/E}F^*\) be the class-formation isomorphism. Its inverse is the reciprocity isomorphism, and for \(x\in E^*\) one writes \(\{x,F/E\}=\theta_{F/E}^{-1}(\bar x)\).
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary: Corollary
Corollary. Let \(\mathbf { \mathbb { F } } / \mathbf { \mathbb { E } }\) be an abelian extension with Galois group G.Let \(\mathbf { U } _ { \Xi } \subset \mathbf { E } ^ { \ast }\) be the group of units of E.Then the reciprocity map \(\mathbf { E } ^ { * } \mathbf { G }\) sends \(U _ { \mathbf { E } }\) onto the inertia subgroup ofG.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 10
Proposition 10. Consider an extension \(\mathbf { F } \supset \mathbf { E } ^ { \prime } \supset \mathbf { E }\) with F/E Galois.The \(g r o u p \mathbb { G } _ { \mathbb { F } / \mathbb { E } }\) is a subgroup of \(\mathbf { G } _ { \mathbf { F } / \mathbf { E } }\) a)If \(x \in \mathbb { E } ^ { \prime * }\) and \(y = \Nu _ { \Xi ^ { \prime } i \in } ( x ) ,\) then the image of \(\{ x , \mathbf { F } / \mathbf { E ^ { \prime } } \} \in \mathbf { G } _ { \mathbf { F } / \mathbf { E } } ^ { a } .\) in \(\mathbf { G } _ { \mathbf { F } / \mathbf { E } } ^ { \pmb { \alpha } }\) is equal to \(\{ y , \mathbf { F } / \mathbf { E } \}\) b)If \(\boldsymbol { x } \in \mathbb { E } ^ { * }\) ,the image of \(\{ x , \mathbf { F } / \mathbf { E } \} \in \mathbf { G } _ { \mathbf { F } / \mathbf { E } } ^ { a }\) in \(G _ { \mathcal { F } j \mathbf { E } ^ { \prime } } ^ { \alpha }\) under the transfer is equal to \(\{ x , \ F / \operatorname { E } ^ { \prime } \}\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 11
Proposition 11. 1f \(\mathbf { F } / \mathbf { E }\) is a Galois extension and \(s \in \mathbb { G } _ { F / \ E }\) ,then \[ \{ s x , s F / s \mathbb { E } \} = s \circ \{ x , \mathbf { F } / \mathbb { E } \} \circ s ^ { - 1 } \qquad f o r \ a l l \ x \in \mathbb { E } ^ { * } . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 12
Proposition 12.Consider an extension \(\mathbf { F } ^ { \prime } \supset \mathbf { F } \supset \mathbf { E }\) with \(\mathbf { F } / \mathbf { E }\) and \(\mathbf { F } ^ { \prime } / \mathbf { E }\) Galois \(\ b { I f } \ b { x } \in \ b { \mathrm { E } } ^ { * }\) then the imageof \(\{ { \boldsymbol { x } } , { \boldsymbol { \mathsf { F } } } ^ { \prime } / { \boldsymbol { \mathsf { E } } } \}\) in \(\mathbb { G } _ { \mathtt { F } ; \mathtt { E } } ^ { a }\) is equal to \(\{ \boldsymbol { x } , \boldsymbol { \mathsf { F } } / \boldsymbol { \mathbf { E } } \}\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
This last proposition allows us to define $ { ( x , F / E ) }$ fora Galois extension \(F / \frac { \pi } { L }\) that is not finite;it also shows that we can confine ourselves to abelian extensions.When \(\mathbf { F }\) is themaximal abelian extension \({ \mathfrak { E } } ^ { \alpha }\) of E, we write \(\{ x , { \bar { \mathbf { \pi } } } / { \mathbf { E } } \}\) instead \(\sigma _ { \mathrm { ~ } } ^ { \mathrm { ~ f ~ } } \{ x , \mathbb { E } ^ { a } / \mathbb { E } \}\) ；it is an element of the Galois group \(\mathfrak { A } _ { \Xi } = \mathsf { G } \{ \mathbf { E } ^ { a } / \Xi \} .\) The reciprocity map allows the identification of \(\mathfrak { Y } _ { \Xi }\) with the Hausdorff completion of \(\mathbf { E } ^ { \ast }\) forthe topology definedby the groups of norms (cf.Chap.XI, \(\ S 4 )\) We will determine this topology in the next chapter,for the special case where \(R\) is finite.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 13
Proposition 13. Let \(L / \bar { \bf K }\) be anunramified extension.If we identify the groups \(G _ { I / K }\) and \(\mathbf { G } _ { \mathbf { f } ; \hat { \mathbf { K } } }\) ,then \[ ( x , \mathbf { L } / \mathbf { K } ) = \mathbf { F } _ { \mathbf { K } } ^ { v ( x ) } , \] where \(\mathbf { F _ { K } }\) denotes the canonical generator of \(\mathbf { G } _ { \mathbb { L } / \bar { \mathbf { K } } }\) ,and where \(\mathfrak { v }\) is the valuation of K.
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
such that \(\dot { \mathrm { m } } \Psi _ { \mathrm { E } } ( u _ { \mathrm { F / E } } ) = \updownarrow / n _ { \ddag }\) with \(n = \left[ \mathbf { F } : \mathbf { E } \right]\) It is called the fundamental class of the extension \(F / \mathbb { E }\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Definition / construction
where \(\mathfrak { T } _ { \mathbb { K } }\) is the inertia group of \({ \bf K } ^ { a } / { \bf K }\) (defined by passage to the limit from the finite case).
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 14
Proposition 14. For every \(q \in { \bf Z } , \hat { \bf H } ^ { q } ( { \bf G } , \hat { \bf L } _ { n r } ^ { * } ) = 0 .\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary 1
Corollary 1. The exact sequence \(0 \to { \hat { \mathbb { U } } } _ { n r } \to { \hat { \mathbb { L } } } _ { n r } ^ { * } \to { \mathbb { Z } } \to 0\) defines an isomor-phismof \(\mathbf { G } ^ { a } = \hat { \mathbf { H } } ^ { - 2 } ( \mathbf { G } , \pmb { \mathbb { Z } } )\) onto \(\hat { \mathbb { H } } ^ { - 1 } \{ \mathbb { G } , \mathbb { U } _ { n s } \}\) ：
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary 2
Corollary 2. Let \(\pmb { \mathscr { s } } _ { \sharp } \in \mathbb { G }\) and \(z _ { i } \in \sum _ { n r } ^ { * }\) be elements such that \[ \prod z _ { i } ^ { s _ { i } - 1 } = 1 . \] \[ T h e n \prod s _ { i } ^ { w ( z _ { i } ) } \equiv 1 \mathrm { ~ } i n \mathrm { ~ } G ^ { a } . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary: Corollary
Corollary. \(L e t \ x \in K ^ { * }\) y∈L*,s∈G be such that \[ x = \mathbb { N } y , y ^ { \mathsf { F } - 1 } = \pi ^ { \mathsf { s } - 1 } , \pi \mathit { b e i n g ~ a ~ u n i f o r m i z e r ~ o f ~ } \hat { \mathsf { L } } _ { n r } . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Lemma 1
Lemma 1. In order that an element \(\pmb { x }\) \(\widehat { \mathbb { L } } _ { n r }\) (resp.of \(\scriptstyle { \hat { \mathbf { K } } } _ { n r } \}\) belong to L (resp. to K),it is necessary and sufficient that \(\mathbf { F } { \boldsymbol { x } } = { \boldsymbol { x } } .\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Theorem 2
Theorem 2 (Dwork).Let \(L / \kappa\) bea totally ramified Galois extension,having abelian Galois group G.Suppose that the residue field \(\Re = \mathbb { L }\) is quasi-finite. Let \(x \in \mathbb { K } ^ { * }\) ; let \(y \in \hat { \mathbf { L } } _ { n y } ^ { * }\) be such that \(\aleph _ { y } = x\) ;let \(\boldsymbol { z } _ { i } \in \mathbb { \hat { L } } _ { n r } ^ { * }\) \(s _ { i } \in \mathbf { G }\) be such that \[ y ^ { \mathbf { F } - 1 } = \prod z _ { i } ^ { s _ { i } - 1 } . \]
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Proposition 15
Proposition 15. Suppose \(\bar { \kappa }\) haspositive characteristic.Let V be the group of unitsof \(\hat { \mathfrak { L } } _ { \pi r }\) For every integer \(m \gtrsim \mathrm { \mathfrak { k } }\) ,thehomomorphism \(x \mapsto x ^ { F - 1 }\) maps \(V ^ { ( m ) }\) onto itself.If \(x\) is an element of \(\mathbf { V }\) whose residue class \(\vec { x } \in \bar { \mathbb { K } } _ { n \tau } ^ { * }\) is aroot of unity,then there exists \(y \in \mathbf { V }\) such that \(x = y ^ { \mathbf { F } - \textbf { t } }\) ，
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Corollary
Corollary.If \(\bar { \aleph }\) isafinite field,then \(\mathbf { V } = \mathbf { V } ^ { \ F \cdots \ F }\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.
Convention / notation
and denote by \(\mathbf { \vec { F } }\) the free generatorof \(\mathfrak { g }\) that defines the quasi-finite structure on \(R\)
Not formalized. No checked compatible source closes this local class-field-theory/quasi-finite-field reciprocity statement; available CFT implementations cross unresolved proof boundaries.