FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 30 definitions, 23 propositions, 4 lemmas, 9 corollaries, 7 examples, 8 conventions and 2 other statements.
Of the 83 statements checked against Lean, 36 are formalized somewhere and 47 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 47 | 57% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 36 | 43% | Mathlib states and proves it. |
| checked in total | 83 |
- Canonical source block: FC10 Serre Chapter 1, “Discrete Valuation Rings and Dedekind Domains”,
FC10-C01-U001–FC10-C01-U083, 83 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 C01:
mathlib36,project-existing0,package-import0,reference-port0,unmatched47.
Definition / construction
AringA iscalled a discretevaluationring if it isaprincipal ideal domain (Bourbaki,Alg., Chap.VII) that has a unique non-zero prime ideal m(A). [Recall that an ideal \(\mathfrak { p }\) ofa commutative ring A iscalled prime if thequotient ring \(A / p\) is an integral domain.]
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::IsDiscreteValuationRing.TFAE — Mathlib’s DVR equivalence includes the PID-with-a-unique-nonzero-prime characterization used by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The field \(A/m(A)\) is the residue field of a discrete valuation ring \(A\).
Formalized. Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean::IsLocalRing.ResidueField, IsLocalRing.residue — This is exactly the residue field of a local/DVR ring and its quotient map.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The invertible elements of a discrete valuation ring are its units.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
Ina principal ideal domain, the non-zero prime ideals are the ideals of the formπA,where \(\pmb { \pi }\) is an irreducible element.The definition above comes down to saying that A has one and only one irreducible element,up to multiplication by an invertible element;such an element is called a uniformizing element ofA(or uniformizer;Weil [123] calls it a“prime element”).
Formalized. Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::irreducible_iff_uniformizer, exists_units_eq_smul_zpow_of_irreducible; Mathlib/RingTheory/Valuation/Discrete/Basic.lean::IsUniformizer.of_associated, associated_of_isUniformizer — Uniformizers are precisely irreducibles in a DVR and any two differ by a unit.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Thenon-zero ideals ofA are of the form \(\mathfrak { m } \{ \mathbf { A } \} = \mathfrak { r } ^ { n } \mathbf { A }\) where \(\pmb { \pi }\) is auniformizing element.If \(x \neq 0\) is any element ofA,one can write \(x = \pi ^ { n } \mathfrak { u }\) with \(\pmb { n } \in \mathbb { N }\) and \(\pmb { u }\) invertible；the integer \(\pmb { n }\) iscalled thevaluation (or the order) of \(\pmb { x }\) and is denoted \(v _ { \{ x \} } ^ { \{ }\) ; it does not depend on the choice of \(\pmb { \pi }\)
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::exists_maximalIdeal_pow_eq_of_principal; Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::exists_units_eq_smul_zpow_of_irreducible — The maximal-ideal powers classify nonzero ideals and every nonzero fraction is a unit times an integral power of a uniformizer.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
(We make the convention that \(v ( 0 ) = + \infty ,\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 1
Proposition1.LetK bea field,and let \(v \colon \mathbb { K } ^ { * } \to \mathbb { Z }\) beahomomorphism having properties a) and \(\mathbf { \hat { \rho } } _ { \mathbf { \hat { \rho } } }\) above.Then theset A of \(\mathbf { x } \in \mathbf { K }\) such that \(v ( x ) \geq \emptyset\) is \(\pmb { \alpha }\) discretevaluation ring havinguas its associated valuation.
Formalized. Mathlib/RingTheory/Valuation/Discrete/Basic.lean::valuationSubring_isDiscreteValuationRing — A rank-one discrete valuation has a valuation subring which is a DVR, exactly Serre’s construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example / comparison
1Let \(p\) beaprime number,and let \(\mathbf { Z } _ { \{ p \} }\) be the subset of the field \(\mathbf { Q }\) of rationals consisting of the fractions \(r / s ,\) where \(\pmb { s }\) is not divisible by \(p\) ; this is a discrete valuation ring with residue field the field \(\vec { \mathbf { F } } _ { \mathfrak { p } }\) of \(p\) elements.If \({ i } ! _ { \mathfrak { P } }\) denotes the associated valuation, \(v _ { p } \{ x \}\) is none other than the exponent of \(p\) in the decomposition of \(x\) into prime factors. An analogous procedure applies to any principal ideal domain (and even to any Dedekind domain,cf.$3).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Example / comparison
2)Let \(k\) be a field,and let \(k \{ \{ \Upsilon \} \}\) be the field of formal power series in one variable over \(k\) For every non-zero formal series \[ f ( \mathbf { T } ) = \sum _ { n \geq n _ { 0 } } \mathfrak { a } _ { n } \mathbf { T } ^ { n } , \qquad \mathfrak { a } _ { n _ { 0 } } \neq 0 , \] one defines the order \(v ( f )\) of \(f\) to be the integer \(n _ { 0 }\) (cf.Bourbaki,Alg.,Chap. IV). One obtains thereby a discrete valuation of \(k ( ( \tilde { \Pi } ) )\) ,whose valuation ring is \(k [ [ \mathbf { T } ] ]\) ,theset of formal series with non-negative exponents；its residue feld is \(k\) ，
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Example / comparison
3)Let \(\mathbf { V }\) beanormal algebraic variety,of dimension \(\pmb { \eta }\) ,and let W be an irreducible subvariety of \(\mathbf { V }\) ,of dimension \(n - 1 .\) Let \(\mathbf { A } _ { \mathbf { V } / \mathbf { W } }\) be the local ring of \(\mathbf { V }\) along \(\mathbf { W }\) (i.e.,the set of rational functions \(f\) on \(\mathbf { V }\) which are defined at leastat one point of W).The normality hypothesis shows that \(\mathbf { A } _ { \mathbf { V } / \mathbf { W } }\) is integrallyclosed;the dimension hypothesis shows that it is a one-dimensional local ring;therefore it isa discrete valuation ring (cf. \(\ S 2\) prop.3)； its residue fieldis the field of rational functions on \(\mathbf { w }\) f \({ \mathfrak { v } } _ { \mathbf { W } }\) denotes the associated valuation,and if \(f\) is a rational function on \(\mathbf { V }\) the integer \(v _ { W } \{ f \}\) is called the “order”of \(f\) along \(\mathbf { w }\) ;it is the multiplicity of W in the divisor of zeros and poles of \(f\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Example / comparison
4Let \(\pmb { \mathbb { S } }\) be a Riemann surface (i.e.,a one-dimensional complex manifold), and let \(\mathbf { P } \in \mathbb { S }\) The ring \(S _ { P }\) of functions holomorphic in a neighborhood (unspecified) of \(\mathbf { P }\) is a discrete valuation ring,isomorphic to the subring of convergent power series in \(\mathbf { C } [ \lbrace \mathbf { T } \rbrace ]\) ;itsresidue field is C.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 2
Proposition2.Let A bea commutativering.In orderthat A bea discrete valuationring,it isnecessaryand sufficient that it bea Noetherian local ring,and that itsmaximal ideal be generated byanon-nilpotent element.
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain — The TFAE theorem gives the Noetherian-local/principal-maximal-ideal characterization under the source domain hypotheses.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 3
Proposition3.Let A bea Noetherian integral domain.In order that A bea discrete valuation ring,it is necessary and sufficient that it satisfy the two following conditions: (i）Aisintegrally closed. (ii)A hasa unique non-zero prime ideal.
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::IsDiscreteValuationRing.TFAE — The same TFAE package includes the integrally-closed/unique-nonzero-prime characterization.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
For a non-zero ideal \(\mathfrak a\) of an integral domain \(A\) with fraction field \(K\), set \(\mathfrak a^{\prime}=\{x\in K:x\mathfrak a\subset A\}\). If \(A\) is Noetherian this is a fractional ideal; \(\mathfrak a\) is invertible when \(\mathfrak a\mathfrak a^{\prime}=A\).
Formalized. Mathlib/RingTheory/FractionalIdeal/Basic.lean::FractionalIdeal; Mathlib/RingTheory/FractionalIdeal/Inverse.lean::mul_inv_cancel_iff_isUnit — Fractional ideals and invertibility by a multiplicative inverse are represented exactly.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
A subset \(S\) of an integral domain is called multiplicative if it contains \(1\), is closed under multiplication, and does not contain \(0\).
Formalized. Mathlib/Algebra/Group/Submonoid/Defs.lean::Submonoid; Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean::le_nonZeroDivisors_of_noZeroDivisors, zero_notMem_nonZeroDivisors — A multiplicative subset with 1 and closed multiplication is Mathlib’s submonoid together with 0 ∉ S; over a domain this is equivalently a submonoid of the nonzero divisors, exactly the source convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
An element \(x\) of a ring containing \(A\) is integral over \(A\) if it satisfies a monic equation \(x^n+a_1x^{n-1}+\cdots+a_n=0\) with \(a_i\in A\).
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean::IsIntegral — IsIntegral is the monic-polynomial definition in the source.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
One says that Ais integrallyclosed inaring \(\mathbf { B }\) containing it if every element ofB integral over A belongs to A.One says that A is integrally closed if it is an integral domain integrally closed in its field of fractions.Cf.Bourbaki, Alg.comm.,Chap.V,81.]
Formalized. Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean::IsIntegrallyClosedIn, IsIntegrallyClosed — These are exactly Serre’s two integrally-closed notions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 1
Lemma 1.Let A be a discrete valuationring,and let \(x _ { i }\) be elements of the fieldof fractions of A such that \(v \{ x _ { \mathrm { i } } \} > v \{ x _ { \mathrm { i } } \}\) for \({ \mathfrak { i } } \geq 2\) One then has \[ x _ { 1 } + x _ { 2 } + \cdots + x _ { n } \neq 0 . \]
Formalized. Mathlib/RingTheory/Valuation/IsTrivialOn.lean::Valuation.map_sum_eq_of_lt — The strict-minimum valuation rule gives the source non-cancellation assertion for a unique term of minimal valuation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
For a multiplicatively closed subset \(S\) of an integral domain \(A\), the fractions \(x/s\) with \(x\in A\) and \(s\in S\) form the localization \(S^{-1}A\); its prime ideals correspond by contraction to the prime ideals of \(A\) disjoint from \(S\).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
Thisapplies notably when ${ { } } = { { } } - { } $ where \({ \mathfrak { p } }\) isaprime ideal of A.The ring \(S ^ { - 1 } A\) is then denoted \(\mathsf { A } _ { \mathfrak { p } }\) ；it isa local ring with maximal ideal \(p A _ { p }\) and residue field the field of fractions of \(\mathsf { A } / \mathsf { p }\) ;theprime ideals of \(A _ { y }\) correspond to those prime ideals of A that are contained in p. One says that \(\mathbf { A } _ { \mathfrak { p } }\) isthe localisationofAat \(\mathfrak { p }\) cf.Bourbaki,Alg.comm.,Chap.I, \(\ S 2\)
Formalized. Mathlib/RingTheory/Localization/AtPrime/Basic.lean::Localization.AtPrime, IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.orderIsoOfPrime, IsLocalization.AtPrime.equivQuotMaximalIdeal — Localization at a prime is local, with the stated prime correspondence and residue field description.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 4
Proposition 4.If Ais a Noetherian integral domain,the following two properties are equivalent: (i） For erery prime ideal \({ \mathfrak { P } } \neq 0\) fA, \(\mathbf { A } _ { \mathfrak { p } }\) is a discrete raluation ring. (iiAis integrally closedandof dimension \(\leq 1\)
Formalized. Mathlib/RingTheory/DedekindDomain/Dvr.lean::IsDedekindDomainDvr, IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain; Mathlib/RingTheory/DedekindDomain/Basic.lean::isDedekindDomain_iff — Mathlib packages both equivalent Dedekind characterizations: integrally closed dimension ≤1 and DVR localizations.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
An integral domain has dimension at most \(1\) when every non-zero prime ideal is maximal.
Formalized. Mathlib/RingTheory/DedekindDomain/Basic.lean::Ring.DimensionLEOne, IsDedekindDomain — The dimension-one and Dedekind-domain source definitions are the native Mathlib notions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: Definition.A Noetherian integral domain which has the two equivalent…
Definition.A Noetherian integral domain which has the two equivalent propertiesofprop.4iscalledaDedekinddomain.
Formalized. Mathlib/RingTheory/DedekindDomain/Basic.lean::Ring.DimensionLEOne, IsDedekindDomain — The dimension-one and Dedekind-domain source definitions are the native Mathlib notions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example / comparison
ExAMPLEs.Every principal ideal domain is Dedekind.The ring of integers ofanalgebraic number field is Dedekind (apply prop.9 below to thering Z).
Formalized. Mathlib/RingTheory/DedekindDomain/Basic.lean::IsPrincipalIdealRing.isDedekindDomain; Mathlib/NumberTheory/NumberField/Basic.lean::instance : IsDedekindDomain (𝓞 K) — Both source examples—PIDs and rings of integers of number fields—are native instances.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 5
Proposition 5.In a Dedekind domain,everynon-zero fractional ideal is invertible.
Formalized. Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::isDedekindDomainInv_iff, IsDedekindDomainInv.commGroupWithZero, FractionalIdeal.semifield — Every nonzero fractional ideal is invertible in a Dedekind domain, and the nonzero fractional ideals form the resulting multiplicative group.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
1f \(\mathbf { K }\) isthe field of fractionsofA,a fractional idealaofA isasub-AmoduleofK finitely generated overA.Onesays \(\pmb { \mathfrak { a } }\) isinvertible ifthere exists \({ \mathfrak { q } } ^ { \prime } \subset { \mathbb { K } }\) with a. \({ \mathfrak { a } } ^ { \prime } = \mathsf { A }\) ]
Formalized. Mathlib/RingTheory/FractionalIdeal/Basic.lean::FractionalIdeal; Mathlib/RingTheory/FractionalIdeal/Inverse.lean::mul_inv_cancel_iff_isUnit — This is the exact fractional-ideal and invertibility definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
\(\{ \mathfrak { a } : \mathfrak { b } \}\) denotes the ideal of those \(\displaystyle x \in \mathbb { K }\) such that \(x ^ { \mathfrak { f } } \in \mathfrak { a }\) If \({ \mathfrak { A } } ^ { \prime } = \{ \mathsf { A } : { \mathfrak { a } } \} ,\) to say that \(\pmb { \mathfrak { a } }\) is invertible amounts to saying that a. \({ \mathfrak { a } } ^ { \prime } = \mathbf { A } .\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary: Corollary.The non-zero fractional ideals of a Dedekind domain forma group…
Corollary.The non-zero fractional ideals of a Dedekind domain forma group undermultiplication.
Formalized. Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::isDedekindDomainInv_iff, IsDedekindDomainInv.commGroupWithZero, FractionalIdeal.semifield — Every nonzero fractional ideal is invertible in a Dedekind domain, and the nonzero fractional ideals form the resulting multiplicative group.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
This group is called the ideal group of the ring.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 6
Proposition 6. 1f \(x \in \mathsf { A }\) \(x \neq 0\) ,then only finitely many prime ideals contain x.
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::Ideal.finite_factors — Applied to the principal ideal generated by x, finite prime support is exactly Serre’s proposition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary: Corollary
Corollary. \(1 f\) one denotes by \({ \mathfrak { v } } _ { \mathfrak { p } }\) thevaluation ofK defined by \(\mathbf { A } _ { \mathfrak { p } }\) ,then for eter \(x \in \mathbb { K } ^ { * }\) the numbers \({ \mathfrak { r } } _ { { \mathfrak { p } } } ( x )\) arealmost all zero (i.e., zero except for a finitenumber).
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::FractionalIdeal.finite_factors, FractionalIdeal.finprod_heightOneSpectrum_factorization, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal — The prime exponents of a principal/fractional ideal have finite support and give the unique factorization asserted by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 7
Proposition 7.Euery fractional ideal a ofA canbewritten uniquely inthe form: \[ { \mathfrak { a } } = \prod { \mathfrak { p } } ^ { v _ { \mathrm { e } } ( a ) } , \] where the \(v _ { p } ( 0 )\) are integers almost all zero.
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::FractionalIdeal.finite_factors, FractionalIdeal.finprod_heightOneSpectrum_factorization, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal — The prime exponents of a principal/fractional ideal have finite support and give the unique factorization asserted by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Approximation Lemma
Approximation Lemma.Let \(k\) bea positive integer.For every i, \(1 \leq i \leq k ,\) let \({ \mathfrak { p } } _ { \mathrm { i } }\) bedistinct prime ideals ofA, \(x _ { i }\) elements of \(\pmb { \kappa }\) ，and \(\hbar _ { j }\) integers.Then there exists an \(x \in \mathbb { K }\) such that \(v _ { p _ { i } } \{ x - x _ { i } \} \geq n _ { i }\) forall \(\dot { \pmb { \xi } } ,\) and \(v _ { q } ( x ) \geq 0\) for \(q \neq\) \({ \mathfrak { p } } _ { : } , \dots , { \mathfrak { p } } _ { k }\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary: Corollary.A Dedekinddomain with only finitely many prime ideals is principal.
Corollary.A Dedekinddomain with only finitely many prime ideals is principal.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Convention / notation
Throughout this paragraph,K isa feld and La finite extension of K；its degree \([ 1 , \mathbb { K } ]\) will be denoted by n.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 8
Proposition8.Hypothesis(F）is satisfied when \(L / \mathbb { K }\) is aseparable extension.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
Remarks.1） The same proof shows that \(\mathbf { B } ^ { * }\) is a finitely generated Bmodule,i.e.,a fractional ideal of B. Its inverse is called the different of B overA,cf.Chap. III, \(\ S 3\)
Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::Submodule.traceDual, FractionalIdeal.dual, differentIdeal — The trace-dual codifferent is a fractional ideal and its inverse is Mathlib’s different ideal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 9
Proposition9.IfAisDedekind thenBisDedekind.
Formalized. Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean::IsIntegralClosure.isDedekindDomain, integralClosure.isDedekindDomain — The integral closure of a Dedekind domain in the finite separable setting is Dedekind.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 2
Lemma 2. Let \({ \bf A } \subset \bf \delta B\) berings,with \(\mathbf { B }\) integral over A.1f \(\mathfrak { P } \subset \mathfrak { Q }\) are prime idealsof \(\mathfrak { B }\) such that \(\Re \cap \mathbf { A } = \cap \mathbf { A }\) then \(\mathfrak { P } = \mathfrak { Q }\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
Let us keep the hypotheses of prop. 9.If \(\mathfrak { P }\) is a non-zero prime ideal of B,and if \({ \mathfrak { p } } = { \mathfrak { P } } \cap { \mathfrak { A } }\) wewill say that \(\mathfrak { F }\) divides \(\mathfrak { P }\) (or that \(\mathfrak { F }\) is“above”p）, and we will write \({ \mathfrak { P } } _ { \sharp } ^ { \sharp } { \mathfrak { p } }\) Thisrelation is also equivalent to saying that \(\mathfrak { P }\) contains the ideal \(\mathfrak { p B }\) generated by \(\mathfrak { p }\) Denote by \({ \mathcal { C } } _ { \mathfrak { P } }\) the exponent of \(\mathfrak { P }\) in the decomposition of \(\mathfrak { p B }\) into prime ideals.Thus：
Formalized. Mathlib/RingTheory/Ideal/Over.lean::Ideal.LiesOver; Mathlib/RingTheory/RamificationInertia/Ramification.lean::Ideal.ramificationIdx — LiesOver is the prime-above relation and ramificationIdx is the exponent in the factorization of the extended prime.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The integer \(e _ { \mathfrak { P } }\) is called theramification index of \(\mathfrak { F }\) in the extension \(L / \mathbb { K }\)
Formalized. Mathlib/RingTheory/RamificationInertia/Ramification.lean::Ideal.ramificationIdx — This is the source ramification-index definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
On the other hand,if \(\mathfrak { P }\) divides \({ \mathfrak { P } }\) the field \(\mathbb { B } / \mathfrak { P }\) is an extension of the field \(A / \phi\) As \(\pmb { \mathrm { B } }\) is finitely generated over A, \(\mathbf { B } / \mathfrak { P }\) is an extension of \(A / \pi\) of finite degree.The degree of this extension is called the residue degree of \(\mathfrak { P }\) in the extension \(\mathbb { E } / \mathbb { K }\) ,and is denoted \(f _ { \mathfrak { P } }\) Thus: \[ f _ { \mathfrak { P } } = \{ \mathbf { B } / \mathfrak { P } : \mathbf { A } / \mathfrak { p } \} . \]
Formalized. Mathlib/RingTheory/RamificationInertia/Inertia.lean::Ideal.inertiaDeg — This is the residue-field degree definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
[When we want to specify \(\mathbf { K }\) ,we write \(\mathcal { C } _ { \mathfrak { P } / \mathfrak { P } }\) and \(f _ { \mathfrak { P } _ { i / \sharp } }\) ,instead of \(e _ { \mathfrak { P } }\) and \(f _ { \phi } . \}\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
When there is only one prime ideal \(\mathfrak { P }\) which divides’p and \(f _ { \ P } = 1\) 、one says that \(1 _ { \mathcal { A } } / \mathbb { K }\) is totally ramified at \(\mathfrak { P }\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
When \(e _ { \mathfrak { P } } \simeq \mathfrak { k }\) and \(\mathbf { B } / \mathfrak { P }\) is separable over \(\mathbb { A } / \mathbb { p }\) one says that \(L / R ^ { \frac { 3 } { 2 } }\) isun ramified at \(\mathfrak { P }\) If \(\mathrm { L } / \mathbb { K }\) is unramified forall the prime ideals \(\mathfrak { P }\) dividing \({ \mathfrak { P } }\) ,one says that \(L / \mathsf { K }\) is unramified above \({ \mathfrak { p } }\) (or“at p”); cf. Chap.III,$5.
Formalized. Mathlib/RingTheory/Unramified/Locus.lean::Algebra.IsUnramifiedAt; Mathlib/NumberTheory/RamificationInertia/Unramified.lean::Ideal.isUnramifiedAt_iff — The local unramified condition is equivalent to ramification index one plus separable residue extension.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 10
Proposition 10.Let \({ \mathfrak P }\) beanon-zero prime ideal of A,the ring \(\mathbf { B } / \mathbf { p } \mathbf { \ B }\) is an \(A / \ p\) algebra of degree \({ \mathfrak { n } } = [ { \mathrm { L } } \colon \mathbb { K } ]\) isomorphic to the product \(\prod _ { \mathbf { i } } \mathbf { \Pi } _ { \mathbf { n } \mathbf { i } ; \mathbf { p } } \mathbf { B } / \ P ^ { \mathbf { i } , \mathbf { r } \cdot \mathbf { q } }\) ： \(V _ { \phi }\) havetheformula: \[ \mu = \sum _ { \mathfrak { P } \mid \mathfrak { p } } e _ { \mathfrak { P } } f _ { \mathfrak { P } } . \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary: Corollary.The number of prime ideals \(\mathfrak { P }\) f \(\mathbf { B }\)…
Corollary.The number of prime ideals \(\mathfrak { P }\) f \(\mathbf { B }\) which divide a prime ideal \(\mathfrak { p }\) ofAisat least1and at most n.If A has only finitely many ideals,then so hasB(which is therefore principal).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
If \(\mathfrak P\) is a non-zero prime of \(B\) over \(\mathfrak p=A\cap\mathfrak P\), the valuation \(v_{\mathfrak P}\) prolongs \(v_{\mathfrak p}\) with index \(e_{\mathfrak P}\), meaning \(v_{\mathfrak P}(x)=e_{\mathfrak P}v_{\mathfrak p}(x)\) for \(x\in K\).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 11
Let \(w\) be a discrete valuation of \(L\) which prolongs \(v_{\mathfrak{p}}\) with index \(e\). Then there is a prime divisor \(\mathfrak{q}\) of \(\mathfrak{p}\) with \(w = v_{\mathfrak{q}}\) and \(e = e_{\mathfrak{q}}\).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
Let \(I_A\) and \(I_B\) be the ideal groups. For a non-zero prime \(\mathfrak p\) of \(A\) and a prime \(\mathfrak P\) of \(B\) above it, define \(i(\mathfrak p)=\mathfrak pB=\prod_{\mathfrak P\mid\mathfrak p}\mathfrak P^{e_{\mathfrak P}}\) and \(N(\mathfrak P)=\mathfrak p^{f_{\mathfrak P}}\); extending multiplicatively gives the inclusion and norm homomorphisms on ideal groups.
Formalized. Mathlib/RingTheory/Ideal/Norm/RelNorm.lean::Ideal.relNorm; Mathlib/RingTheory/Ideal/Operations.lean::Ideal.map — Extension of ideals and relative ideal norm give the two multiplicative homomorphisms on ideal groups.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Let \(\mathcal { C } _ { \mathbf { A } }\) be the category of A-modules offinite length.If \(\mathbb { M } \in \mathcal { E } _ { A }\) and if M is oflength \(\pmb { \mathcal { M } }\) Mhas a composition series: \(\Updownarrow\) \[ 0 = \mathbf { M } _ { 0 } \subset \mathbf { M } _ { 1 } \subset \cdots \subset \mathbf { M } _ { m } = \mathbf { M } , \] each \(\mathbf { M } _ { i } / \mathbf { M } _ { i - 1 }\) being isomorphic toa simple A-module,i.e., to a quotient \(A / \mathfrak { P } _ { i }\) where \({ \mathfrak { p } } _ { \mathfrak { i } }\) is a non-zero prime ideal ofA (ignoring the trivial case \(\mathbb { A } = \mathbb { K }\) 1 By the Jordan-Holder theorem, the sequence of \(\mathbb { A } _ { j } { \mathfrak { p } } _ { i }\) depends only on M (up to order),and one can put: \[ \chi _ { \mathrm { A } } ( \mathbf { M } ) = \prod _ { i = 1 } \mathfrak { p } _ { i } . \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Example / comparison
ExAMPLE.When \(\mathbb { M } = \mathbb { b } / \mathbb { a }\) ,whereaand \(\mathfrak { b }\) arenon-zero fractional ideals with \({ \mathfrak { a } } \subset { \mathfrak { z } }\) ,one has \(\gamma _ { \mathrm { { A } } } ( \mathbf { M } ) = 0 \mathrm { ~ . ~ } \mathbf { b } ^ { - 1 }\) Inparticular, \(\chi _ { \mathrm { A } } ( \mathrm { A } / \mathfrak { a } ) = \mathfrak { a }\) if \({ \mathfrak { a } } \subset { \mathfrak { A } }\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
Restriction of scalars gives an exact functor from finite-length \(B\)-modules to finite-length \(A\)-modules; on the corresponding ideal Grothendieck groups, the induced homomorphism is the norm \(N:I_B\to I_A\).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 12
Proposition12.If MisaB-moduleof finite length,then \(\chi _ { \mathrm { A } } ( \mathbf { M } ) = \mathbb { N } \{ \chi _ { \mathrm { B } } ( \mathbf { M } ) \} .\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 13
Proposition 13.IfMisanA-moduleoffinite length,then \(\chi _ { 3 } ( \mathrm { M _ { B } } ) = i \{ \chi _ { A } ( \mathrm { M } ) \}\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 14
Proposition 14. 1f \(x \in \mathbb { L }\) ,then \(\mathsf { N } \{ x \mathbf { B } \} = \mathsf { N } _ { \mathbf { L } / \mathbf { K } } \{ x \} \mathbf { A }\)
Formalized. Mathlib/RingTheory/Ideal/Norm/RelNorm.lean::Ideal.relNorm_singleton — The relative norm of a principal ideal is the principal ideal generated by the algebraic norm.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 3
Lemma 3.Let A be a principal ideal domain and \(u \colon \mathrm { A } ^ { n } \mathrm { A } ^ { n } \ .\) linear map with \(\mathrm { d e t } \{ \{ \boldsymbol { \imath } \} \neq 0 .\) Thende \(\mathfrak { X } \{ u \} \mathbf { A } = \chi _ { \mathbf { A } } \{ \mathbf { C o k e r } \ u \}\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Lemma 4
Lemma 4. Let \({ \mathfrak { m } } _ { \mathrm { i } } = \{ { \mathfrak { m } } , g _ { i } \}\) be the ideal of \(\mathtt { B } _ { f }\) generated by m and the canonical image of \({ \pmb q } _ { \pmb { i } }\) \(\mathbf { B } _ { f }\) ;the ideals \(\mathfrak { m } _ { 4 }\) \(i \in \mathbb { I } ,\) aremaximal and distinct,and every maximal ideal of \(\mathbf { B } _ { f }\) isequal tooneof them.Thequotient \(B _ { f } / \Im \Im _ { i }\) isisomorphic to the field \(k _ { i } = k [ \mathbf { X } ] / \{ \varphi _ { i } \} .\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 15
Proposition 15.If A is a discrete valuation ring,and if \(\vec { j }\) is irreducible, then \(\theta _ { f }\) is adiscrete vatuation ring with maximal ideal \(\mathfrak { m } \mathbb { B } _ { f }\) and residue field \(k [ X ] / ( 7 )\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary 1
Corollary1.IfKisthefieldof fractionsofA,thepolynomial \(f\) is irreducible inK[X].If \(\scriptstyle I ,\) denotesthe field \(\mathbb { K } \{ \mathbf { X } \} / \{ f \}\) thenthering \(\mathbf { \boldsymbol { \mathsf { B } } } _ { f }\) is the integral closure ofAinL.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary 2
Corollary 2.1f \(\vec { f }\) isaseparablepolynomial,the_extension \(L / K\) is unramified.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 16
Proposition 16.LetAbeadiscretevaluationring,Kits field of fractions,and letL bean extension of Kof finite degreen.Let B be the integral closure ofA inL.Suppose thatB isadiscretevaluation ring and that the residue fieldLofB isa simple extension of degree n of the residue feld \(k = \widetilde { \sf K }\) ofA.Let \(x\) be any element of B whose image \(\bar { x }\) in L generates L over \(k .\) and let \(f\) be the characteristicpolynomialof \(\pmb { x }\) overK.Then the homomorphism of \(\mathbf { A } \{ \mathbf { X } \}\) into Bthat maps \(\mathbf { X }\) onto \(\boldsymbol { \mathbf { \rho } } _ { \mathbf { x } }\) definesby passagetothequotient anisomorphism of \(\mathfrak { B } _ { f }\) onto \(\mathfrak { B }\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 17
Proposition 17. Suppose Ais \(^ a\) discrete raluation ring and that \(f\) has the following form: \[ f = { \mathbf { X } } ^ { n } + a _ { 1 } { \mathbf { X } } ^ { n - 1 } + \cdots + a _ { n } , \qquad a _ { i } \in { \mathfrak { n } } , a _ { n } \notin { \mathfrak { m } } ^ { 2 } . \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary: Corollary
Corollary. The polynomial \(f\) is irreducible in \(\mathsf { K } [ \mathbf { \boldsymbol { X } } ]\) and \(i f \downarrow = \mathbb { K } [ \mathbb { X } ] / ( f ) ,\) then \(\mathbf { B } _ { f }\) istheintegral closureofAin \(\mathbf { \lambda } _ { \mathbf { L } }\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 18
Proposition18.Let A be a discrete valuation ring,K its field of fractions, and letL bea finite extension of K of degreen.Let B be the integral closure ofAinL.Suppose that B isa discrete valuation ring,and that the associated valuation prolongs that of A with ramification index n.Let \(x\) be auniformizing elementofB,and let \(f\) be the characteristic polynomial of \(x\) over K.Then \(f\) is anEisenstein polynomial,and the homomorphism of \(\mathsf { A f X } ]\) into B that mapsX onto \(x\) definesby passage to the quotient an isomorphism of \(\mathtt { B } _ { f }\) onto B.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Convention / notation
We return now to the hypotheses and notation of paragraphs 4 and S,and we further assume that \(L / \mathbb { K }\) isa Galois extension,Its Galois group will be denoted \(\mathrm { G f } \left\{ 1 , / \mathrm { K } \right\}\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 19
Proposition 19.The group \(\mathrm { G } \{ { \bf L } / \mathrm { K } \}\) actstransitivelyon the setofprime ideals ofBdividinga given prime ideal \(\mathfrak { p }\) ofA.
Formalized. Mathlib/NumberTheory/RamificationInertia/Galois.lean::Ideal.isPretransitive_of_isGaloisGroup, exists_smul_eq_of_isGaloisGroup — The Galois group acts transitively on primes above a fixed prime.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary: Corollary.Let \(\mathfrak { p }\) bea non-zero prime ideal of A.The integers…
Corollary.Let \(\mathfrak { p }\) bea non-zero prime ideal of A.The integers \(e _ { \ P }\) and \(f _ { \ P }\) for \(\mathfrak { P }\) dividingp)dependonlyonp.Ifonedenotes themby \(e _ { p } , f _ { p } ,\) andi \({ \mathfrak { g } } _ { \mathfrak { p } }\) denotes thenumberof primeideals \(\mathfrak { P }\) dividingp,then \[ n = e _ { \mathfrak { p } } f _ { \mathfrak { p } } g _ { \mathfrak { p } } . \]
Formalized. Mathlib/NumberTheory/RamificationInertia/Galois.lean::ramificationIdx_eq_of_isGaloisGroup, inertiaDeg_eq_of_isGaloisGroup, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn — In the Galois case e and f are constant above p and the native cardinality formula is n=efg.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The subgroup of \(\mathrm { G } \{ { \bf { l } } / \mathrm { K } \}\) consisting of those s such that \(s \{ \mathfrak { P } \} \cong \mathfrak { P }\) is called the decomposition group of \(\mathfrak { P }\) in \(L / \mathbb { K }\) ；we denote it by \(\operatorname { I D } _ { \ P } ( \mathbf { L } / \mathbf { K } )\) or sometimes simply by D.If \(\mathfrak { P }\) isanother prime ideal ofB over the same ideal \(\mathfrak { p }\) ofA,prop.19 shows that \(\bf \delta D _ { \overline { { 3 } } } . ( \bf L / K )\) is conjugate to \(\bf { D } _ { \ P } \{ { \bf L } / \hbar \}\) The index of \(\mathfrak { D }\) in \(\operatorname { G } \{ \ 1 , \hbar \}\) is equal to the number \(g _ { \mathfrak { p } }\) of prime ideals of B dividing \(\mathfrak { p }\)
Formalized. Mathlib/RingTheory/Ideal/Over.lean::Ideal.stabilizer; Mathlib/NumberTheory/RamificationInertia/Galois.lean::card_stabilizer_eq — The decomposition group is the stabilizer of the chosen prime; orbit–stabilizer gives its index.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
Wenow fix the ideal \({ \mathfrak { P } } .\) and we write \({ \mathbb G } , { \mathbb D } , e , f , g\) instead of \(\mathrm { { G } \{ { L } / { K } \} , }\) \(\mathrm { D } _ { \mathfrak { p } } ( \mathrm { L } / \mathrm { K } ) , e _ { \mathfrak { p } } , f _ { \mathfrak { p } } , g _ { \mathfrak { p } }\) ByGalcis theory,the group \(\mathbf { p }\) corresponds to an extension \(\mathtt { K } _ { \mathtt { D } }\) ofK contained in L;this extension is only Galois when \(\mathfrak { D }\) is normal in G.We have: 1i \[ [ \mathsf { K } _ { \mathsf { D } } : \mathsf { K } ] = \mathsf { g } , \qquad [ \mathsf { L } : \mathsf { K } _ { \mathsf { D } } ] = e f , \qquad \mathsf { G } ( \mathrm { L } / \mathsf { K } _ { \mathsf { D } } ) = \mathsf { D } . \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
If E is a field between \(\mathbf { K }\) anj \(\texttt { \textbf { k } }\) let \(\mathbf { B } _ { \mathrm { E } } = \mathbf { E } \cap \mathbf { B }\) be the integral closure of A inE, \(\mathfrak { P } _ { \mathtt { E } } = \mathfrak { P } \cap \mathtt { B } _ { \mathtt { E } }\) and let \(\mathbf { \overline { { E } } }\) be the residue field \(\mathbf { B } _ { \mathbf { E } } / \mathfrak { P } _ { \ E }\) Thisapplies in particular to \(\mathbf { K }\) and \(\pmb { \downarrow }\) defining the fields \(\bar { \bf K }\) and \(\scriptstyle { \mathfrak { L } }\) IsED, \(\pmb { \mathscr { s } }\) defines by passage to the quotient a \(\bar { \bf K }\) -automorphism \(\Im\) of \(\pmb { \updownarrow }\) We thus obtain a homomorphism \[ \mathfrak { E } : \mathrm { D } \to \mathbf { G } ( \bar { \mathbf { L } } / \bar { \mathbf { K } } ) \]
Formalized. Mathlib/RingTheory/Ideal/Over.lean::Ideal.stabilizerHom, Ideal.ker_stabilizerHom — The residue action of the decomposition group and its kernel are exactly the stabilizer homomorphism and inertia group.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
whose kernel is called the inertia group of \(\mathfrak { P } _ { : }\) and is denoted \(\mathbb { T } _ { \mathfrak { s } ^ { \sharp } } ( \mathbf { 1 } _ { \mathfrak { s } / } \mathbf { K } )\) or simply T. Corresponding to it is a Galois extension \(\operatorname { \bf { K } } _ { \Upsilon } / \operatorname { \bf { K } } _ { \mathfrak { D } } ,\) with Galois group \(\mathbf { D } / \mathbf { T }\) ; one has \(\bf G ( \bf L / \bf K _ { \mathrm { T } } ) = T\)
Formalized. Mathlib/RingTheory/Ideal/Over.lean::Ideal.stabilizerHom, Ideal.ker_stabilizerHom — The residue action of the decomposition group and its kernel are exactly the stabilizer homomorphism and inertia group.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 20
Proposition 20. The residue extension \(E / \sqrt { K }\) is normal and the homomorphism \[ \varepsilon : \mathbb { D } \to \mathbf { G } ( \mathbf { \bar { L } } / \mathbf { \bar { K } } ) \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Convention / notation
We continue to denote by \(L _ { s }\) the largest separable extension of \(\pmb { \mathrm { K } }\) in \(\mathbb { \Gamma }\) We have just shown that it is a Galois extension ofR with Galois group \(\mathbf { D } / \mathbf { \widetilde { I } }\) Put: \[ f _ { 0 } = [ { \boldsymbol { \mathrm { L } } } _ { s } \colon { \boldsymbol { \mathrm { K } } } ] = [ { \boldsymbol { \mathrm { L } } } : { \boldsymbol { \mathrm { K } } } ] _ { s } \qquad p ^ { s } = [ { \boldsymbol { \mathrm { L } } } : { \boldsymbol { \mathrm { L } } } _ { s } ] = [ { \boldsymbol { \mathrm { L } } } : { \boldsymbol { \mathrm { K } } } ] _ { i } , \] so that \[ f = f _ { 0 } p ^ { s } . \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 21
Proposition 21.With notation as above, let $w , w _ { } , w _ { } , v $ be the discrete valuationsdefinedbytheideals \({ \mathfrak { P } } , { \mathfrak { P } } _ { \mathbb { T } } , { \mathfrak { P } } _ { \mathbb { D } } , { \mathfrak { P } }\) Then: a \([ \mathrm { L } : \mathbb { K } _ { \mathbb { T } } ] = e p ^ { \varsigma }\) \([ \mathbf { K } _ { \mathrm { f } } : \mathbf { K } _ { \mathrm { D } } ] = f _ { 0 }\) \([ \mathsf { K } _ { \mathbb { D } } \colon \mathsf { K } ] = g .\) \(\left. \dot { f } \right. \ w\) prolongs \(\boldsymbol { \ w } _ { \mathsf { T } }\) withindex \(e\) \(w _ { \updownarrow }\) and \(w _ { \mathbf { D } }\) prolong \(\mathfrak { v }\) with index 1. c \(K _ { 1 } = I _ { s }\) \(\overrightarrow { \mathbf { K } } _ { \mathfrak { V } } = \overleftarrow { \mathbf { K } }\) Inparticular, \([ \mathbb { L } ; \mathbb { K } _ { \mathbb { T } } ] = p ^ { s } , [ \mathbb { K } _ { \mathbb { T } } ; \mathbb { K } _ { \mathsf { D } } ] = f _ { 0 } , [ \mathbb { K } _ { \mathsf { D } } ; \mathbb { K } ] = 1 .\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Corollary: Corollary, If \(I / R\) is separable then it is a Galois extension with Galois…
Corollary, If \(I / R\) is separable then it is a Galois extension with Galois group \(\mathbf { D } / \mathbf { T }\) and we have \(\bar { \mathbf { K } } _ { \mathtt { T } } = \bar { \mathbf { L } } ,\) \(\begin{array} { r } { [ \mathbf { L } : \mathbf { K } _ { \mathbf { T } } ] = \pmb { \varrho } . } \end{array}\) \([ \mathsf { K } _ { \mathsf { T } } = \mathsf { K } _ { \mathsf { D } } ] = \mathsf { f } .\) \([ \mathsf { K } _ { \Omega } ; \mathsf { K } ] = g\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Convention / notation
With the same hypotheses as in prop.21,let E bea subfield of \(\mathbb { L }\) containing \(\kappa\) ; the groups \(\mathbb { D } \{ 1 , / \mathbb { E } \}\) and \(\operatorname { T } \{ \operatorname { L } / \operatorname { E } \}\) are well-defined;similarly,when \(\mathbb { E } / \mathbb { K }\) is Galois,the groups \(\scriptstyle \mathrm { ~ D ( E / K ) ~ }\) and \(\mathrm { T } \{ \mathrm { E } / \mathrm { K }\) arewell-defined.
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 22
Proposition 22 a \(\mathrm { D } ( \mathrm { L } / \mathrm { E } ) = \mathrm { D } ( \mathrm { L } / \mathrm { K } ) \cap \mathrm { G } ( \mathrm { L } / \mathrm { E } )\) and \(\begin{array} { r } { \mathfrak { T } ( \mathrm { L } / \mathrm { E } ) = \mathfrak { T } ( \mathrm { L } / \mathrm { K } ) \cap \mathrm { G } ( \mathrm { L } / \mathrm { E } ) , } \end{array}\) \(b ) \downarrow f \in / \ K\) is Galois,the diagram below is commutative,and its rows and columns are exact: \[ \begin{array} { c } { { 1 } } \\ { { \downarrow \downarrow \qquad \downarrow \qquad \downarrow } } \\ { { \downarrow \mathrm { T } ( \mathrm { L } / \mathrm { E } ) \mathrm { T } ( \mathrm { L } / \mathrm { K } ) \mathrm { T } ( \mathrm { E } / \mathrm { K } ) 1 } } \\ { { \downarrow \qquad \downarrow \nonumber } } \\ { { \downarrow \mathrm { D } ( \mathrm { L } / \mathrm { E } ) \mathrm { D } ( \mathrm { L } / \mathrm { K } ) \mathrm { D } ( \mathrm { E } / \mathrm { K } ) 1 } } \\ { { \downarrow \mathrm { G } ( \mathrm { L } / \mathrm { E } ) \mathrm { G } ( \mathrm { L } / \mathrm { K } ) \mathrm { G } ( \mathrm { E } / \mathrm { K } ) 1 } } \\ { { \downarrow \qquad \downarrow \qquad \downarrow \qquad \downarrow } } \\ { { \downarrow \qquad \downarrow \qquad \downarrow \qquad \downarrow } } \end{array} \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
For an unramified prime \(\mathfrak P\) above \(\mathfrak p\) with finite residue field of size \(q\), the Frobenius substitution \(s_{\mathfrak P}\) is the element of the decomposition group characterized by \(s_{\mathfrak P}(b)\equiv b^q\pmod{\mathfrak P}\) for all \(b\in B\); it generates the decomposition group and is also denoted \(\{\mathfrak P,L/K\}\).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Proposition 23
Proposition 23.Let E beasubfield of \(\mathtt { L }\) containing \(\kappa\) and let \(\mathfrak { P } _ { \Xi } = \mathfrak { P } \cap \mathfrak { E }\) Then: a \(( \mathfrak { P } , \mathbf { L } / \mathbf { E } ) = ( \mathfrak { P } , \mathbf { L } / \mathbf { K } ) ^ { f } .\) with \(f = [ \vec { \bf E } : \vec { \bf K } ]\) \(^ { \{ b \} }\) IfE is Galois over \(\kappa\) ,the image of \(\{ \mathfrak { P } , \mathbf { L } / \mathbf { K } \}\) in \(\mathrm { G } \{ { \bf E } / \mathbb { K } \}\) is \(\{ \mathcal { P } _ { \mathbb { E } } , \mathbb { E } / \mathbb { K } \}\)
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Definition / construction
In particular, if \(\mathrm { G } \{ \mathfrak { k } / \mathfrak { K } \}\) is abelian, \(\{ \mathfrak { P } , \mathbf { L } / \mathbf { K } \}\) depends only on \({ \mathfrak { p } } = { \mathfrak { P } } \cap { \mathbf { A } }\) ；i is theArtinsymbolof \(\pmb { \ p }\) and is denoted \(\{ { \mathfrak { p } } , \mathbf { L } / \mathbf { K } \}\) One defines by linearity the Artin symbol for any ideal a ofA that does not containa ramified prime,and one denotes it again by \(\{ \mathfrak { a } , \mathbf { L } / \mathbb { K } \}\) [the notations \[ { \Bigg ( } { \frac { \mathrm { L } / \mathrm { K } } { \mathrm { ~ \mathbf { q } ~ } } } { \Bigg ) } , \quad { \mathrm { o r ~ s i m p i y } } \quad { \Bigg ( } { \frac { \mathrm { L } } { \mathrm { ~ \mathbf { a } ~ } } } { \Bigg ) } , \] are also found in the literature].
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Artin Reciprocity Law
ArtinReciprocityLaw (cf.[3],[75],[94],[123]).LetLbea finite abelian extension ofa number fieldK,A thering ofintegers ofK,and \(\mathfrak { p } _ { \ i }\) the prime idealsofA thatramify in \(L / \mathbb { K }\) Then there exist positive integers \(n _ { i }\) such that the conditions (i） \(v _ { p _ { i } } \{ x \to 1 \} \geq n _ { i }\) for all i, \(x\) is positive in every real embedding of \(\aleph\) that is not induced by a real embedding ofL, imply \(\displaystyle \{ x \mathbf { A } , \mathbf { L } / \mathbf { K } \} = 1 .\) Furthermore, every automorphism \(\mathbf { s } \in \mathbf { G } \{ \mathbf { L } / \mathbf { K } \}\) is of the form \(\{ { \mathfrak { a } } , \mathbf { k } / \mathbf { K } \}\) for \(a\) suitable ideal a (in fact,one even hass=(p,L/K) for infinitely many prime ideals \(\mathfrak { p }\) of A).
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.
Example / comparison
EXAMPLE.Let n be a positive integer, \({ \bf K } = { \bf Q } ;\) and let \(\mathbf { L } = \mathbf { Q } ( \zeta _ { n } )\) be the field of nth roots of unity.The Galois group \(\operatorname { G f } [ \mathbb { K } ]\) is a subgroup \(\mathbf { G } ^ { \prime } \{ n \}\) of the group \(\mathbf { G } ( n )\) of invertible elements of \(\mathbf { Z } _ { i } / { \mathfrak { n } } \mathbf { Z }\) (cf.Bourbaki, Alg., Chap.V)； if \(x \in G ^ { \prime } ( n )\) ,the automorphism \(\pmb { \sigma _ { x } }\) associated to \(x\) transforms a root of unity \(\zeta _ { n }\) into its xth power.If \(\{ p , n \} = 1\) ,one sees easily (e.g., by using the results of Chap. IV, \(\ S 4 \}\) that \(p\) isunramified,and that the Artin symbol \(( { \mathfrak { p } } , \mathbb { L } / \mathbb { K } )\) is equal to \(\sigma _ { p }\) Itfollowsby linearitythat the Artinsymbolof \(\pmb { \alpha }\) positive integer m prime to nis equal to \(\sigma _ { m }\) Consequently, \(\mathrm { G } ^ { \prime } ( n ) = \mathrm { G } \{ n \}\) that is to say \[ [ \mathbf { L } : \mathbf { K } ] = \varphi ( n ) \]
Not formalized. No checked source-complete owner was found for this full commutative-algebra/ramification bundle after project, pinned/current Mathlib, and targeted external search.