FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 12 definitions, 1 theorem, 18 propositions, 5 lemmas, 13 corollaries, 1 example and 5 conventions.
Of the 55 statements checked against Lean, 0 are formalized somewhere and 55 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 55 | 100% | A documented search found no Lean statement of it anywhere. |
| checked in total | 55 |
- Canonical source block: FC10 Serre Chapter 4, “Ramification Groups”,
FC10-C04-U001–FC10-C04-U055, 55 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 C04:
mathlib0,project-existing0,package-import0,reference-port0,unmatched55.
Convention / notation
Throughout this chapter,K denotesa field complete undera discrete valuation \(v _ { \mathbb { X } }\) .The corresponding valuation ring is denoted \(\mathbf { A } _ { \mathbf { K } }\) itsmaximal ideal \({ \mathfrak { p } } _ { \mathtt { K } }\) ,its residue field \(\bar { \mathbf { K } } = \mathbf { A _ { \mathbf { K } } } / \mathfrak { p _ { \mathbf { K } } }\) ,and \(\mathbf { U _ { K } } = \mathbf { A _ { K } } - \mathfrak { p _ { K } }\) the multiplicative group of invertible elements of \(\mathbf { A } _ { \mathbf { k } }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Convention / notation
If \(\mathbb { L }\) isa finite separable extension of K, \(\mathbf { A _ { 1 } }\) denotes the integral closure of \(A _ { k }\) in \(\mathbf { L }\) ;it isa complete discrete valuation ring (Chap. II, \(\ S 2\) prop. 3). We define \(v _ { \mathrm { L } } , \ { \mathfrak { p } } _ { \mathrm { L } } , \ \nabla _ { \mathrm { L } } , \ \mathrm { L }\) as above.We will always assume that the residue extension \(I / R\) isseparable.The ramification index of \(\mathfrak { P } _ { \mathtt { L } }\) in \(L / \mathbb { K }\) will be denoted \(e _ { k / \mathrm { K } }\) , and its residue degree \(f _ { \mathbf { L } / \mathbf { K } }\) ;we have \(e _ { \updownarrow ; \updownarrow \updownarrow } \cdot f _ { \updownarrow / \updownarrow } = \left[ \updownarrow ; \kappa \right]\) cf Chap.1, \(\ S 4\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Lemma 1
Lemma 1. Let \(\pmb { \mathscr { S } } \in \mathbb { G }\) and letibe an integer \(\geq - 1\) Then the three following conditionsareequivalent: a \(\mathfrak { s }\) operates trivially on the quotient ring \(\mathbf { A _ { i , \ell } } / { \mathfrak { p } _ { \downarrow , \ell } ^ { \mathrm { i + 1 } } }\) b \(v _ { \mathrm { L } } \{ s \{ a \} \ - \ a \} \geq i + 1\) for all \(a \in \mathbf { A } _ { \mathbf { L } }\) c \(v _ { \downarrow } \{ s \{ x \} - x \} \ge i + 1\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 1
Proposition1.For each integer \(i \geq - 1\) ,let \(\mathbf { G } _ { \mathfrak { f } }\) be the set of \(\pmb { s } \in \mathbb { G }\) satisfying conditionsa),b),c)of lemma 1.Then the \(\mathbf { G } _ { i }\) forma decreasing sequence of normal subgroups of \(\textbf { G }\) \(\mathbf { G _ { \lambda - 1 } } = \mathbf { G }\) \(\mathbf { G } _ { \mathfrak { d } }\) is the inertia subgroup of \(\mathbf { G }\) (cf Chap. 1, \(\ S 7\) ,and \(\mathrm { G } _ { i } \approx \{ 1 \}\) forisufficiently large.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
The group \(\mathbf { G } _ { i }\) is called the ith ramification group of \(\mathbf { G }\) (orof \(H _ { } / k \}\) .The ramification groups define a filtration of G (in the sense of Bourbaki,Alg. comm.,Chap.II,s2);the quotient \(\mathbf { G } / \mathbf { G } _ { \mathfrak { g } }\) is the Galois group \(\mathrm { G } \{ \vec { \bf L } / \vec { \bf K } \}\) ofthe residue extension (cf. Chap.I, \(\ S 7\) ；the quotients \(\mathbf { G _ { i } } / \mathbf { G _ { i + \delta t } }\) \(i \geq 0 .\) wifl be studied in the next section.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
Still denoting by \(x\) an \(\mathbf { A } _ { \mathbf { K } }\) generator of \(\mathbf { A } _ { \mathbf { I } , }\) ,we define a function \(i _ { G }\) on \(\textbf { G }\) by the formula \[ i _ { \mathrm { G } } ( s ) = v _ { \mathrm { L } } \{ s ( \boldsymbol { x } ) - { x } \} . \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 2
Proposition 2.For every \(s \in \mathbb { H }\) \(i _ { \mathbb { H } } \{ s \} = i _ { \mathbb { G } } \{ s \} ,\) and \(\hat { \mathbf { H } } _ { \mathrm { i } } = G _ { \mathrm { i } } \land \hat { \mathbf { H } } .\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary: Corollary.Let \(\mathbf { K } { \mathbf { r } }\) bethe largest unramified…
Corollary.Let \(\mathbf { K } _ { \mathbf { r } }\) bethe largest unramified subextension of \(\mathbf { L }\) over \(\mathbf { K }\) ,and let Hbe the corresponding subgroup of G.Then H is equal to the inertia group \(\mathbf { G _ { 0 } }\) ,and theramificationgroupsofGof index \(\geq 0\) are equal to those of \(\bf \delta H\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 3
Proposition 3.For every \(\sigma \in \mathbb { G } / \mathbb { H }\) \[ i _ { \mathrm { G } / \ H } ( \sigma ) = \frac { 1 } { e ^ { \prime } } \sum _ { s \pi } i _ { \mathrm { G } } ( s ) , \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary: Corollary
Corollary. if \(\mathbf { K } ^ { \prime }\) isa subextension of \(\mathbf { L } _ { i }\) corresponding to the subgroup H \(\mathbf { G }\) then \[ v _ { \kappa } \{ \mathfrak { D } _ { \kappa ^ { \prime } / \kappa } \} = \frac { 1 } { e ^ { \prime } } \sum _ { s \neq \mathrm { H } } i _ { \mathrm { G } } ( s ) , \quad w i t h \ e ^ { \prime } = e _ { \lfloor \kappa ^ { \prime } \cdot } \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
For a Dedekind domain \(A\), a finite Galois extension of its fraction field, and a prime \(\mathfrak P\) above \(\mathfrak p\), define the global ramification groups \(G_i(\mathfrak P)\) as the ramification groups of the completed extension; equivalently, \(s\in G_i(\mathfrak P)\) iff \(s(x)\equiv x\pmod{\mathfrak P^{i+1}}\) for every \(x\in B\).
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
Keeping the notation and hypotheses of section l,we denote by \(\mathsf { K } _ { \mathsf { r } }\) the largest unramified extension of \(\kappa\) contained in \(\texttt { L }\) (cf.cor. to prop.2).Denote by \(\pi\) a uniformizer ofL.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 4
Proposition 4. If \(\mathfrak { D } _ { \mathtt { L } / \mathtt { K } }\) denotes thedifferent of \(\mathbf { L } / \mathbb { K }\) ,then \[ v _ { \mathrm { L } } ( \mathfrak { D } _ { \mathrm { L } / \mathrm { K } } ) = \sum _ { s \neq 1 } i _ { \mathrm { G } } ( s ) \approx \sum _ { i \approx 0 } ^ { i \infty } ( \mathrm { C a r d } ( \mathrm { G } _ { i } ) - 1 ) . \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 5
Proposition 5.Let ibe a non-negative integer.In order that an element \(s\) of theinertia group \(\mathbf { G } _ { \mathfrak { g } }\) belong to \(\mathbf { G } _ { i }\) it isnecessary and sufficient that \[ s ( \pi ) / \pi \equiv 1 \ \mathrm { m o d . } \ \mathfrak { p _ { \mathrm { L } } ^ { i } } . \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Convention / notation
(Throughout the sequel, we will write \(\mathrm { \bf U _ { L } ^ { \it \ / i } }\) instead of \(\mathrm { U } _ { \ P _ { } } ^ { \{ i \} }\) ,except when there is a risk of confusion with the group of ith powers of elements of \(u _ { \downarrow }\) 1
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 6
Proposition 6. (a) \(\mathrm { U } _ { \mathbb { L } } ^ { 0 } / \mathrm { U } _ { \mathbb { L } } ^ { 1 } = \mathbb { E } ^ { * }\) (multiplicative group of the residue field L). \(( b )\) For \(i \geq 1\) the group \(\mathbb { E } _ { L } ^ { i } / \mathbb { U } _ { L } ^ { i + 1 }\) is canonicallyisomorphictothegroup \({ \mathfrak { p } } _ { \downarrow , i } ^ { i } { \mathfrak { p } } _ { \downarrow , } ^ { i + 1 }\) which is itself isomorphic (non-canonically)to theadditive group of theresidue field \(\mathbb { \bar { E } }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
Remark.The direct sum of the \(\mathfrak { p } _ { \mathtt { L } } ^ { \mathtt { i } } / \mathfrak { p } _ { \mathtt { L } } ^ { \mathtt { i } + \mathtt { i } }\) has a natural structure of graded \(\mathtt { E }\) -algebra (namely,thegraded algebraassociated to the \({ \mathfrak { p } } _ { 1 , \cdot }\) -adic filtration of \(A _ { k }\) cf.Bourbaki，Alg.comm.,Chap. III, \(\ S 2 )\) In particular, if we set \(\Omega _ { \tt L } = { \mathfrak { p } } _ { \tt L } / { \mathfrak { p } } _ { \tt L } ^ { 2 }\) then there is a canonical map of the ith tensor power \(\Omega _ { \mathrm { L } } ^ { i }\) of \(\Omega _ { \mathrm { L } }\) into \(p _ { 2 } ^ { i } / p _ { 2 } ^ { i + 1 }\) ; it is easy to see that this map is an isomorphism. Thus one can canonically identify \(\mathrm { U } _ { \mathrm { L } } ^ { i } / \mathrm { U } _ { \mathrm { L } } ^ { i + 1 }\) with \(\Omega _ { \mathrm { { L } } } ^ { i }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 7
Proposition 7.The map which,to \(\pmb { \mathscr { s } } \in \mathbf { G } _ { j }\) ,assigns \(s ( \pi ) / \pi\) induces by passage to thequotient an isomorphism \(\theta _ { i }\) ofthe quotient group \(\mathrm { G } _ { i } / \mathrm { G } _ { i + \textbf { i } }\) onto a subgroup of the group \(\mathrm { U } _ { \mathrm { L } } ^ { i } / \mathrm { U } _ { \mathrm { L } } ^ { i + 1 }\) Thisisomorphism is independent of the choice of uniformizer \(\mathfrak { X }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 1
Corollary1. The group \(\bf G _ { 0 } / G _ { 1 }\) is cyclic,and is mapped isomorphically by \(\theta _ { 0 }\) ontoa subgroup of the group of roots of unity contained in \(\mathbb { Z }\) Its order is primeto the characteristic of theresidue feld \(\mathbb { Z }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 2
Corollary 2. If the characteristic of \(\pmb { \updownarrow }\) is zero,then \(\mathbf { G } _ { \mathrm { : } } = \{ 1 \}\) ,and the group \(\mathbf { G _ { \mathfrak { g } } }\) is cyclic.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 3
Corollary 3.If the characteristic of \(\mathbf { L }\) is \(p \neq 0 ,\) the quotients \(\mathbf { G } _ { i } / \mathbf { G } _ { i + 1 }\) \(i \geq 1\) are abelian groups,and are direct products of cyclic groups of order \(p\) The group \(\mathbf { G _ { \lambda _ { 1 } } }\) isa \(p\) group.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 4
Corollary 4.If the characteristic of \(\mathbb { \bar { E } }\) is \(p \neq \emptyset\) the inertia group \(\mathbf { G } _ { \mathfrak { g } }\) has the following property: \(\{ \mathbb { R } _ { p } \}\) lt is the semi-direct product of a cyclic group of order prime to \(p\) with a normal subgroup whose order is a power of \(\pmb { p }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 5
Corollary 5.The group \(\mathbf { G } _ { \mathfrak { d } }\) is solvable.If \(\bar { \bf K }\) isa finite field,then G too is solvable.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 8
Proposition 8. Let \(\pmb { k }\) bean algebraically closed field of characteristic zero, and let \({ \bf K } = k ( \{ { \bar { \bf T } } \} )\) Then the algebraic closure \({ \bf K } _ { \pmb { \mathscr { a } } }\) of the field \(\pmb { \ K }\) is the union of the fields \({ \bf K } _ { n } = k ( ( { \bf T } ^ { 1 / n } ) )\) ,forintegral \(n \geq \sharp\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary
Corollary.The Galois group \(\tilde { \mathbf { G } } ( \mathbb { K } _ { a } / \mathbb { K } )\) is isomorphic to \(\hat { \pmb { z } }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 9
Proposition 9.1f \(\mathfrak { s } \in \mathbf { G } _ { \mathfrak { s } }\) and \(\mathfrak { t } \in \mathbf { G } _ { \mathfrak { i } } / \mathbf { G } _ { \mathfrak { i } + \mathfrak { i } } , \mathfrak { i } \geq \mathfrak { i } ,\) then \[ \begin{array} { r } { \theta _ { i } ( s \tau s ^ { - \frac { 1 } { 4 } } ) = \theta _ { 0 } ( s ) ^ { i } \theta _ { i } ( \tau ) . } \end{array} \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 1
Corollary 1. 1f \(\mathfrak { s e G } _ { \mathfrak { g } }\) and \(\pmb { \mathscr { t } } \in \mathbf { G } _ { \pmb { i } }\) \(i \geq 1\) then s \(\boldsymbol { \mathfrak { s } } ^ { - 1 } \boldsymbol { \mathfrak { t } } ^ { - 1 } \in \mathbf { G } _ { i + 1 }\) if and only if \(\ S ^ { \dot { \mathbf { f } } } \in \mathbb { G } _ { 1 }\) ：r \(\pmb { \mu } \in \pmb { \sigma } _ { i + \pmb { \updownarrow } }\) ，
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 2
Corollary 2.Suppose G is abelian,and let \(\scriptstyle { e _ { 0 } }\) be the order of \(\mathbf { G } _ { 0 } / \mathbf { G } _ { \frac { 1 } { 2 } }\) Then for any integer inot divisible by \(e _ { 0 }\) \(\mathbf { G } _ { \mathrm { i } } = \mathbf { G } _ { \mathrm { i + : } }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 10
Proposition 10. 1f \(s \in \mathbf { G } _ { i }\) \(t \in \mathbb { G } _ { j } .\) and \(i , j \ge 1\) then \(s t s ^ { - 1 } t ^ { - 1 } \in \mathrm { G } _ { i + j + 1 } .\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 11
Proposition 11. The integers \(i \geq 1\) such that \(\mathbf { G } _ { i } \neq \mathbf { G } _ { i + 1 }\) are all congruent to one another mod. \(p\) (where \(\pmb { p }\) is the characteristic of the residue field L.)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Lemma 2
Lemma 2. With the hypotheses of prop.10,we have sts \(\cdot ^ { - 1 } t ^ { - 1 } \in G _ { i + j }\) and \[ \theta _ { i + j } ( s t s ^ { - 1 } t ^ { - 1 } ) = ( j - i ) \theta _ { i } ( s ) \theta _ { j } ( t ) . \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
We keep the notation and hypotheses of the two preceding sections.If \(\pmb { u }\) is a real number \(\geq - \mathrm { \Large ~ \frac { 4 } { 4 } , ~ G } _ { u }\) denotes the ramification group \(\mathbf { G } _ { i }\) ,where \(\pmb { \dot { \ell } }\) is the smallest integer \(\geq u ,\) Thus Put \[ s \in \mathrm { G } _ { u } \Leftrightarrow i _ { \mathrm { G } } ( s ) \geq u + 1 . \] \[ \underset { : \times _ { \ast } } { \varphi } \{ u \} = \int _ { 0 } ^ { u } \frac { d t } { \{ G _ { 0 } : G _ { t } \} } . \] When \(- 1 \leq t \leq 0 ,\) our convention is that \(\{ \mathbf { G } _ { 0 } : \mathbf { G } _ { t } \}\) is equal to \(\{ \mathbf { G } _ { - 1 } : \mathbf { G } _ { 0 } \} ^ { - 1 }\) for \(t = - 1\) and is equal to \(1 = \{ \mathbf { G } _ { 0 } : \mathbf { G } _ { 0 } \} ^ { - 1 }\) for \(- 1 < t \leq 0\) The function \(\phi ( u )\) is thus equal to \(\mathfrak { u }\) between \(\mathbf { \Phi } - \mathbf { \hat { i } }\) and 0.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
[When we need to specify the extension \(\mathbf { \mu } _ { \mathbf { L } / \mathbf { K } }\) ,we write \(\varphi _ { \pm , / \ K }\) instead of \(\varphi . \}\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 12
Proposition 12 a)The function \(\wp\) is continuous,piecewise linear,increasing,and concave. b \(\varphi ( 0 ) = 0 ,\) cIf we denote by \({ \varphi } _ { d } ^ { \prime }\) and \({ \varphi } _ { g } ^ { \prime }\) therightandleftderivativesof \(\varphi\) ,then \[ \varphi _ { g } ^ { \prime } ( u ) = \varphi _ { d } ^ { \prime } ( u ) = 1 / \{ \mathbf { G } _ { 0 } : \mathbf { G } _ { u } \} \] \[ \begin{array} { r l } & { \psi _ { g } ( u ) = \psi _ { d } ( u ) = \mathbf { 1 } / ( \mathbf { V } _ { 0 } \cdot \mathbf { V } _ { u } ) \quad y ~ a ~ \textit { s n o t } a n ~ t r a v e r , } \\ & { \varphi _ { g } ^ { \prime } ( u ) = \mathbf { 1 } / ( \mathbf { G } _ { 0 } ; \mathbf { G } _ { u } ) , \qquad \varphi _ { d } ^ { \prime } ( u ) = \mathbf { 1 } / ( \mathbf { G } _ { 0 } ; \mathbf { G } _ { u + 1 } ) \quad i f ~ u ~ i s ~ a n ~ i n t e g e r . } \end{array} \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Convention / notation
The verification is immediate. Note that these properties characterise \(\phi\) The map \(\varphi\) isa homeomorphism of the half-line \([ - 1 , + \infty ]\) onto itself. Denote by \(\psi\) (or \(\psi _ { \pm / \kappa } \}\) the inverse map.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 13
Proposition 13 a） The function \(\psi\) is continuous,piecewise linear,increasing and convex. b \(\psi ( 0 ) = \emptyset .\) cif \(v = \phi ( u ) ,\) then \(\psi _ { g } ^ { \prime } ( v ) = 1 / \varphi _ { g } ^ { \prime } ( u ) , \psi _ { d } ^ { \prime } ( v ) = 1 / \varphi _ { d } ^ { \prime } ( u ) .\) (In particular, \({ \psi } _ { \mathfrak { s } } ^ { \prime }\) and \(\psi _ { d } ^ { \prime }\) onlytakeon integervalues.) d \(1 1 0\) is an integer,so is \(u = \psi ( v )\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
The upper numbering is defined by \(G^v=G_{\psi(v)}\), equivalently \(G^{\varphi(u)}=G_u\), where \(\psi=\varphi^{-1}\).
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 14
Proposition 14. 1f \(\mathbf { H }\) is \(\pmb { \mathrm { a } }\) normal subgroup of G,then \(\{ \mathrm { G / H } \} ^ { \mathrm { s } } = \mathrm { G } ^ { \mathrm { s } } \mathrm { H } / \mathrm { H }\) for al \(\imath\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 15
Proposition 15.The functions \(\varphi\) and \(\psi\) satisfy the transitivity formulas: \[ \varphi _ { \downarrow / \kappa } = \varphi _ { \kappa ^ { \prime } / \kappa } \circ \varphi _ { \downarrow / \kappa } , a n d \quad \psi _ { \downarrow / \kappa } = \psi _ { \downarrow , \downarrow \kappa ^ { \prime } } \circ \psi _ { \kappa ^ { \prime } / \kappa } . \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Lemma 3
Lemma 3. φL/k(u）= \(\varphi _ { \mathrm { L } / \mathcal { K } } ( u ) = \frac { 1 } { g _ { 0 } } \sum _ { s \in \mathbb { G } } \operatorname { I n f } ( i _ { \mathrm { G } } ( s ) , u + 1 ) - 1 .\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Lemma 4
Lemma 4. Let \(\sigma \in { \mathbb G } / { \mathbb H }\) and let \(j \{ \sigma \}\) be the upper bound of the integers \(i _ { G } \{ s \}\) as srunsthrough thepre-image of \(\pmb { \sigma }\) inG.Then \[ i _ { \mathrm { G / H } } ( \sigma ) - 1 = \varphi _ { \mathrm { L / K } ^ { \prime } } ( j ( \sigma ) - 1 ) . \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Lemma 5
Lemma 5. If \(\mathfrak { r } = \phi _ { \mathfrak { L } / \mathbb { K } } \cdot \{ \mathfrak { u } \}\) then \(\mathrm { G } _ { u } \mathrm { H } / \mathrm { H } = \left( \mathrm { G } / \mathrm { H } \right) _ { t s } .\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
For an infinite Galois extension, the upper ramification groups \(G^v\) are defined by inverse limit over finite Galois subextensions.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
A real number \(v\) is a jump of the upper ramification filtration if \(G^v\ne G^{v+\varepsilon}\) for every \(\varepsilon>0\).
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
- Let E be a subextension of the Galois extension \(L / \kappa\) (the latter having separable residue extension,as always).Define \(\varphi _ { \mathtt { E } / \mathtt { K } }\) to be \(\varphi _ { \downarrow , i \& } \circ \psi _ { \downarrow , i \in }\) ；prop. 15shows that this definition is independent of the extension \(\mathbf { E }\) chosen and that the \(\varphi _ { \mathbb { E } / \mathbb { K } }\) satisfy the same transitivity formulas as the \({ \varphi } _ { \mathbb { L } / \mathbb { K } }\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition: Proposition l6.Let K be a field complete under a discrete valuation,and…
Proposition l6.Let K be a field complete under a discrete valuation,and having finite residue field \(k = \mathbb { F } _ { q }\) with \(q = p ^ { f }\) Given an integer n prime to \(\mathfrak { p }\) Let \({ \bf K } _ { \pi }\) (resp. \(k _ { n } )\) bethefieldobtainedbyadjoiningtoK(resp. \(k )\) thenthroots of unity.The field \(\mathbb { K } _ { \mathfrak { n } }\) isanunramified extension of K and hasresidue field \(k _ { \pi }\) 1f \(5\) is \(\pmb { \mathcal { a } }\) primitive nth root of unity,then \(\mathbf { A } _ { \mathbf { K } _ { n } } = \mathbf { A } _ { \mathbf { K } } \mathbf { [ } \boldsymbol { \zeta } \mathbf { ] }\) The Galois group \(G ( K _ { n } / \mathbb { K } )\) can be identified with the group \(\operatorname { G } ( { k _ { \mathfrak { n } } } / { k } )\) ; it is cyclic, generated by anautomorphism s such that \(s \{ z \} = z ^ { q }\) forevery nth root of unity z.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 1
Corollary1.Thedegree \([ K _ { n } ; \mathbb { K } ]\) is equal to the smallest integer \(\gamma \geq \mathbf { f }\) such that \(q ^ { r } \equiv 1\) mod.n.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary 2
Corollary 2. The maximal unramified extension \(K_{nr}/K\) is obtained by adjoining to \(K\) all roots of unity of order prime to \(p\).
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Definition / construction
where \(\mathbf { L }\) runs through the set of finite subextensions of a given Galois extension \(E / \mathbf { K }\) An element \(\pmb { \ell }\) of \(\boldsymbol { \mathsf { T } }\) is by definition a system \(\{ t _ { \mathbb { L } } \} _ { \sharp _ { \ell } } \subset \mathbb { E } \} _ { \sharp _ { \ell } }\) with \(t _ { 1 } \in T _ { 1 }\) and \(\varphi _ { \mathtt { t } , \mathtt { l } , \mathtt { l } } . \{ t _ { \mathtt { l } , } \} = \mathfrak { t } _ { \mathtt { L } }\) if \(\mathbf { L } \supset \mathbf { \bar { L } } ^ { \prime }\) if now \(\mathbf { G }\) is the Galois group of an extension \(\mathbf { L } / \mathbf { L } ^ { \prime }\) ,put \[ \mathrm { G } ( t ) = \mathrm { G } _ { t _ { \mathrm { L } } } = \mathrm { G } ^ { t _ { \mathrm { L } } } , \quad \mathrm { f o r ~ a l l ~ } t \in \mathbb { T } . \] IfH is a subgroup of \(\mathbf { G } _ { \mathbf { \lambda } }\) then \(\mathrm { H } ( t ) = \mathrm { H } \cap \mathrm { G } ( t )\) andif \(\mathbf { H }\) is normal, \(\{ \mathbf { G } / \mathbf { H } \} ( t ) =\) \(\mathrm { G } \{ \mathfrak { t } \} \mathrm { H } / \mathrm { H }\) ：the indexing of theramifcation groups byTiscompatible both with passage to a subgroup and with passage to a quotient group.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Theorem: Theorem (Hasse-Arf).If G is an abelian group,and \(i j ^ { \star }\) v is a…
Theorem (Hasse-Arf).If G is an abelian group,and \(i j ^ { \star }\) v is a jump in the filtration \(\vec { \mathbf { U } } ^ { \mathfrak { r } }\) then \(v\) is an integer.
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Example / comparison
ExAMPLE.Suppose G is cyclic of order \(p ^ { \# } .\) where \(p\) is the characteristic of \(R _ { s }\) and let \(\mathbf { G } \{ i \}\) be the subgroup of \(\mathbf { G }\) of order \(p ^ { \pmb { \imath } - \pmb { i } }\) The theorem of Hasse-Arf means that there exist strictly positive integers \[ i _ { 0 } , i _ { 1 } , \dotsc , i _ { n - 1 } , \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 17
Proposition 17. Let \(K _ { n }\) be the field obtained from \(\mathbf { K } = \mathbf { Q } _ { p } \mathrm { ~ } b \mathbf { y }\) adjoining a primitite nth root of unity \(\zeta .\) with \(n = p ^ { \ m }\) Then i \([ \mathsf { K } _ { n } ; \mathsf { K } ] = \varphi ( n ) = ( p - 1 ) p ^ { m - 1 }\) iiThe Galois group \(\mathrm { G } ( \mathbb { K } _ { n } / \mathbb { K } )\) can be identified with the group \(\mathrm { G } ( \mathfrak { n } )\) invertibleelementsin thering \(\mathbf { Z } / \mu \mathbf { Z }\) ii \(\ K _ { \mathfrak { n } }\) is a totally ramified extension of \(\aleph\) The element \(\pi = \zeta - 1\) is \(a\) uni formizer of \(\mathsf { K } _ { \mathfrak { n } }\) ,and \(A _ { k _ { 1 } } = A _ { k } [ ( \zeta ]\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Convention / notation
We now determine the ramification groups of \(\mathrm { G } = \mathrm { G } ( \mathbb { K } _ { \eta } / \mathbf { K } )\) If \(\smash { t ^ { \gamma } }\) is an integer, \(0 \leq \mathfrak { r } \leq m .\) denoteby \(\mathbf { G } \{ \pmb { \mathscr { n } } \} ^ { * }\) the subgroup of \(G ( \mathfrak { n } )\) consisting of all elements \(^ { g }\) such thal \(a \equiv 1 { \mathrm { ~ m o d . } } p ^ { \prime }\) The group \(\mathrm { G } \{ \eta \} / \mathrm { G } \{ n \} ^ { \ast }\) can be identified with the group \(\operatorname { G f } { \mathfrak { p } } ^ { \mathrm { r } } { \mathfrak { f } } _ { \mathfrak { z } }\) i.e.,with the Galois group of the extension \({ \sf K } _ { p } , { \sf K }\) Thus \(\begin{array} { r } { \mathrm { G } ( n ) ^ { * ! } = \mathrm { G } ( \mathrm { K } _ { n } / \mathrm { K } _ { p ^ { v } } ) } \end{array}\)
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Proposition 18
Proposition 18. The ramification groups \(\mathbf { G } _ { \# }\) f \(\mathrm { { G } } \{ \mathsf { K } _ { \mathfrak { n } } / \mathsf { K } \}\) are: \[ \begin{array} { c c c } { { } } & { { } } & { { \mathrm { G } _ { 0 } = \mathrm { G } , } } \\ { { i f ~ \updownarrow \leq u \leq p - 1 , } } & { { } } & { { \mathrm { G } _ { u } = \mathrm { G } ( n ) ^ { 1 } } } \\ { { i f ~ p \leq u \leq p ^ { 2 } - 1 , } } & { { } } & { { \mathrm { G } _ { u } = \mathrm { G } ( n ) ^ { 2 } } } \\ { { : } } & { { } } & { { \vdots } } \\ { { i f ~ p ^ { m - 1 } \leq u , } } & { { } } & { { \mathrm { G } _ { u } = \mathrm { G } ( n ) ^ { m } = \{ 1 \} . } } \end{array} \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.
Corollary: Corollary The jumps in the filtration \(( \pmb { G } ^ { } )\) are integers
Corollary The jumps in the filtration \(( \pmb { G } ^ { * } )\) are integers. Moreover, and \[ \begin{array} { r } { \mathbf { G } ^ { v } = \mathbf { G } ( n ) ^ { v } \quad f o r \ 0 \leq v \leq m , } \\ { \mathbf { G } ^ { v } = \lbrace 1 \rbrace \quad f o r \ v \geq m . } \end{array} \]
Not formalized. Pinned and current Mathlib explicitly leave higher ramification groups in lower numbering as TODO; no checked compatible source closes this Serre row.