Finite extensions of a nonarchimedean local field are local fields #
Let K be a nonarchimedean local field and let M be a field that is a finite-dimensional
K-algebra, with no topology or valuative relation assumed on M. Since K is complete for its
normalized absolute value (TauCeti.normalizedNormedField), the spectral norm of M/K is a
multiplicative ultrametric norm on M extending that absolute value, and it is the only absolute
value on M that does so. This file equips M with the resulting normed field, its topology,
and the valuative relation of the norm, and proves that with these structures M is a
nonarchimedean local field whose valuation extends that of K.
Completeness of K also makes this extension of the valuation unique: any valuation on M
restricting to the valuation class of K induces the order of the spectral norm, since an
element of spectral norm at most 1 has a minimal polynomial with integral coefficients. Hence
any valuative relation on M extending that of K is the one constructed here, any compatible
valuative topology on M is the norm topology, and every K-algebra automorphism of M
preserves the valuation. The same integrality of the minimal polynomial identifies the ring of
integers of M with the integral closure of that of K.
All structures are named definitions rather than global instances, so that a field already
carrying a compatible topology or valuative relation acquires no diamond. They are meant to be
installed locally, as in letI := finiteExtensionValuativeRel K M.
Main definitions #
TauCeti.finiteExtensionNormedField K M: the spectral norm ofM/Kas a normed field.TauCeti.finiteExtensionNormedFieldTopology K M: the topology of that norm.TauCeti.finiteExtensionValuativeRel K M: the valuative relation of that norm.
Main results #
TauCeti.finiteExtensionNormedField_norm_algebraMap: the norm extends the normalized absolute value ofK.TauCeti.finiteExtensionNormedField_norm_unique: it is the only absolute value onMdoing so.TauCeti.finiteExtensionNormedField_completeSpace:Mis complete for the norm.TauCeti.finiteExtension_valuativeExtension: the valuative relation onMextends that ofK.TauCeti.finiteExtension_isValuativeTopology: the norm topology is the valuative topology.TauCeti.finiteExtension_isNonarchimedeanLocalField:Mis a nonarchimedean local field.TauCeti.finiteExtensionNormedField_norm_le_norm_iff: a valuation onMrestricting to the valuation class ofKinduces the order of the spectral norm.TauCeti.finiteExtensionValuation_isEquiv: any two such valuations are equivalent.TauCeti.finiteExtensionValuativeRel_eq: any valuative relation onMextending that ofKisfiniteExtensionValuativeRel K M.TauCeti.finiteExtensionNormedFieldTopology_eq: any valuative topology for such a relation is the norm topology.AlgEquiv.valuation_eq:K-algebra automorphisms ofMpreserve the valuation.AlgEquiv.continuous_of_valuativeExtension:K-algebra automorphisms ofMare continuous.AlgHom.valuativeExtension: aK-algebra map fromMto a field whose valuative relation extends that ofKmakes that field a valuative extension ofM.Valuation.Integers.isIntegral_iff_valuation_le_one: for any valuative relation onMextending that ofK, an element ofMis integral over a ring of integers ofKexactly when its valuation is at most1.TauCeti.integerRing_eq_integralClosure:πͺ[M]is the integral closure ofπͺ[K]inM.TauCeti.integerRingEquivIntegralClosure: the resultingπͺ[K]-algebra equivalence betweenπͺ[M]and the integral closure ofπͺ[K]inM.AlgHom.integerRingHom: aK-algebra map of finite extensions restricts to anπͺ[K]-algebra map of their rings of integers.AlgHom.residueFieldHom: the resultingπ[K]-embedding of residue fields, which is functorial (AlgHom.residueFieldHom_comp,AlgHom.residueFieldHom_id); the restriction to rings of integers is local (AlgHom.isLocalHom_integerRingHom).
Implementation notes #
The norm is Mathlib's spectralNorm.normedField, applied after locally installing
normalizedNontriviallyNormedField K; the needed completeness and ultrametricity of K are
normalizedNormedField_completeSpace and normalizedNormedField_isUltrametricDist. The
valuative topology comes from Mathlib's NormedField.toValued, and local compactness of M
from FiniteDimensional.proper.
References #
- J. Neukirch, Algebraic Number Theory, Chapter II, Β§4 (Theorem 4.8) and Β§6.
- J.-P. Serre, Corps Locaux, Chapter II, Β§2.
The normed-field structure on a finite extension M of a nonarchimedean local field K
given by the spectral norm of M/K with respect to the normalized absolute value of K.
Equations
Instances For
The topology on a finite extension M of a nonarchimedean local field K induced by the
norm of finiteExtensionNormedField K M.
Equations
Instances For
The norm of finiteExtensionNormedField K M is the spectral norm of M/K.
The norm of finiteExtensionNormedField K M extends the normalized absolute value of K.
The norm of finiteExtensionNormedField K M is the only real absolute value on M extending
the normalized absolute value of K.
The norm of finiteExtensionNormedField K M is ultrametric.
A finite extension of a nonarchimedean local field is complete for the norm of
finiteExtensionNormedField K M.
The valuative relation on a finite extension M of a nonarchimedean local field K defined
by the norm of finiteExtensionNormedField K M: x β€α΅₯ y exactly when βxβ β€ βyβ.
Instances For
The relation finiteExtensionValuativeRel K M compares norms.
The valuative relation finiteExtensionValuativeRel K M extends the valuative relation
of K.
The norm topology finiteExtensionNormedFieldTopology K M is the valuative topology of
finiteExtensionValuativeRel K M.
A finite extension M of a nonarchimedean local field K, with the topology and valuative
relation of the spectral norm, is a nonarchimedean local field.
Uniqueness of the extended valuation #
A valuation w on a finite extension M of a nonarchimedean local field K which restricts
to the valuation class of K has the closed unit ball of the spectral norm of M/K as its
valuation ring.
A valuation w on a finite extension M of a nonarchimedean local field K which restricts
to the valuation class of K induces the same order on M as the spectral norm of M/K.
Uniqueness of the extended valuation. Any two valuations on a finite extension M of a
nonarchimedean local field K which restrict to the valuation class of K are equivalent.
For any valuative relation on a finite extension M of a nonarchimedean local field K
extending that of K, x β€α΅₯ y holds exactly when the spectral norm of x is at most that of
y.
Uniqueness of the extended valuative relation. A valuative relation on a finite extension
M of a nonarchimedean local field K which extends that of K is the relation
finiteExtensionValuativeRel K M of the spectral norm.
The topology finiteExtensionNormedFieldTopology K M of the spectral norm is the topology of
any valuative topological structure on M whose valuative relation extends that of K.
Galois invariance of the valuation. Every K-algebra automorphism of a finite extension
M of a nonarchimedean local field K preserves the canonical valuation of any valuative relation
on M extending that of K.
Embeddings respect the extended valuations. A K-algebra map ΞΉ : M ββ[K] N from a
finite extension M of a nonarchimedean local field K to a field N, for valuative relations
on M and on N both extending that of K, makes N a valuative extension of M through
ΞΉ.toAlgebra.
The ring of integers is the integral closure #
The integers of a finite extension are the integral elements. Let M be a finite
extension of a nonarchimedean local field K, with a valuative relation extending that of K,
and let O be any ring of integers of K, that is, (valuation K).Integers O. An element of
M is integral over O exactly when its valuation is at most 1; see Neukirch, Chapter II,
Β§4 and Β§6.
The ring of integers πͺ[M] of a finite extension M of a nonarchimedean local field K,
for a valuative relation extending that of K, is the integral closure of πͺ[K] in M.
The ring of integers πͺ[M] of a finite extension M of a nonarchimedean local field K,
as an πͺ[K]-algebra, is the integral closure of πͺ[K] in M; this is the equivalence given by
integerRing_eq_integralClosure.
Equations
Instances For
The equivalence integerRingEquivIntegralClosure does not change the underlying element.
The inverse of integerRingEquivIntegralClosure does not change the underlying element.
A base-field algebra equivalence restricts to an algebra equivalence of integer rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integer-ring equivalence acts by the original field equivalence.
A base-field algebra map restricts to an algebra map of integer rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integer-ring map acts by the original field map.
The algebra map of a finite compatible extension is continuous for the given valuative topologies.
Galois automorphisms are continuous. Every K-algebra automorphism of a finite extension
M of a nonarchimedean local field K is continuous for the valuative topology of M, since it
preserves the valuation.
A K-embedding of finite extensions of a nonarchimedean local field restricts to a local
homomorphism of their rings of integers.
The embedding of residue fields induced by a K-embedding of finite extensions of a
nonarchimedean local field K. It is linear over the residue field of K.
Equations
Instances For
The induced embedding of residue fields sends the residue of an integer x to the residue of
its image.
Passing to residue fields is functorial.
Passing the identity embedding to residue fields gives the identity embedding.