FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 12 definitions, 3 theorems, 16 propositions, 4 lemmas, 9 corollaries, 5 examples and 2 conventions.
Of the 51 statements checked against Lean, 2 are formalized somewhere and 49 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 49 | 96% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 2 | 4% | This repository states and proves it. |
| checked in total | 51 |
- Canonical source block: FC10 Serre Chapter 14, “Local Symbols and Existence Theorem”,
FC10-C14-U001–FC10-C14-U051, 51 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 C14:
mathlib0,project-existing2,package-import0,reference-port0,unmatched49.
Definition / construction
Let \(\mathbf { K }\) be a field, \(\mathbf { K } _ { s }\) a separable closure of \(\aleph\) ,and let \(\mathsf { G } = \mathsf { G } \{ \mathsf { K } _ { s } / \mathsf { K } \}\) f \(\chi\) is a character of G–i.e., an element of \({ \bf H } ^ { 1 } ( { \bf G } , { \bf Q } / { \bf Z } )\) -then \(\delta \chi\) is an element of \(\mathbb { H } ^ { 2 } ( \mathbb { G } , \mathbb { Z } )\) If \(b \in \mathbb { K } ^ { * }\) ,the cup product \(\dot { \boldsymbol { b } } . \delta \mathbb { Z }\) is an element of the Brauer group \(\mathbb { H } ^ { 2 } ( \mathbb { G } , \mathbb { K } _ { s } ^ { * } ) = \mathbb { B } _ { \mathbb { K } }\) .We denote this element by the symbol \(\{ \chi , b \}\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 1
Proposition 1 (i \(\{ \chi + \chi ^ { \prime } , b \} = \{ \chi , b \} + ( \chi ^ { \prime } , b ) .\) (i） \(\{ \chi , b b ^ { \prime } \} = \{ \chi , b \} + \{ \chi , b ^ { \prime } \} .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 2
Proposition 2. Let \(\boldsymbol { b } \in \mathbb { K } ^ { * }\) The element of \(\mathrm { H } ^ { 2 } \{ \pmb { \mathrm { L } } _ { \pmb { \chi } } / \mathrm { K } \}\) which corresponds to \(b\) isnone other than \(( \chi , b )\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary 1
Corollary 1. For \(( x , b )\) to be zero,it is necessary and sufficient that b bea norm in the extension \(L _ { x } / \mathbf { K }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary 2
Corollary 2.Foran elementof \(\mathbf { B } _ { \mathbf { K } }\) to have the form \(\{ \chi , b \}\) it isnecessary and sufficient that it besplit by \(L _ { z }\) ，
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 3
Proposition 3. Let \(s _ { \mathtt { b } } = \{ b , \^ { * } / \mathbf { K } \}\) be the element of \(\mathbf { G } ^ { \mathfrak { a } }\) defined by the reciprocity map.Then \[ \{ \chi , b \} _ { v } = \chi \{ s _ { b } ) , \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary: Corollary
Corollary. \(1 9 \chi\) is a character such that \(\{ \chi , b \} _ { v } = 0\) for all \(\boldsymbol { b } \in \mathbb { K } ^ { * }\) ,then \(\chi = 0\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
We have seen in Chap.X, \(\ S 3\) that each element \(a \in \mathbb { K } ^ { \ast }\) defines a homomorphism \(\varphi _ { a } \colon { \mathrm { G } } \to { \mathbf { Z } } / n { \mathbf { Z } } ,\) as follows:we choose in \({ { \bf { K } } _ { s } }\) a root \(\pmb { \alpha }\) of the equation \(\alpha ^ { n } = a\) and set \(\varphi _ { a } ( s ) = s \{ \alpha \} / \alpha .\) Next we choose a primitive nth root of unity \(\pmb { \nu }\) that has the effect of identifying \(\mu _ { \mathfrak { s } }\) with the group \({ \pmb Z } _ { f } { \pmb n } { \pmb Z }\) ; if we then set \[ \chi _ { a } ( s \} = { \frac { \mathbb { 1 } } { n } } \varphi _ { a } ( s ) \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
we obtain a homomorphism of \(\textbf { G }\) into the subgroup \(\{ 1 / \pi \} Z / Z\) of \(\mathbf { Q } / \mathbb { Z } ,\) i.e., a character of G.We know(loc.cit.) that the map \({ a \chi _ { a } }\) defines an isomorphism of \(\mathbf { K } ^ { \ast } / \mathbf { K } ^ { \ast n }\) onto the group of those characters of \(\mathbf { G }\) having order dividing n.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 4
Proposition 4. i） \(( a a ^ { \prime } , b ) = ( a , b ) + ( a ^ { \prime } , b ) .\) i \(\{ a , \dot { b } \dot { b } ^ { \prime } \} = \{ a , b \} + \{ a , \dot { b } ^ { \prime } \} ,\) iii） In order that \(\{ a , b \} = 0 _ { \ast }\) it is necessary and sufficient that \(b\) be \(a\) norm in theextension \({ \mathbb K } \{ a ^ { 1 / \pi } \} / { \mathbb K }\) iv） 1f \(a \in \mathbb { K } ^ { \ast }\) and \(\boldsymbol { x } \in \mathbb { K }\) are such that \(x ^ { n } - a \neq 0 .\) then \(\{ a , x ^ { n } - a \} = 0 .\) In particular, \(\{ a , - a \} = 0\) and \(\{ a , \mathrm { ~ i ~ } - a \} = 0 .\) v \(\{ a , b \} + \{ b , a \} = 0 .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
3)For \(n \div 2\) we have \(\mu _ { n } = \left\{ \pm 1 \right\}\) and the symbol \(\{ a , b \}\) is defined under the single hypothesis that \(\mathbf { \ X }\) have characteristic different from 2.The corresponding Severi-Brauer variety is the conic having homogeneous equation \(x ^ { 2 } - a y ^ { 2 } - b z ^ { 2 } = 0 .\) In particular, \(\{ a , b \} = 0\) if and only if this conic has a rational point in \(\mathbf { K }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Convention / notation
We denote by \(\pmb { \dot { \updownarrow } }\) the injection thus defined of \(\mathbf { H } ^ { z } ( \mathbf { G } , \mathbf { Z } / n \mathbf { Z } )\) into the Brauer group \(\mathbf { \delta B _ { K } }\) ，
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
Now let \(^ { a }\) and \(b\) be two elements of \(\kappa ^ { * }\) By what was said at the beginning of this section,we can associate to them the elements \(\varphi _ { \alpha } , \varphi _ { \mathfrak { b } }\) of the group \(H ^ { \mathrm { t } } \{ \mathbf { G } , \mathbf { Z } / n \mathbf { Z } \}\) The cup product then yields an element \(\varphi _ { \alpha } , \varphi _ { \beta }\) of \({ \mathrm { H } } ^ { 2 } ( \mathbf { G } , \mathbf { Z } / n \mathbf { Z } ) .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 5
Proposition 5. \(\{ a , b \} = i \{ \varphi _ { a } , \varphi _ { b } \} .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary: Corollary.Ifan element \(b \in \mathbb { K } ^ { }\) is \(\pmb { a }\) norm in…
Corollary.Ifan element \(b \in \mathbb { K } ^ { * }\) is \(\pmb { a }\) norm in every cyclic extension of \(\mathbf { K }\) f degreedividing \(\pmb { n }\) then \(\ b { b } \in \mathbb { K } ^ { \ast n }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Convention / notation
Remark.The symbol \(\left\{ a , b \right\} _ { \sharp }\) defined here is the inverse of the one in ArtinTate ([8], Chap.XI)，,but ooincides with the one in Hasse’s Bericht \(( [ 3 1 ] ,\) Teil I, \(\ S 1 1\) ,thanks to two compensating changes of sign. Properties i),ii) andiv) of prop.7 show that \(\{ a , b \} _ { v }\) isa“symbol”in the sense of algebraic \(\mathbf { K }\) -theory；see Moore \([ 1 0 0 ]\) and Tate [120,121] for more on this.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 6
Proposition 6. 1f \(\alpha \in \mathbb { K } _ { s } ^ { * }\) is an nth root of \(a ,\) andif \(s _ { \boldsymbol { \mathbf { b } } } = ( \boldsymbol { \mathbf { b } } , \boldsymbol { \mathbf { \mu } } ^ { * } / \boldsymbol { \mathbf { K } } )\) then \[ \{ a , b \} _ { n } = s _ { b } \{ \alpha \} / \alpha . \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary: Corollary.The symbol \(\left\{ a , b \right\} { \mu }\) doesnot depend on the…
Corollary.The symbol \(\left\{ a , b \right\} _ { \mu }\) doesnot depend on the choice of the root of unity \(\aleph\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 7
Proposition 7 i） \(\{ a a ^ { \prime } , b \} _ { \nu } = \{ a , b \} _ { \nu } \cdot ( a ^ { \prime } , b \} _ { \nu } \cdot\) i） \(( a , b \dot { b } ^ { \prime } ) _ { v } = ( a , \dot { b } ) _ { v } , ( a , \dot { b } ^ { \prime } ) _ { v } ,\) iIn order that \(\{ a , b \} _ { v } = \mathtt { i }\) itisnecessary and sufficient that \(^ { b }\) bea norm in the extension \({ \mathrm { K } } \{ \{ t ^ { 1 / n } \} / { \mathrm { K } }\) iv） \(( a , \textrm { -- } a ) _ { v } = \textrm { f } = ( a , \textrm { f } - a ) _ { v }\) v \(\{ a , b \} _ { \ast } , \{ b , a \} _ { v } = 1\) ： vi \(\it l f ^ { \prime } ( a , b ) _ { t } = 1\) forall \(b \in \mathbb { K } ^ { \ast }\) then \(a \in \mathbb { K } ^ { * n }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Lemma 1
Lemma 1.K contains the nth roots of unity if and only if \(\pmb { \ K }\) does;in that case thecanonical homomorphism \(\mathbf { U _ { \ K } } \to \mathbf { R ^ { * } }\) induces an isomorphism of the group \(\mu _ { n }\) ofnthrootsofunity of \(\pmb { \ K }\) onto the group \(\overline { { \mu } } _ { \varkappa }\) ofnth roots ofunity of R.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Lemma 2
Lemma 2. Let \(k\) bea quasi-finite field containing the group \(\mu _ { \eta }\) of nth roots ofunity (n being prime to the characteristic of \(k )\) Given \(x \in k ^ { * }\) ,let \(y \in k _ { s } ^ { * }\) be a solution to the equation \({ \boldsymbol { y } } ^ { \# } = { \boldsymbol { x } } ,\) and let \(z = \operatorname { F } y / y\) Then z belongs to \(\mu _ { n }\) and does not depend on the choiceof solution \(y ; i f\) we set \(\mathbb { P } _ { n } \{ x \} = z ,\) thenthe map \(\boldsymbol { \mathsf { P } } _ { \mathfrak { s } }\) defines by passage to the quotient an isomorphism of \(k ^ { \ast } / k ^ { \ast \pi }\) onto \(\mu _ { \pi }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Example / comparison
ExAMPLE. If \(k\) is a \(\hat { \pmb { \mathscr { k } } }\) nitefieldwith \(q\) elements,the hypothesis that \(k\) contains \(\mu _ { \eta }\) is equivalent to saying that ndivides \(q \sim \sharp\) .The map \(\mathbf { P } _ { \pi }\) is then given by the following formula: \[ \mathbf { P } _ { n } ( x ) = x ^ { \frac { q - 1 } { n } } \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 8
Proposition 8. Let a and \(\pmb { b }\) be two elements of \(\mathbf { K } ^ { * }\) and let \(\alpha\) and \(\beta\) be thei valuations.Set \[ c = ( - \mathbf { \nabla } \mathbf { j } ) ^ { \alpha \beta } \frac { a ^ { \beta } } { b ^ { \alpha } } . \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary: Corollary
Corollary. If \(\pmb { \widetilde { \kappa } }\) is a finite field with \(q\) elements,then \(( a , b ) _ { \scriptscriptstyle \parallel } , = \overline { { c } } ^ { \{ q - 1 \} / \eta }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 9
Proposition 9.Let K bea field complete underadiscretevaluationv;suppose that \(\kappa\) has characteristic zero and itsresidue field \(\bar { \bf K }\) has characteristic \(p \neq 0 ,\) Let \(e = v ( p )\) betheabsoluteramification index of \(\mathbf { K }\) (cf.Chap. II, \(\ S 5\) .For every positive integer \(m _ { i }\) denote by \(\mathbb { U } ^ { ( m ) }\) themultiplicative group of those \(x\) in \(\mathbf { K }\) such that \(v ( x - 1 ) \geq m\) (cf. Chap. IV, \(\ S 2\) Then,for \(m > e / \{ p 1 \} .\) the mapx→xpisan isomorphism of Umonto U(m+e).
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Example / comparison
ExAMPLES.i) If \({ \bf K } = { \bf Q } _ { p }\) with \(p \neq 2\) we can take \(m = \mathrm { ~ \mathfrak { k } ~ }\) and we see that \(\textrm { U } ^ { \{ \} } )\) is isomorphic to \(\mathbf { Z } _ { p }\) ; an element \(x\) of \(\mathfrak { U } ^ { \{ 1 \} }\) is a generator if and only if \(x\) does not belong to \(\mathbf { U } ^ { \{ 2 \} }\) \(x = 1 + p\) is an example.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 10
Proposition 10.With the hypotheses and notation of prop.9,assume further that \(\mathbf { K }\) isa finite extension of degree n of the feld \(\mathbf { Q } _ { p }\) .1f \(m > e / ( p - 1 ) ,\) then the group \(\mathbf { U } ^ { ( m ) }\) is \(\pmb { a }\) free \(\mathbf { Z } _ { p }\) moduleofrank \({ \pmb n } _ { \pmb { \imath } }\) and the group \(\mathbb { U } ^ { \lbrace \mathbb { 1 } \rbrace }\) isthe product ofa free \(\mathbb { Z } _ { p }\) moduleof ranknandacyclic group of orderapower f \(p\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Lemma 3
Lemma 3.Every element \(x\) of \(\mathbf { Z } _ { 2 }\) which is congruent to 1 mod.8 is a square.
Formalized. LeanCategories/Lattices/Valued/DyadicSymbol.lean::dyadicUnitClass_eq_one_iff; Mathlib/NumberTheory/Padics/RingHoms.lean::PadicInt.toZModPow — A dyadic unit is a square exactly when its residue modulo 8 is 1; an element congruent to 1 mod 8 is a unit, giving Serre’s lemma immediately.
Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280
Definition / construction
Let \({ \bf K } _ { s }\) be a separable closure of \(\kappa\) ,and let \(\mathrm { G } = \mathrm { G } \{ \mathrm { K } _ { s } / \mathrm { K } \}\) We have seen in Chap.X,$3 that everyelement \(a \in \mathbb { K }\) definesthomomorphism \(\varphi _ { a } \colon { \vec { \mathbf { G } } } \to { \vec { \mathbf { Z } } } / p { \vec { \mathbf { Z } } }\) as follows:we choose a root \(\propto\) in \({ \pmb X } _ { s }\) of the equation \(\wp ( \alpha ) = a ,\) and we set \(\varphi _ { a } \{ s \} = s \alpha - \alpha .\) f \(\begin{array} { r } { \psi _ { a } ( s ) = ( 1 / p ) \varphi _ { a } ( s ) , } \end{array}\) the map \(\psi _ { \alpha }\) is a homomorphism of G into the subgroup \(\{ 1 / p \} \mathbf { Z } / \mathbf { Z }\) of \(\mathbf { Q } / \mathbf { Z } ,\) ie.,acharacter of G.We know (loc.cit.) that the map \(a { \psi } _ { a }\) defines an isomorphism of \(\mathbb { K } / \wp ( \mathbb { K } )\) onto the group of those characters \(\psi\) of \(\mathbf { G }\) such that \(p \psi = 0 .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
Now let \(b \in \mathbb { K } ^ { * }\) According to the general definitions of \(\ S \Sigma\) ,we set \[ \{a, b\} = \{\psi_{a}, b\}, \] an element of \(B_{K}\) with \(p\{a,b\} = 0\).
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 11
Proposition 11. i \(\{ a + a ^ { \prime } , b \} = \{ a , b \} + \{ a ^ { \prime } , b \} .\) i） \([ a , b b ^ { \prime } ) = [ a , b \} + \{ a , b ^ { \prime } \}\) iiIn order that \([ a , b \} = \emptyset ,\) itisnecessary and sufficient that \(b\) bea norm in theextension \(\mathbb { K } ( \pmb { \mathscr { x } } ) / \mathbb { K }\) ,where \(\wp \{ \alpha \} = a\) iv） \([ a , a ) = 0\) forall \(a \in \mathbb { K } ^ { * }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Example / comparison
ExAMPLE.For \({ \pmb { p } } = 2 .\) the Severi-Brauer variety corresponding to \([ a , b \}\) is the conic having homogeneous equation \(x ^ { 2 } + x y + a y ^ { 2 } + b z ^ { 2 } = 0 .\) In particular, \([ a , b ) = 0\) if and only if this conic has a rational point in \(\mathbf { \ K }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
We now pass to the case where \(\mathbf { K }\) is the field \(k ( \{ t \} )\) offormal series over a feld \(k\) of characteristic \({ \pmb p } .\) If \(\omega = f\) dt isadifferential formofK,the coefficient of \(t ^ { - 1 }\) in \(f\) is called the residue of \(\omega\) ,and is denoted \(R e s ( \omega ) .\) It can be shown (cf.for example [56], Chap. I, prop.5’) that it does not depend on the choice of uniformiser t.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 12
Proposition 12. Let \({ \bf K } = k ( \{ t \} )\) where \(k\) isaperfect field of characteristic \(p \neq 0 ,\) 1f \({ a \in \mathbb { K } }\) and \(b \in \mathbb { K } ^ { \ast }\) ,let \(c = \operatorname { R e s } ( a d b / b ) \in k\) Then \[ \{ a , b \} = \{ c , t \} \quad i n \ \mathbf { B _ { \mathrm { K } } } . \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Example / comparison
ExAMPLE.If \(k\) isafinite fieldwith \(q = p ^ { f }\) elements,the map Sis given by the formula \[ \operatorname { S } ( x ) = x ^ { p ^ { f - 1 } } + x ^ { p ^ { f - 2 } } + \cdot \cdot \cdot + x ^ { p } + x = \operatorname { T r } _ { k \mid \operatorname { F } _ { p } } ( x ) . \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 13
Proposition 13.If α∈ K,isa root of the equation p(α)=a,andif sb=(b,*/K), then \[ \{ a , b \} _ { v } = s _ { b } \{ \alpha \} - \alpha . \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 14
Proposition 14. 1） \([ a + a ^ { \prime } , b \} _ { v } = [ a , b ) _ { v } + [ a ^ { \prime } , b \} _ { v } .\) ii \(\{ a , b b ^ { \prime } \} _ { v } + \{ a , b ^ { \prime } \} _ { v }\) ii） In order that \(\left[ a , b \right) _ { v } = 0 .\) it is necessary and sufficient that \(^ { b }\) be a norm in the extension \(\mathbf { K } ( \alpha ) / \mathbf { K }\) where \(\wp \left\{ \alpha \right\} = a\) 1 iv） \(\{ a , a \} _ { v } = 0\) for all \(a \in \mathbb { K } ^ { * }\) ， v） \([ a , b \} _ { v } 0\) for all \(\pmb { b } \in \mathbb { K } ^ { * }\) ,then \(a \in \wp \{ \mathrm { K } \} .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Lemma 4
Lemma 4. Let \(k\) bea quasi-finite field of characteristic \({ \mathfrak { p } } \neq { \mathfrak { g } } .\) Given \(x \in k ,\) let \(y \in k _ { s }\) beasolution to the equation \(\wp \left\{ y \right\} = x ,\) and let \(z = { \overrightarrow { \mathbf { F } } } y \cdots y\) Then \(z \in \mathbf { F } _ { p } = \mathbf { Z } / p \mathbf { Z } ,\) and \(\pmb { z }\) does not depend onthe choice of solution \(y ; i f\) we put \({ \tilde { \bf { S } } } \{ x \} = z ,\) then the map S defines by passage to the quotient an isomorphism of \(k _ { i } ^ { j } \wp ( k )\) onto \(\mathbf { Z } / p \mathbf { Z }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 15
Proposition 15. Let \(K = k \{ \{ t \} \}\) where \(k\) is a quasi-finite field of characteristic \(p\) 1f \(a \in \mathbb { K }\) and \(\boldsymbol { \mathfrak { b } } \in \mathbb { K } ^ { * }\) then \[ [ a , b \} _ { v } = \mathbf { S } \Bigg ( \mathbf { R e s } \Bigg ( a \frac { d b } { b } \Bigg ) \Bigg ) . \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary: Corollary
Corollary. If \(k\) is \(a\) finite field,then \([ a , b \} _ { v } = { \mathrm { T r } } _ { k / F _ { p } } ( { \mathrm { R e s } } ( a d b / b ) \} ) .\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Proposition 16
Proposition 16.Let ${ K } = { k } { { } ) $ ,where \(\pmb { k }\) is a quasi-finite field of characteristic \(p . f f\) an element \(\boldsymbol { b } \in \mathbb { K } ^ { \ast }\) is \(\pmb { a }\) norm in every cyclic extension of \(\mathbf { K }\) of degree \({ \pmb p } .\) then \(b \in { \mathbb { K } } ^ { * p }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Theorem 1
Theorem1.Every closed subgroupoffinite index in \(\aleph ^ { * }\) is anorm group (in the sense of Chap. XI, $ S 4 $
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary 1
Corollary 1.In order that a subgroup of finite index of \(\aleph ^ { * }\) be a norm group, it is necessary and sufficient that it contain \(\mathbb { U } _ { \mathbb { K } } ^ { \{ n \} }\) fornsufficiently large.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Corollary 2
Corollary 2 i） The intersection of the norm groups of \(\mathbf { K } ^ { \ast }\) is \(\left\{ \begin{array} { l } { \mathbf { \widehat { f } } \ \mathbf { \widehat { f } } } \\ { \mathbf { \widehat { t } } } \end{array} \right\}\) iif \({ \mathfrak { T } } _ { \mathbb { K } }\) denotes the inertia group of the maximal abelian extension \(K ^ { \alpha } / \mathbb { K }\) then thereciprocity map \(\mathbb { U } _ { \mathbb { K } } \to \mathfrak { T } _ { \mathbb { K } }\) isan isomorphism of topological groups (cf.Chap. XIII, \(\ S 3\) iii）The Galois group \(\mathfrak { A } _ { \mathtt { K } } = \mathbf { G } ( \mathbb { K } ^ { a } / \mathbb { K } )\) of the maximal abelian extension is an extension of \(\hat { \mathbf { Z } } \dot { b _ { \mathrm { F } } } \mathbf { U } _ { \kappa }\) ，
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
For a local function field, \(A_K^0\) is the subgroup of the maximal abelian Galois group inducing an integral power of Frobenius on \(K_{nr}\); with inertia open it is the modified Galois group, and reciprocity identifies \(K^*\) with it topologically.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
Let Kbe an algebraic number feld,i.e.,a finite extension of Q.Each absolute value v of \(\kappa\) determines acompletion \(\mathbb { K } _ { v }\) of \(\mathbf { K }\) for the topology defined by \(\pmb { v } ,\) These fields are of two types: for ultrametric v, \(\mathbf { K } _ { v }\) is a field of the sort considered in the preceding section,whereas for non-ultrametric \(v ,\) \(\mathbf { K } _ { v }\) is isomorphic to \(\pmb { \mathrm { R } }\) orto C.Note that local class field theory applies (trivially!）toRand to C;in particular,there isa“reciprocity isomorphism” \[ f : \mathbb { R } ^ { \star } / \mathbb { N } ( \mathbf { C } ^ { \star } ) \mathbb { G } ( \mathbf { C } / \mathbf { R } ) \] defined in an obvious way.
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Definition / construction
AnideleofKis,bydefinition,a family \(\left\{ x _ { \mathrm { p } } \right\}\) with \(\pmb { x } _ { s } \in { \mathbb { K } } _ { v } ^ { * }\) forall \({ \mathfrak { v } }\) but \(\boldsymbol { x } _ { v }\) beinga unit for almost all \(v ,\) The ideles formagroup \({ \bf { I } } _ { \bf { X } }\) under muitiplication；the multiplicative group \(\mathbf { K } ^ { \ast }\) embeds diagonally into \({ \bf \widehat { l } _ { X } }\)
Formalized. LeanCategories/Algebra/IdeleGroup.lean::FiniteIdeleGroup, IdeleGroup, principalIdele, principalIdele_injective — The project defines the restricted-product idèle group with local units at almost all finite places and the injective diagonal embedding Kˣ→I_K.
Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280
Definition / construction
For a finite abelian extension \(L/K\), the local reciprocity maps \(f_v:K_v^*/N L_w^*\to D_v\) are trivial on almost all idele components, so their product defines the global reciprocity map \(f:I_K\to G(L/K)\).
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Theorem: Theorem
Theorem. The map \(f\) issurjective,and its kernel is generated by \(\mathbf { K } ^ { \ast }\) and \(\ N _ { \mathbf { L } / \mathbb { K } } ^ { \sharp } \{ \mathbf { l } _ { \mathbf { L } } \}\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Theorem 2
Theorem 2. Let \(p\) beprime,and letEbe thefield obtainedbyadjoining all the roots of unity to \(\mathbf { Q } _ { p }\) Then \(\mathbf { \delta E }\) is the maximal abelian extension of \(\mathbf { Q } _ { p }\)
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.
Example / comparison
ExAMPLE.Take \(\mathbf { K } = \mathbf { Q } , n = 2\) and choose aand \(\pmb { b }\) to be distinct odd primes. By \(\ S 5\) we have \[ ( a , b ) _ { a } = { \binom { b } { a } } , \qquad ( a , b ) _ { b } = { \binom { a } { b } } , \quad \ldots ( a , b ) _ { 2 } = { \left( - 1 \right) } ^ { { \frac { a - 1 } { 2 } } { \frac { b - 1 } { 2 } } } , \]
Not formalized. The project has quadratic Q_p symbol calculations and idèles, but this full general local-symbol/existence-theorem statement is not available at Serre’s stated generality.