Algebraic extensions of a nonarchimedean local field #
The spectral norm extends the normalized absolute value of a nonarchimedean local field K
to every algebraic extension M/K. This file constructs the corresponding normed field,
topology and valuative relation, and proves uniqueness of the extended absolute value and
valuation class. The structures are named definitions, installed locally, so an existing
compatible topology or valuative relation acquires no instance diamond.
The valuation ring is the integral closure of 𝒪[K] in M. Algebra maps from algebraic
extensions preserve compatible valuations and therefore restrict to local maps of integer
rings and induce functorial embeddings of residue fields. Automorphisms preserve the valuation
and are continuous for its topology.
For finite-dimensional extensions, completeness and local compactness are proved in
TauCeti.NumberTheory.LocalField.FiniteExtension.Basic.
Main definitions #
TauCeti.algebraicExtensionNormedField: the spectral norm as a normed field.TauCeti.algebraicExtensionNormedFieldTopology: the topology of that norm.TauCeti.algebraicExtensionValuativeRel: the valuative relation of that norm.AlgHom.integerRingHom,AlgHom.residueFieldHom: the induced maps on integers and residues.
Main results #
TauCeti.algebraicExtensionNormedField_norm_unique: uniqueness of the extended absolute value.TauCeti.algebraicExtensionValuation_isEquiv: uniqueness of the extended valuation class.TauCeti.algebraicExtensionValuativeRel_eq: uniqueness of the extended valuative relation.TauCeti.algebraicExtensionNormedFieldTopology_eq: compatibility with a given valuative topology.AlgHom.valuativeExtension: algebra maps preserve the extended valuation.TauCeti.integerRing_eq_integralClosure: identification of the valuation ring with the integral closure of𝒪[K].
Implementation notes #
The norm is Mathlib's spectralNorm.normedField, applied after locally installing
normalizedNontriviallyNormedField K; completeness and ultrametricity of K come from
normalizedNormedField_completeSpace and normalizedNormedField_isUltrametricDist. The
valuative topology comes from Mathlib's NormedField.toValued. Uniqueness of the valuation
uses the integrality of the minimal polynomial of any element of spectral norm at most 1.
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 an algebraic 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.
Instances For
The topology on an algebraic extension M of a nonarchimedean local field K induced by the
norm of algebraicExtensionNormedField K M.
Instances For
The norm of algebraicExtensionNormedField K M is the spectral norm of M/K.
The norm of algebraicExtensionNormedField K M extends the normalized absolute value of K.
The norm of algebraicExtensionNormedField K M is the only real absolute value on M extending
the normalized absolute value of K.
The norm of algebraicExtensionNormedField K M is ultrametric.
The valuative relation on an algebraic extension M of a nonarchimedean local field K defined
by the norm of algebraicExtensionNormedField K M: x ≤ᵥ y exactly when ‖x‖ ≤ ‖y‖.
Instances For
The relation algebraicExtensionValuativeRel K M compares norms.
The valuative relation algebraicExtensionValuativeRel K M extends the valuative relation
of K.
The norm topology algebraicExtensionNormedFieldTopology K M is the valuative topology of
algebraicExtensionValuativeRel K M.
Uniqueness of the extended valuation #
A valuation w on an algebraic 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 an algebraic 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 an algebraic extension M of a
nonarchimedean local field K which restrict to the valuation class of K are equivalent.
For any valuative relation on an algebraic 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 an algebraic
extension M of a nonarchimedean local field K which extends that of K is the relation
algebraicExtensionValuativeRel K M of the spectral norm.
The topology algebraicExtensionNormedFieldTopology 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 an algebraic 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 an
algebraic extension M of a nonarchimedean local field K to a commutative ring N, with
valuative relations on M and N both extending that of K, makes N a valuative extension of
M through ι.toAlgebra.
Valuative extensions in a tower. Let M be an algebraic extension of a nonarchimedean
local field K, and N a commutative ring that is an M-algebra and a K-algebra in a scalar
tower. If the valuative relations on M and N both extend that of K, then the valuative
relation of N extends that of M, for the ambient algebra structure.
AlgHom.valuativeExtension states this for the algebra structure ι.toAlgebra of an algebra map
ι : M →ₐ[K] N. ValuativeExtension M N only involves algebraMap M N, and for
ι = IsScalarTower.toAlgHom K M N the algebraMap of ι.toAlgebra is algebraMap M N by
definition, so the field transfers to the ambient [Algebra M N] without change.
The ring of integers is the integral closure #
The integers of an algebraic extension are the integral elements. Let M be an algebraic
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 an algebraic 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 an algebraic 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.
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.
Instances For
The integer-ring equivalence acts by the original field equivalence.
Galois automorphisms are continuous. Every K-algebra automorphism of an algebraic
extension M of a nonarchimedean local field K is continuous for its valuative topology, since
it preserves the valuation.
A base-field algebra map from an algebraic extension to a compatible valued field restricts to an algebra map of integer rings.
Instances For
The integer-ring map acts by the original field map.
Restricting a composite embedding to integer rings gives the composite restrictions.
Restricting the identity embedding to integer rings gives the identity.
A K-embedding from an algebraic extension of a nonarchimedean local field to a compatible
valued field restricts to a local homomorphism of their rings of integers.
The embedding of residue fields induced by a K-embedding from an algebraic extension of a
nonarchimedean local field K to a compatible valued field. It is linear over the residue field
of K.
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.