FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 9 definitions, 3 theorems, 14 propositions, 3 lemmas, 10 corollaries and 3 conventions.
Of the 42 statements checked against Lean, 5 are formalized somewhere and 37 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 37 | 88% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 5 | 12% | Mathlib states and proves it. |
| checked in total | 42 |
- Canonical source block: FC10 Serre Chapter 3, “Discriminant and Different”,
FC10-C03-U001–FC10-C03-U042, 42 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 C03:
mathlib5,project-existing0,package-import0,reference-port0,unmatched37.
Definition / construction
Let V be a finite dimensional vector space over K. A lattice of V (with respect to A)is a sub-A-module \(\mathbf { x }\) of \(\mathbf { V }\) that is finitely generated and spans \(\mathbf { v }\) IfA is principal,this means that \(\mathbf { X }\) is a free A-module of rank \(\{ \mathbf { V } : \mathbb { K } \}\) ; one can oftenreduce to this case by localisation,i.e.,by replacing Awith \(A _ { p }\) and \(\mathbf { X }\) with \(\mathbf { A } _ { \mathfrak { p } } \mathbf { X } = \mathbf { X } _ { \mathfrak { p } }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Lemma 1
Lemma 1. If \(\mathbf { X _ { t } }\) and \({ \bf X } _ { 2 }\) are lattices of \(\mathbf { v }\) ，then the fractional ideal \(\chi ( X _ { 1 } / X _ { 3 } )\) \(\chi \{ \mathbf { X } _ { 2 } / \mathbf { X } _ { 3 } \} ^ { - 1 }\) ,defined forevery lattice \(\mathbf { X } _ { 3 } \subset \mathbf { X } _ { 1 } \cap \mathbf { X } _ { 2 }\) ,depends only on \(\mathbf { X } _ { 1 }\) and \(\mathbf { X } _ { 2 }\) ：
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
We may therefore associate to \(\mathbf { X } _ { 1 }\) and \({ \bf X } _ { 2 }\) the non-zero fractional ideal \[ \chi ( { \bf X } _ { 1 } , { \bf X } _ { 2 } ) = \chi ( { \bf X } _ { 1 } / { \bf X } _ { 3 } ) . \chi ( { \bf X } _ { 2 } / { \bf X } _ { 3 } ) ^ { - 1 } \quad \mathrm { f o r ~ } { \bf X } _ { 3 } \subset { \bf X } _ { 1 } \cap { \bf X } _ { 2 } . \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 1
Proposition 1.The following formulasarevalid: \[ \begin{array} { r l } & { \chi _ { \downarrow } ( X _ { \downarrow } , X _ { \bar { 2 } } ) \cdot \chi ( X _ { 2 } , X _ { 3 } ) \cdot \chi ( X _ { 3 } , X _ { \uparrow } ) = \mathbb { 1 } . } \\ & { \chi _ { \downarrow } ( X _ { \downarrow } , X _ { 2 } ) \cdot \chi ( X _ { 2 } , X _ { 1 } ) = \mathbb { 1 } . } \\ & { \chi _ { \downarrow } ( X _ { \downarrow } , X _ { 2 } ) = \chi _ { \downarrow } ( X _ { \downarrow } / X _ { 2 } ) \operatorname { i f } X _ { \downarrow } \supset X _ { 2 } . } \end{array} \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Convention / notation
(We-denote by 1 the unit element of the group of non-zero fractional idealsof A,i.e.,the ideal A.)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 2
Proposition 2. 1f \(\mathcal { U }\) is a K-automorphism of \(\mathbf { V }\) and \(\mathbf { \boldsymbol { x } }\) a lattice of \(\blacktriangledown\) then \(\chi ( \mathbf { X } , t \{ \mathbf { X } \} ) = \{ \operatorname* { d e t } ( t \{ t \} ) \}\) (principal ideal generated by \(\operatorname { d e t f } \{ u \} \}\) ，
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
Let \(n = [ \mathbf { V } : \mathbb { K } ] .\) and let \(W = \bigwedge ^ { n } \mathbf { V }\) ; it is a one dimensional vector space overK.To each lattice \(\mathbf { X }\) f \(\mathbf { V }\) let us associate \({ \bf X } _ { \mathbb { W } } = \bigwedge { \bf X }\) which may be identified with a lattice of \(\mathbf { W }\) ;as \(\boldsymbol { \mathrm { f } } \boldsymbol { \mathrm { W } } : \boldsymbol { \mathrm { K } } \boldsymbol { \mathrm { J } } = 1\) if \(\mathbf { \delta D }\) and \(\mathbf { \overrightarrow { D } } ^ { \prime }\) are two lattices of W,there is a unique non-zero fractional ideal a of \(\mathbf { K }\) such that \(\mathbf { D } ^ { \prime } \mathbf { a D }\) (namely, \(\chi ( \mathbf { D } , \mathbf { D ^ { \prime } } ) .\) Applyingthisto \(\mathbf { D } = \mathbf { X } _ { \mathbb { W } }\) \(\mathbf { D } ^ { \prime } = \mathbf { X } _ { \mathbb { W } } ^ { \prime }\) ,we obtain an ideal which is none other than \(\chi ( X , X ^ { \prime } )\) :this follows from localisation and applying proposition 2.
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
Let X bea lattice of \(\mathbf { V }\) ,and let \({ \mathbf { X } } _ { \mathbf { w } }\) be its nth exterior power,identified witha lattice ofW.The image of \({ \Chi } _ { \mathbb { W } } \otimes _ { \mathbf { A } } { \mathbf { X } } _ { \mathbb { W } }\) under \(\mathbf { T }\) isanon-zero fractional ideal of \(\kappa\) ,which is called the discriminant of \(\mathbf { X }\) with respect to \(\mathfrak { T }\) we denote itby \(\mathfrak { d } _ { \mathbf { X } , \boldsymbol { \mathsf { T } } }\) orsimply \({ \mathfrak { d } } _ { \mathbf { X } }\) when that does not lead to confusion.
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 3
Proposition 3.If X is a free A-module with basis \(\mathbf { S } = \mathbf { \varphi } _ { \parallel } ^ { \parallel } \mathbf { e } _ { 1 } , \dots , \mathbf { e } _ { n } \mathbf { \varphi } _ { \parallel } ^ { \dagger }\) ,then \(\mathbf { \hat { n } _ { X , \tilde { 1 } } }\) isthe principal ideal generated by the discriminant \(\scriptstyle \mathbf { D } _ { \widetilde { \mathbf { f } } } \mathbf { \left\{ S \right\} }\) (in the sense of Bourbaki,Alg.,Chap.IX, \(\ S 2 )\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 4
Proposition 4. Let \(\mathbf { X }\) be a lattice of \(\mathbf { V }\) and let \({ { \mathbf { } } } _ { { \mathbf { } } _ { \overline { { \mathbf { } } } } } ^ { * }\) be the set of all \(y \in V\) such that \(\mathbb { T } ( x , y ) \in \mathbf { A }\) forall \(x \in \mathbb { V }\) Then \({ \bf X } _ { \bar { \bf \Delta } } ^ { \ast }\) is a lattice of \(\mathbf { V }\) and \[ \mathfrak { d } _ { \mathbf { X } , \mathfrak { Y } } = \chi \{ \mathbf { X } _ { \mathfrak { I } } ^ { \ast } , \mathbf { X } \} . \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 5
Proposition 5.1f \(\mathbf { \boldsymbol { x } }\) amd \(X ^ { \prime }\) are lattices of \(\mathbf { V }\) then \[ \mathfrak { d } _ { \mathbf { X } ^ { \prime } , \mathbf { Y } } = \mathfrak { d } _ { \mathbf { X } , \mathbf { Y } } . \gamma \{ \mathbf { X } , \mathbf { X } ^ { \prime } \} ^ { 2 } . \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary: Corollary
Corollary. If \(X ^ { \prime } \subset X\) then \(\mathfrak { d } _ { \mathbf { X } ^ { \star } , \mathfrak { T } } = \mathfrak { d } _ { \mathbf { X } , \mathfrak { T } ^ { \widehat { \mathfrak { a } } ^ { 2 } } }\) ,where o is amideal of A: \(a = 1 j ^ { i }\) and only g \(\mathbf { X } ^ { \prime } = \mathbf { X }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
is surjective and that the bilinearform \(\mathfrak { F r f } ( x y )\) is non-degenerate on L.Thus the definitions and results of the preceding \(\ S\) are applicable to this form；in particular,the discriminant ofa lattice of \(\mathbf { L }\) (withrespect to A) is defined; if this lattice isa free A-module with basis \(\{ e _ { i } \}\) ,itsdiscriminant is the ideal generated by det \(\{ \mathrm { T r } \{ e _ { \mathrm { i } } e _ { j } \} \}\) ,and itisknown (Bourbaki,Alg.,Chap.V, \(\ S 1 0\) prop.12) that \[ \mathsf { d e t } \{ \mathsf { T r } ( e _ { i } e _ { j } ) \} = \{ \mathsf { d e t } ( \sigma ( e _ { i } ) ) \} ^ { 2 } , \] where \(\sigma\) runs through the set of \(\mathbf { K }\) -monomorphismsof \(\pmb { \mathrm { L } }\) into an algebraic closure of \(\kappa\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Convention / notation
Inparticular,this applies to the integral closure B of A in \(\mathbf { \check { L } }\) ,forprop.8of Chapter Ishows that B is a lattice of L.The corresponding discriminant will be denoted \(\mathfrak { d } _ { \mathfrak { A } / \mathrm { A } }\) ,orsometimes \(\mathfrak { d } _ { \mathbf { L } / \kappa }\) (when no confusion about A is possible).
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
The codifferent \(B^*\) of \(B/A\) is the set of \(y\in L\) such that \(\operatorname{Tr}(xy)\in A\) for all \(x\in B\).
Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::Submodule.traceDual, FractionalIdeal.dual, differentIdeal — These are the trace codifferent and its inverse different.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The different \(\mathfrak D_{B/A}\) is the inverse fractional ideal of the codifferent \(B^*\).
Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::Submodule.traceDual, FractionalIdeal.dual, differentIdeal — These are the trace codifferent and its inverse different.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 6
Proposition 6. \(\mathfrak { d } _ { \mathtt { B } / \mathtt { A } } = \chi _ { \mathtt { A } } ( \mathtt { B } ^ { * } / \mathtt { B } ) = \Nu _ { \mathtt { L } / \mathtt { K } } ( \mathfrak { D } _ { \mathtt { B } / \mathtt { A } } ) .\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary
Corollary.Thediscriminant \(\mathfrak { d } _ { \mathfrak { g } _ { i } \mathbf { A } }\) is contained in A.
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 7
Proposition7.Let a (resp.b) bea fractional ideal of K(resp.L) relative to A (resp.B).The following two properties are equivalent: (i \({ \mathrm { T r } } ( { \mathfrak { b } } ) \subset { \mathfrak { a } }\) ：m \(\mathfrak { b } \subset \mathfrak { a } . \mathfrak { D } _ { \mathfrak { B } / \mathrm { A } } ^ { - 1 }\) ，
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 8
Proposition 8. Let \(M / \mathbb { L }\) be a separable extension of finite degree n, C the integralclosureofAinM.Then \[ \mathfrak { D } _ { \mathrm { C / A } } = \mathfrak { D } _ { \mathrm { C / B } } , \mathfrak { D } _ { \mathrm { B / A } } \quad a n d \quad \mathfrak { d } _ { \mathrm { C / A } } = ( \mathfrak { d } _ { \mathrm { B / A } } ) ^ { n } , \mathrm { N } _ { \mathrm { L / K } } ( \mathfrak { d } _ { \mathrm { C / B } } ) . \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 9
Proposition 9.If Sisamultiplicative subset of A,then \[ \begin{array} { r } { { \mathbb S } ^ { - 1 } \mathfrak { D } _ { \mathtt { B } / \mathtt { A } } = \mathfrak { D } _ { \mathbb { S } ^ { - 1 } \mathtt { B } / \mathbb { S } ^ { - 1 } \mathtt { A } } \quad a n d \quad { \mathbb S } ^ { - 1 } \mathfrak { d } _ { \mathtt { B } / \mathtt { A } } = \mathfrak { d } _ { \mathbb { S } ^ { - 1 } \mathtt { B } / \mathbb { S } ^ { - 1 } \mathtt { A } } . } \end{array} \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 10
Proposition 10.Let \(\mathfrak { P }\) beaprime ideal ofB,and let \({ \mathfrak { p } } = { \mathfrak { P } } \cap\) A.Let \(\widehat { \mathfrak { T } } _ { \mathfrak { P } }\) be the ideal generated by the different \(\mathfrak { D } _ { \mathfrak { g } / \mathfrak { A } }\) in the completion \(\widehat { \sf B } _ { \mathfrak { P } }\) ;then \(j _ { \emptyset }\) is the different of the ring \(\hat { \mathbf { B } } _ { \mathfrak { P } }\) with respect to the ring \(\hat { \mathbf { A } } _ { \mathfrak { p } }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary: Corollary
Corollary. Let \(\mathfrak { H }\) be the idealof \(\hat { \mathsf { A } } _ { \mathfrak { p } }\) generated by the discriminant \(\bf \widehat { g } _ { B / A }\) ,and let \({ \mathfrak { d } } _ { \mathfrak { P } }\) be thediscriminant of \(\hat { \textmd B } _ { \mathfrak { P } }\) with respect to \(\hat { \mathbf { A } } _ { p }\) Then \[ { \hat { \mathfrak { d } } } = \prod _ { \mathfrak { g } _ { \vert \mathfrak { p } } } { \mathfrak { d } } _ { \mathfrak { g } } . \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Theorem 1
Theorem 1. Let \(\mathfrak { P }\) beaprime ideal of \(\mathbf { \delta B }\) andlet \({ \mathfrak { p } } = { \mathfrak { P } } \cap { \mathfrak { A } }\) In order that the extension \(L / \mathbf { K }\) be unramified at \(\mathfrak { P }\) (cf. Chap. \(1 , \ S 4 \}\) it is necessary and sufficient that \(\mathfrak { P }\) does not divide the different \({ \mathfrak { D } } _ { { \mathfrak { s } } / A }\) ，
Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::not_dvd_differentIdeal_iff; Mathlib/RingTheory/Unramified/Locus.lean::Algebra.IsUnramifiedAt — A prime is unramified exactly when it does not divide the different.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary 1
Corollary 1.Let p be a prime ideal of A.Inorder that \(\mathbf { L } / \mathbf { K }\) be unramified at \(\mathfrak { p }\) it is necessary and sufficient that \(\mathfrak { p }\) does not divide the discriminant \(\mathfrak { d } _ { \mathfrak { B } / \mathrm { A } }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary 2
Corollary2. Almost all the prime ideals of \(\mathbf { \delta B } ( o r\) ofA)are unramified in the extension \(L / K\)
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::Ideal.finite_factors; Mathlib/RingTheory/DedekindDomain/Different.lean::not_dvd_differentIdeal_iff — Only finitely many primes divide the nonzero different, so all but finitely many primes are unramified.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
We now examine more closely the structure of unramified extensions, limiting ourselves to the casewhere Aisacomplete discrete taluation ring; we denote its residue field by \(k\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Theorem 2
Theorem 2. Let \(k ^ { \prime } / k\) bea finite separable extension. Then there exists a finite unramified extension \(K / \mathbb { X }\) whose corresponding residue extension is isomorphic to \(k ^ { \prime } / k\) ；thisextension is unique、up to unique isomorphism.Itis Galois \(i f\) and only if \(k ^ { \prime } / k\) is.
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Theorem 3
Theorem 3.Let \(\mathbf { \vec { K } } / \mathbf { \vec { K } }\) bea finite unramified extension,with residue extension \(k ^ { \prime } / k\) and let \(\mathbb { K } ^ { \prime \prime } / \mathbb { K }\) be anarbitrary finite extension,with residue extension \(k ^ { \prime \prime } / k\) The set of \(\mathbf { K }\) -isomorphismsof \(\aleph ^ { \prime }\) into \(\mathbf { K } ^ { \prime \prime }\) is then in one-to-one correspondence (byreduction) with the setof \(k\) isomorphismsof \(\bigstar ^ { \prime }\) into \(k ^ { \prime \prime }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary 1
Corollary 1. Let \(k _ { s }\) be the separable closure of \(k\) (i.e.,the largest separable extension of \(k\) withina given algebraic closureof \(k\) andlet \(\mathbb { K } _ { n \pi }\) be the inductive (direct） limit of theunramified extensions of \(\mathbf { K }\) that correspond to the finite subextensions of \(k _ { s }\) Thefield \(\mathbf { K } _ { n s }\) is Galois overK with residue feld \(k _ { s }\) ,and \(\mathrm { G } ( K _ { n r } / \mathrm { K } ) = \mathrm { G } ( k _ { s } / k ) .\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
The extension \(K _ { \mathfrak { s r } }\) iscalled the maximal unramified extension of \(\mathbf { K }\) Itis unique,up to isomorphism.For example,if \(\pmb { k }\) isa finite field, \(\mathrm { G } ( k _ { s } / k )\) is isomorphic to the completion \(\pmb { \hat { z } }\) of \(\mathbf { z }\) for the topology of subgroups of finite index,and the same holds for \({ \mathrm { G } } ( \mathbb { K } _ { n r } / \mathbb { K } )\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary 2
Corollary 2.Let \(\mathbf { K } ^ { \prime \prime } / \mathbf { K }\) beafinite extension,with residue extension \(k ^ { \prime \prime } / k\) The subextensions \(K / \kappa\) of \({ \bf K } ^ { \prime \prime } / { \bf K }\) which are unramified over \(\kappa\) are in one-to-one correspondence with the separable subextensions \(k ^ { \prime } / k\) of \(k ^ { \prime \prime } / k\) *
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary 3
Corollary 3.With the hypothesesof cor.2,there exists amaximal unramified subextension \(\kappa / \kappa\) of \(\mathbf { K } ^ { \prime \prime } / \mathbf { K }\) Itsresidue extension \(k ^ { \prime } / k\) is thelargest separable subextension of \(k ^ { \prime \prime } / k\) We have \(e ( \mathbb { K } ^ { \prime \prime } / \mathbb { K } ) = e ( \mathbb { K } ^ { \prime \prime } / \mathbb { K } ^ { \prime } )\) \(f ( \mathbf { K } ^ { \prime \prime } / \mathbf { K } ^ { \prime } ) = \big [ \mathbf { \mathcal { k } } ^ { \prime \prime } : \mathbf { \mathcal { k } } \big ] _ { i }\) ,and \(f ( \mathbf { \mathbf { \mathbf { K } } ^ { \prime } } / \mathbf { \mathbf { \mathbf { K } } } ) = \big [ \pmb { k } ^ { \prime \prime } : \pmb { k } \big ] _ { s }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 11
Proposition 11. Let \(n=[L:K]\) and let \(C\subset B\) be a subring containing \(A\) with \(A\)-basis \(1,x,\ldots,x^{n-1}\). If \(f\) is the characteristic polynomial of \(x\), then (i) \(f\in A[X]\); (ii) \(C^*\) is free over \(A\) with basis \(x^i/f^{\prime}(x)\), \(0\le i\le n-1\).
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 12
Proposition 12. Suppose that B (hence also A) is a discrete valuation ring; ifLand \(\bar { \kappa }\) denote the residue fields of these two rings,suppose also that the extension \(I / R\) is separable.ThenB has a basis over A composed of the powers \(1 , x , \ldots , x ^ { n - 1 }\) ofa singie element \(\pmb { x }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Lemma 3
Lemma 3.The products \(\mathbf { x } ^ { i } \Re ^ { j }\) \(0 \leq i < j , 0 \leq j < e ,\) forma basis for the Amodule B.
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Lemma 4
Lemma4.Theelement \(x\) may be chosen so that there exists a monic polynomial R(X),of degree \(f _ { i }\) with coefficients inA,such that \(\mathbb { R } ( x )\) is a uniformizer of B.
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary 1
Corollary 1.With the preceding notation and hypotheses, \[ \mathfrak { r } = f ^ { \prime } \{ \mathfrak { x } \} , \mathfrak { D } _ { \mathtt { B } / \mathrm { A } } ^ { - \mathrm { ~ f ~ } } . \]
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Corollary 2
Corollary2.Thedifferen \({ \mathfrak { D } } _ { { \mathfrak { B } } / { \mathbf { A } } }\) dividestheprincipal ideal \(( f ^ { \prime } ( x ) )\) For these two ideals to be equal,it is necessary and sufficient that \(\mathbf { \vec { \mathbf { \mathbf { B } } } } \mathbf { \vec { \mathbf { \mathbf { C } } } }\) (i.e.,that \(\mathbf { B } = \mathbf { A } \{ x \} .\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Proposition 13
Proposition 13.Let \(\mathfrak { P }\) bea non-zero prime ideal of B,and let \(p = \mathfrak { P } n\) A.Let \(E _ { \mathfrak { P } }\) and \({ \bar { \mathsf { K } } } _ { \mathfrak { p } }\) be the corresponding residue fields.Suppose that the residue extension is separable.Then the exponent of \(\mathfrak { P }\) in the different \(\mathfrak { D } _ { \mathbb { R } ^ { / } \mathrm { A } }\) is greater than or equal to \(e _ { \mathfrak { P } } - \mathfrak { k } \mathrm { ~ f ~ } \ell _ { \mathfrak { P } }\) denoting the ramification index),with equality taking place if and only if \(e _ { \mathfrak { g } }\) is prime to the characteristic of the residue feld \(R _ { p }\)
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.
Definition / construction
Let B be any commutative A-algebra.The map \(\{ x , y \} \mapsto . \mathrm { v } y ^ { \intercal }\) defines a homomorphism \[ \begin{array} { r } { \theta : \mathbf { B } \otimes _ { \mathbf { A } } \mathbf { B } \mathbf { B } . } \end{array} \] Let Ibe its kernel,and put \(\Omega _ { \mathsf { A } } ( \mathsf { B } ) = \mathbb { I } / \mathbb { I } ^ { 2 } = \mathbb { I } \otimes _ { \mathsf { B S B } } \mathbb { B } ;\) this gives a B-module called the module of A-differentials of the ring B (thisdefinition is due to E.Kahler).If \(\pmb { d x }\) denotes the image of \(x \otimes \operatorname { I } - \operatorname { I } \otimes x\) in \(\ P / \ P ^ { 2 }\) ,every element of \(\Omega _ { A } ( \mathbb { B } )\) can be written in the form \(\sum { y _ { i } d { x _ { i } } }\) ,and we have \[ \begin{array} { r } { d \{ x y \} = x d y + y d x } \\ { d a = 0 \quad \mathrm { i f ~ } a \in \pmb { A } . } \end{array} \] The module \(\Omega _ { \Lambda } ( { \bf B } )\) is actually universal for the above properties (cf.[12], expose 13.as well as[46]).
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential, KaehlerDifferential.ideal, KaehlerDifferential.D — Mathlib defines Ω_{B/A} from the kernel of multiplication modulo its square and supplies the universal derivation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 14
Proposition14.LetA bea Dedekind domain,with fieldof fractions \(\kappa ;\) letL bea finite separable extension of \(\mathbf { K }\) ,and let \(\pmb { \mathrm { B } }\) be the integral closure ofAin L.Suppose that for every prime ideal \(\mathfrak { P }\) ofB,the corresponding residue extensionis separable.The B-module \(\Omega _ { \mathrm { A } } ( \ B { \mathbf { \{ B \} } } )\) can then be generated by one element,and itsannihilator is thedifferent DB/A
Not formalized. The checked libraries contain different, trace-dual, unramified and Kähler-differential infrastructure, but this full discriminant/different statement is not source-complete in the inspected APIs.