FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 14 definitions, 8 theorems, 10 propositions, 2 lemmas, 10 corollaries, 4 examples and 3 conventions.
Of the 51 statements checked against Lean, 9 are formalized somewhere and 42 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 42 | 82% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 9 | 18% | Mathlib states and proves it. |
| checked in total | 51 |
- Canonical source block: FC10 Serre Chapter 2, “Completion”,
FC10-C02-U001–FC10-C02-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 C02:
mathlib9,project-existing0,package-import0,reference-port0,unmatched42.
Definition / construction
For a discrete valuation \(v\) and a real number \(0<a<1\), define \(|x|=a^{v(x)}\) for \(x\ne0\) and \(|0|=0\); this is an ultrametric absolute value.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
For \(v\) discrete, let \(\widehat{K}\) be the completion of \(K\) for the topology defined by its absolute value; the topology does not depend on the choice of the number \(a\). Then \(\widehat{K}\) is a valued field whose absolute value extends that of \(K\).
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 1
Proposition 1.In order that K be locally compact,it is necessaryand sufficient that itsresidue field \(\bar { \mathbf { K } } = \mathbf { A } / \pi \mathbf { A }\) bea finite field andKbe complete.
Formalized. Mathlib/NumberTheory/LocalField/Basic.lean::compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField — For a discretely valued field, local compactness is equivalent to completeness plus finite residue field.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example / comparison
EXAMPLES.1)The field \(\mathbf { Q } _ { p }\) ,completion of Q for the topology defined by the \(p\) -adic valuation,isa locally compact field with residue field \(\mathbf { F } _ { p }\) 1
Formalized. Mathlib/NumberTheory/Padics/PadicIntegers.lean; Mathlib/NumberTheory/Padics/RingHoms.lean::PadicInt.toZMod_eq_residueField_comp_residue; Mathlib/NumberTheory/LocalField/Basic.lean — The p-adic field is complete and locally compact, with p-adic integers and residue field F_p.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
When the residue field has \(q\) elements, the normalized absolute value is the one obtained by taking \(a=q^{-1}\) in \(|x|=a^{v(x)}\).
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 2
Proposition 2.Let K be a field satisfying the conditions of prop.1,and let \(\mu\) bea Haar measure on the locally compact additive group underlying K.Then foreverymeasurable subset \(\mathbf { E }\) f \(\mathbf { K }\) and every \({ \pmb x } \in { \pmb K }\) one has \[ \mu \{ x \mathbf { E } \} = \{ | x | \} \mu ( \mathbf { E } ) , \] where \(\left\{ \left\} \times \right\} \right\}\) denotes the normalised absolutevalue of \(x\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 1
Corollary 1. 1f \(e\) (resp. \(f \}\) denotes the ramification index (resp.the residue degree)ofL over \(\mathbf { K }\) ,then ef \(\approx n\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 2
Corollary 2. There is a unique valuation w of L that prolongs v.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 3
Corollary 3.Two elements of L that are conjugate over K have the same valuation.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 4
Corollary4.For every \(x \in \mathbb { L }\) \(, w ( x ) = ( 1 / f ) v ( \mathbb { N } _ { \mathrm { L } / \mathsf { K } } ( x ) ) .\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 3
Proposition 3.Let K be a field on which a discrete valuationv is defined, havingvaluation ringA.AssumeKto be complete in the topologydefined by \(v\) Let \(\mathbf { { L } } / \mathbf { { K } }\) bea finite extension ofK,and let B be the integral closure of AinL (cf.Chap.I,$4).ThenBisadiscrete valuationringand isa free A-module of rank \(n = [ 1 , \pm , \pm ]\) ;also, \(\mathbb { L }\) iscomplete in the topology defined byB.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
In terms of absolute values, corollary 4 says that the topology of \(L_{+}\) can be defined by the norm \[ \|x\|_{L} = \|N_{L/K}(x)\|_{K}. \] If \(K\) is locally compact and \(\|\cdot\|_{K}\) is normalised, so is \(\|\cdot\|_{L}\). This formula may instead be taken as the definition of \(\|\cdot\|_{L}\), at the cost of proving directly that it is an ultrametric absolute value.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Theorem 1
Theorem 1. Let \(L / \mathbb { K }\) be an extension of finite degree n,va discrete valuation ofKwith ring A,and B the integral closure of A inL.Suppose that the AmoduleBis finitely generated.Let \(\mathfrak { w } _ { i }\) be the different prolongations ofvtoL, and let \(e _ { i } , f _ { i }\) be the corresponding numbers (cf.Chap.I,S4).Let \(\hat { \bf K }\) and \(\widehat { \mathbf { L } } _ { i }\) be the completions of \(\aleph\) and \(\pmb { \downarrow }\) for v and the \(\mathbf { w _ { i } }\) ， (i The field \(\hat { { \mathbb L } } _ { i }\) is an extension of \(\mathbf { K }\) of degree \(n _ { \mathrm { i } } = e _ { i } f _ { \mathrm { i } }\) (ii） The valuation \(\hat { \ w } _ { i }\) is the unique valuation of \(\widehat { \mathbb { L } } _ { i }\) prolonging \({ \widehat { \mathfrak { v } } } ,\) and \[ e _ { i } = e ( \hat { \mathbb { L } } _ { i } / \hat { \mathbb { R } } ) \quad a n d \quad f _ { i } = f ( \hat { \mathbb { L } } _ { i } / \hat { \mathbb { K } } ) . \] (ii)The canonical homomorphism \(\varphi : \mathbb { L } \otimes _ { \mathbb { K } } \hat { \mathbb { K } } \to \prod _ { i } \hat { \mathbb { L } } _ { i }\) is an isomorphism.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 1
Corollary 1.The felds \(\widehat { \mathbb { L } } _ { i }\) are the composites of the extensions \(\hat { \bf K }\) and L of K.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 2
Corollary 2.1f \(x \in \mathbb { L } ,\) the characteristicpolynomial \(\boldsymbol { \mathsf { F } }\) of \(x\) in \(\mathbb { L } / \mathbb { K }\) is equal to theproductof the characteristic polynomials \(\mathbf { \hat { F } } _ { i }\) of \(x\) in the \(E _ { i } / / R\) Inparticular, \(i f\) Tr and \(\mathbf { M }\) (resp. \(\mathbb { T } _ { i }\) and \(\mathbf { N _ { j } }\) denote the trace and norm in \(\mathbf { L } / \mathbf { K }\) (resp.in \([ \hat { \bf \Xi } _ { i } / \hat { \bf K } \}\) then \[ \mathrm { T r } ( x ) = \sum \mathrm { T r } _ { i } ( x ) , \qquad \mathrm { N } ( x ) = \prod \mathrm { N } _ { i } ( x ) . \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 3
Corollary 3.1f \(L / \mathbb { K }\) is separable (in which case the finiteness hypothesis made onB is automatically satisfied),the \([ \hat { \bf \Phi } _ { i } / \hat { \bf K }\) are also.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary 4
Corollary 4.1f \(\mathbf { L } / \mathbf { K }\) is Galois with group \(\mathbf { G }\) andif \(\mathbf { D _ { i } }\) denotes the decomposition group of \(w _ { i }\) in \(\mathbf { G }\) (cf. Chap. I, \(\ S 7 )\) ,the extension \(\hat { \mathbb { L } } _ { i } / \hat { \mathbb { K } }\) is Galois with Galois group \(\mathbf { D _ { i } }\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 4
Proposition 4.With the hypothesesand notation of theorem1,let \(\mathbf { B } _ { i }\) be the ringof the valuation \(w _ { i }\) Thecanonical homomorphism \[ \varphi : \mathbb { B } \otimes _ { \mathbb { A } } \hat { { \mathbb { A } } } \to \prod _ { i } \hat { { \mathbb { B } } } _ { i } \] is then an isomorphism.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 5
Proposition5.Every element \(a \in \mathsf { A }\) can be written uniquely as a convergent series \[ a = \sum _ { n \mathop { \approx } 0 } ^ { \infty } s _ { n } \pi ^ { n } , \quad w i t h s _ { n } \in \mathbb { S } . \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Example / comparison
ExAMPLE. If \(\mathbf { A } = \mathbf { Z } _ { p } .\) one may take S to be the set of non-negative integers less than \(p\) ;one may also-and this is preferable-take S to consist of O and the \(( p - 1 ) s t\) roots of unity;cf. prop.8.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Theorem 2
Theorem2.Let A bea complete discrete valuation ring with residue field K. Suppose that A and \(\bar { \bf K }\) have the same characteristic and that \(\pmb { \mathrm { \widehat K } }\) isperfect. Then A is isomorphic to \(\mathbb { K } \{ [ \mathbf { T } ] \}\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 6
Proposition6.Let A bea local ring that is Hausdorff and complete for the topologydefined by a decreasing sequence \(a _ { 1 } > a _ { 2 } = \cdots\) ofideals such that \({ \mathfrak { a } } _ { \mathfrak { n } } \cdot { \mathfrak { a } } _ { m } \subset { \mathfrak { a } } _ { \mathfrak { n } + m }\) Suppose that \(\bar { \mathbf { K } } = \mathbf { A } / \bar { \mathbf { a } } _ { 1 }\) isafield of characteristic zero.Then Acontainsasystem ofrepresentatives of \(\vec { \bf K }\) whichisa field.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 7
Proposition7.Let A bea local ring that is Hausdorff and complete for the topology defined bya decreasing sequence \({ \mathfrak { a } } _ { \mathfrak { g } } \supset { \mathfrak { a } } _ { \mathfrak { z } } \supset \cdots\) of ideals such that \({ \mathfrak { Q } } _ { n } \cdot { \mathfrak { a } } _ { m } \subset { \mathfrak { a } } _ { n + m }\) Suppose that \({ \mathfrak { a } } _ { \mathfrak { s } }\) isthemaximal ideal ofA,and let \(\Ddot { \mathbf { K } } = \mathbf { A } / \mathfrak { a _ { i } }\) Let \(f ( \mathbf { X } )\) bea polynomial with coeffcients in A such that thereduced polynomial \(\vec { j } \in \mathbb { K } \{ \mathbf { X } \}\) has a simple root \(\lambda\) in \(\pmb { \mathbb { X } }\) Then \(f\) has a unique root \(x\) in A such that \(\overline { { x } } = \lambda\) 1
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
Wewill say thata ring \(\varLambda\) ofcharacteristic \(p\) is perfect if the endomorphism \(x \to x ^ { p }\) of \(\pmb { \mathscr { A } }\) isanautomorphism(i.e.,is surjective).Every element \(x \in { \cal { A } }\) then hasa unique pth root,denoted \(x ^ { p ^ { - 1 } }\) When \(\pmb { \mathscr { A } }\) isa field,this is the usual definition ofaperfect field.
Formalized. Mathlib/FieldTheory/Perfect.lean::PerfectRing — Mathlib’s PerfectRing is the source Frobenius-surjectivity condition in characteristic p.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 8
Proposition8.Let Abea ring that is Hausdorff and complete for the topology defined by a decreasing sequence \({ \mathfrak { a } } _ { 1 } = { \mathfrak { a } } _ { 2 } \supset \cdots\) of ideals such that \(a _ { n } \cdot a _ { m } =\) \(\Omega _ { m + m }\) Assume that the residue ring \(\bar { \mathbf { K } } = \mathbf { A } / \mathbf { a _ { \mathrm { ~ t ~ } } }\) is aperfect ring of characteristic \(p\) Then: (i) There exists one and only one system of representatives \(f : \bar { \mathbb { K } } \to \mathbb { A }\) which commutes with pth powers: \(f ( \lambda ^ { p } ) = f ( \lambda ) ^ { p }\) (i） In order that \(a \in \mathbb { A }\) belongto \(\mathsf { S } = f ( \overrightarrow { \mathsf { K } } )\) it isnecessary and sufficient that abea \(p ^ { \ast }\) thpowerforall \(n \geq 0\) (iii)This system of representatives ismultiplicative,i.e.,one has \(f ( \lambda \mu ) =\) \(f ( \lambda ) , f ( \mu )\) forall） \(\mu \in \bar { \mathbb { K } }\) (iv） \(I f\) A has characteristic \(p\) thissystem of representatives isadditive,i.e., \(f ( \lambda + \mu ) = f ( \lambda ) + f ( \mu ) .\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Lemma 1
Lemma 1. 1f \(a \equiv b\) mod. \({ \mathfrak { a } } _ { \mathfrak { n } }\) ,then \(a ^ { p } \equiv b ^ { p }\) mod. \(\mathfrak { a } _ { \mathfrak { s } ^ { + } \mathfrak { t } }\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
The system of representatives of prop.8 is called the multiplicative system ofrepresentatives,because of property (iii).
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
LetA bea complete discrete valuation ring,with field of fractions \(\mathbf { K }\) and residue field \(\vec { \bf K }\) Suppose that the characteristics of Aand \(\pmb { \mathrm { K } }\) are different, i.e., that A has characteristic zero and \(\pmb { \ K }\) has characteristic \(p \neq 0 .\) One can then identify \(\mathbf { z }\) with a subring of A,and \({ \pmb { p } } \in { \pmb { Z } }\) with an element of A. Since \(p\) goes to zero in \(\bar { \bf K }\) one has \(v \{ p \} \ge 1\) ,where \({ \pmb v }\) is thediscrete valuationattached to A.The integer \(e = v _ { \parallel p } )\) is called the absolute ramification index of A. Observe that the injection \(\mathbf { Z } \to \mathbf { A }\) extends by continuity to an injection of the ring \(\mathbf { Z } _ { p }\) of \(p\) adic integers into A;when the residue field \(\pmb { \mathrm { R } }\) is a finite field with \(q = { \dot { p } } ^ { f }\) elements,prop.S shows that A isa free \(\mathbf { Z } _ { p }\) module of rank \(n = e f\) and \(\kappa\) is an extension of degree n of the \(\pmb { p }\) adic field \(\mathbf { Q } _ { p }\) ; the integer \(e\) can then be interpreted as the ramification index of the extension \({ \bf K } / { \bf Q } _ { p }\) which justifies the terminology.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
A complete discrete valuation ring of unequal characteristic is absolutely unramified when its absolute ramification index \(e=v(p)\) equals \(1\), equivalently when \(p\) is a uniformizer.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Theorem 3
Theorem 3.Forevery perfect fieldkof characteristic \({ p } _ { 1 }\) there existsa complete discrete valuation ring and only one \(\scriptstyle ( u p\) tounique isomorphism） which is absolutelyunramifiedandhas \(\pmb { k }\) as itsresidue field.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Convention / notation
For a perfect field \(k\) of characteristic \(p\), the unique absolutely unramified complete discrete valuation ring with residue field \(k\) is denoted \(W(k)\).
Formalized. Mathlib/RingTheory/WittVector/Basic.lean::WittVector — Mathlib’s p-typical Witt vectors are the ring denoted W(k) by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 4
Theorem4.Let A be a complete discrete valuationring of characteristic unequal to that of itsresidue field \(k\) Lete be its absolute ramification index. Then there existsaunique homomorphismof \(\mathbf { W } ( k )\) into A which makes commutative the diagram: \[ \begin{array} { r } { \mathbb { W } \{ k \} \to \mathrm { A } } \\ { \searrow _ { k } \swarrow } \end{array} \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
A filtered ring satisfying the hypotheses of Proposition 8 is called a \(p\)-ring.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
A \(p\)-ring is strict when its filtration is the \(p\)-adic filtration and \(p\) is not a zero-divisor.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
converges to an element \(a \in \mathbb { A }\) When A is strict,one sees by arguing as in prop.5,that every element \(a \in \mathsf { A }\) can be uniquely expressed in the form of a series of type \(( \# \# )\) ；the \({ \mathfrak { X } } _ { i }\) which occur in this series will be called the \(c o \ast\) ordinates of \(a\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Example / comparison
EXAMPLE OFA STRICT \(p\) -RING. Let \(\mathbf { X } _ { \alpha }\) beafamily of indeterminates,and let S be the ring of \(p ^ { \lnot \infty }\) -polynomials in the \(\mathbf { X } _ { \pmb { \alpha } }\) with integer coefficients,i.e., the union of the rings \(\mathbf { Z } _ { 1 } ^ { \mathrm { f } } \mathbf { X } _ { \alpha } ^ { p - \mathrm { a } } \}\) for all \(\pmb { n } _ { + }\) If one provides S with the \(p\) -adic fitration \(\{ p ^ { n } \mathbf { S } \} _ { \mathfrak { n } \geq \mathfrak { Q } }\) and completes it, one obtains a strict \(\pmb { p }\) ring that will be denoted \(\hat { \pmb { \mathsf { S } } } = \hat { \pmb { \sf z } } \{ \pmb { \mathrm { X } } _ { \alpha } ^ { p - \infty } ]\) The residue ring \(\hat { \bf S } / p \hat { \bf S }\) is the ring \(\mathbb { F } _ { p } [ \mathbf { X } _ { \alpha } ^ { p ^ { - } } ]\) ; it is perfect of characteristic \(\pmb { p }\) Note that the \({ \bf { X } } _ { \pmb { x } }\) aremultiplicative representatives in S since they admit p’th roots for all \(\pmb { n }\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 9
Proposition 9.Let A be a \(p\) ringwith residue ring \(k\) and let \(f : k \Lambda\) be the system of multiplicativerepresentatives in A.Let \(\{ x _ { i } \}\) and \(\{ \beta _ { i } \}\) be two sequences of elementsof \(k\) Then \[ \sum _ { i = 0 } ^ { \infty } f ( \alpha _ { i } ) \cdot p ^ { i } \ast \sum _ { i = 0 } ^ { \infty } f ( \beta _ { i } ) \cdot p ^ { i } = \sum _ { i = 0 } ^ { \infty } f ( \gamma _ { i } ) ~ p ^ { i } \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Proposition 10
Proposition 10.Let A and A’be two \(p\) -ringswithresidue rings \(k\) and \(k ^ { \prime }\) ,and suppose that A is strict.For every homomorphism \(\phi : k k ^ { \prime }\) ,there exists \(\pmb { \mathfrak { q } }\) unique homomorphism \(g : \mathsf { A } \to \mathsf { A } ^ { \prime }\) making commutative the diagram: \[ \begin{array} { l } { \textrm { A } ^ { \textrm { A } ^ { \prime } } \textrm { A } ^ { \prime } } \\ { \textrm { \downarrow } } \\ { \textrm { k } ^ { \textrm { \varphi } } \overset { \cdot } { } \textrm { k } ^ { \prime } . } \end{array} \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary: Corollary.Two strict \(p\) -rings having the same residue ring are canonically…
Corollary.Two strict \(p\) -rings having the same residue ring are canonically isomorphic.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Lemma 2
Lemma 2. Let \(\varphi : k \to k ^ { \prime }\) bea surjective homomorphism,the rings \(k\) and \(k ^ { \prime }\) beingperfect of characteristic \(p\) If there exists a strict \(p\) -ringAwithresidue ring \(k\) thenthere also existsa strict \(p\) ring \(\mathbf { A ^ { \prime } }\) with residue ring \(k ^ { \prime }\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Theorem 5
Theorem 5. For every perfect ring \(k\) of characteristic \({ \pmb p }\) there exists a unique strict \(p\) ring \(\mathbf { W } ( k )\) with residue ring \(k\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Convention / notation
Write \(S_{0},\dots,S_{n},\dots\), resp. \(P_{0},\dots,P_{n},\dots\), for the polynomials \(\varphi_{0},\dots,\varphi_{n},\dots\) associated by theorem 6 with the polynomial \[ \phi(X,Y) = X + Y, \qquad\text{resp.}\qquad \phi(X,Y) = X \cdot Y. \]
Formalized. Mathlib/RingTheory/WittVector/StructurePolynomial.lean::wittStructureInt, wittStructureInt_existsUnique; Mathlib/RingTheory/WittVector/Defs.lean::wittAdd, wittMul — The universal integral Witt structure polynomials and their uniqueness are exactly Serre’s S_n/P_n construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
Witt coordinates may be redefined by writing \(a=\sum_{i\ge0} f(\alpha_i)^{p^{-i}}p^i\); with these coordinates the Witt operations are given by ordinary polynomials.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Theorem 6
Theorem 6.For every \(\Phi \in \mathbb { Z } [ \mathbf { X } , \mathbf { Y } ]\) there exists \(\pmb { \alpha }\) unique sequence \(\{ \varphi _ { \emptyset } , \ldots ,\) \(\varphi _ { n } , \ldots , \ldots )\) of elements of \(\mathbf { Z } [ { \mathrm { X } } _ { 0 } , \ldots , { \mathrm { X } } _ { n } , \ldots ; { \mathrm { Y } } _ { 0 } , \ldots , { \mathrm { Y } } _ { n } , \ldots ]\) such that: \[ \mathbb { W } _ { n } ( \varphi _ { 0 } , \underline { { \mathrm { ~ , ~ . ~ . ~ , ~ } } } , \varphi _ { n } , \underline { { \mathrm { ~ , ~ . ~ . ~ . ~ } } } ) = \phi ( \mathbb { W } _ { n } ( \mathbf { X } _ { 0 } , \underline { { \mathrm { ~ . ~ . ~ . ~ } } } ) , \mathbb { W } _ { n } ( \mathbb { Y } _ { 0 } , \underline { { \mathrm { ~ . ~ . ~ . ~ } } } ) ) , \qquad n = 0 , 1 , \dots . . . \]
Formalized. Mathlib/RingTheory/WittVector/StructurePolynomial.lean::wittStructureInt, wittStructureInt_existsUnique; Mathlib/RingTheory/WittVector/Defs.lean::wittAdd, wittMul — The universal integral Witt structure polynomials and their uniqueness are exactly Serre’s S_n/P_n construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem 7
Theorem 7.The laws of composition defined abore make \(\mathbf { A } ^ { \aleph }\) into \(a\) commutativeunitary ring (called the ring of Witt vectorswith coefficients in A and denotedW(A)).
Formalized. Mathlib/RingTheory/WittVector/Basic.lean::instance : CommRing (𝕎 R) — The Witt addition and multiplication polynomials give the commutative unital ring structure.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example / comparison
ExAMPLEs.We have \[ \mathrm { S } _ { 0 } ( a , b ) = a _ { 0 } + b _ { 0 } , \qquad \mathrm { S } _ { 1 } ( a , b ) = a _ { 1 } + b _ { 1 } + \frac { a _ { 0 } ^ { p } + b _ { 0 } ^ { p } - ( a _ { 0 } + b _ { 0 } ) ^ { p } } { p } , \] \[ \mathrm { P } _ { 0 } \{ a , b \} = a _ { 0 } . b _ { 0 } , \qquad \mathrm { P } _ { 1 } \{ a , b \} = b _ { 0 } ^ { p } a _ { 1 } + b _ { 1 } a _ { 0 } ^ { p } + p a _ { 1 } b _ { 1 } . \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Theorem 8
Theorem 8. 1f \(k\) is \(\pmb { a }\) perfect ring of characteristic \(p , \ \mathbf { W } ( { \boldsymbol { k } } )\) is astrict \(p\) ring with residue ring \(k\)
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Definition / construction
Let \(\mathbf { H }\) be the strict \(p\) ringwith residue ring \(k\) and let \(f : k \mathbb { H }\) be the multiplicative system of representatives of \(\mathbf { H }\) Associate to a Witt vector \(\mathfrak { a } = \{ a _ { 0 } , \dotsc , a _ { n } , \dotsc ,\) the element \(\theta ( \mathfrak { a } ) \in \mathbb { H }\) defined by \[ \theta \{ { \mathfrak a } \} = \sum _ { i = 0 } ^ { \infty } f \{ a _ { i } \} ^ { p ^ { - i } } p ^ { i } . \] The formulas \[ \theta ( { \mathfrak { a } } + { \mathfrak { b } } ) = \theta ( { \mathfrak { a } } ) + \theta ( { \mathfrak { b } } ) , \qquad \theta ( { \mathfrak { a } } , { \mathfrak { b } } ) = \theta ( { \mathfrak { a } } ) , \theta ( { \mathfrak { b } } ) \]
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.
Corollary
Corollary \(\begin{array} { r } { . \mathrm { W } ( \mathbb { F } _ { p } ) = \mathbf { Z } _ { p } a n d \mathrm { W } _ { n } ( \mathbb { F } _ { p } ) = \mathbf { Z } / p ^ { n } \mathbf { Z } . } \end{array}\) 3
Formalized. Mathlib/RingTheory/WittVector/Compare.lean::TruncatedWittVector.zmodEquivTrunc, WittVector.equiv — These are the exact identifications W(F_p)=Z_p and W_n(F_p)=Z/p^nZ, up to the library’s truncation indexing convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
For a ring \(k\) of characteristic \(p\), the Frobenius endomorphism induces the Witt-vector Frobenius \(F:W(k)\to W(k)\), \(F((a_i))=(a_i^p)\).
Formalized. Mathlib/RingTheory/WittVector/Frobenius.lean::WittVector.frobenius, frobeniusEquiv — The Witt-vector Frobenius acts coefficientwise by p-th power over characteristic p.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Remark. In Grothendieck’s language of schemes, the preceding constructions define,for each \(\pmb { \pi } _ { }\) aring scheme \(\mathbf { W } _ { \mathfrak { s t } }\) affine and of finite type over Spec(Z).For any ringA,the ring \(\mathbf { W } _ { n } ( \mathbf { A } )\) is just the set of points of \(\mathbf { W } _ { \pi }\) with valuesin A.
Not formalized. The checked libraries contain completion, local-field, p-adic and Witt-vector infrastructure, but this full completion/Cohen–Witt statement is not exported at Serre’s stated generality.