Unramified extensions of local fields #
Let L/K be an extension of nonarchimedean local fields whose valuations are compatible, in the
sense of ValuativeExtension K L. This file defines the predicate
by the two conditions that the value group of K is carried onto that of L, in the form
ramificationIndex K L = 1, and that the residue extension π[L] / π[K] is separable. The
second condition is automatic here, because the residue field of a nonarchimedean local field is
finite and hence perfect, but it is the condition that makes the predicate the arithmetic notion
of unramifiedness for a general valued field, and it is what the comparison with the Γ©tale
notions rests on.
The file proves the equivalent forms of the predicate that later work uses: the value-group form,
the valuation form v_L β algebraMap = v_K, the ideal form π[K] πͺ[L] = π[L], the degree form
f(L/K) = [L : K], and the comparison with Algebra.FormallyUnramified πͺ[K] πͺ[L],
Algebra.IsUnramifiedAt πͺ[K] π[L] and Algebra.Etale πͺ[K] πͺ[L], which makes Mathlib's
unramifiedness and Γ©tale theory available for extensions of local fields. Unramifiedness is also
shown to be stable in a tower in both directions.
The ideal form is what makes the integers of an unramified extension a lattice modelled on the
residue extension: reduction modulo π[K] πͺ[L] = π[L] loses no generators, by
TauCeti.IsLocalRing.span_residue_image_eq_top_iff_span_eq_top, and the two extensions have the
same degree. Bases therefore correspond in both directions: a family of elements of πͺ[L]
lifting a basis of π[L] over π[K] is a basis of πͺ[L] over πͺ[K], and the reduction of a
basis of πͺ[L] over πͺ[K] is a basis of π[L] over π[K]. These integral bases are the
computational input to the norm and trace of an unramified extension.
Main definitions #
TauCeti.IsUnramified: an extension of nonarchimedean local fields is unramified when its ramification index is1and its residue extension is separable.TauCeti.IsUnramified.basisOfResidueBasis: the integral basis ofπͺ[L]overπͺ[K]given by a family lifting a basis ofπ[L]overπ[K].TauCeti.IsUnramified.residueBasis: the basis ofπ[L]overπ[K]given by the reduction of a basis ofπͺ[L]overπͺ[K].
Main results #
TauCeti.isUnramified_iff_ramificationIndex_eq_one: the separability condition is automatic, so the predicate ise(L/K) = 1.TauCeti.isUnramified_iff_normalizedValuation_comp_unitsMap_surjective:L/Kis unramified exactly when the normalized value group ofKis carried onto that ofL.TauCeti.isUnramified_iff_normalizedValuation_algebraMap:L/Kis unramified exactly when the normalized valuation ofLrestricts to that ofK.TauCeti.isUnramified_iff_map_maximalIdeal_eq:L/Kis unramified exactly whenπ[K]generatesπ[L].TauCeti.IsUnramified.irreducible_algebraMap: in an unramified extension a uniformizer ofKstays a uniformizer ofL.TauCeti.isUnramified_iff_inertiaDegree_eq_finrank:L/Kis unramified exactly whenf(L/K) = [L : K].TauCeti.IsUnramified.isTamelyRamified: an unramified extension is tamely ramified.TauCeti.isUnramified_tower_iff,TauCeti.IsUnramified.trans,TauCeti.IsUnramified.tower_botandTauCeti.IsUnramified.tower_top:M/Kis unramified exactly when both steps of a towerM/L/Kare.TauCeti.IsUnramified.ramificationIndex_tower_eq,TauCeti.IsUnramified.inertiaDegree_tower_eqandTauCeti.IsUnramified.isTotallyRamified_iff_finrank_eq: over an unramifiedL/K, the top stepM/Lhas the ramification index ofM/K, has residue degreef(M/K) / [L : K], and is totally ramified exactly when[L : K] = f(M/K).TauCeti.isUnramified_iff_formallyUnramified,TauCeti.isUnramified_iff_isUnramifiedAtandTauCeti.isUnramified_iff_etale: the comparison with Mathlib'sAlgebra.FormallyUnramified,Algebra.IsUnramifiedAtandAlgebra.Etaleforπͺ[L]overπͺ[K].TauCeti.IsUnramified.finrank_integerRing_eq_finrank_residueField: the rank ofπͺ[L]overπͺ[K]is the degree of the residue extension.TauCeti.IsUnramified.residueBasis_repr: the coordinates of a residue in the residue basis are the residues of the integral coordinates.TauCeti.IsUnramified.residueBasis_basisOfResidueBasisandTauCeti.IsUnramified.basisOfResidueBasis_residueBasis: the two constructions are mutually inverse.TauCeti.IsUnramified.exists_basis_residue_eq: every basis of the residue extension is the reduction of an integral basis.
References #
- J.-P. Serre, Corps Locaux, Chapter I, Β§4 and Chapter III, Β§5.
- J. Neukirch, Algebraic Number Theory, Chapter II, Β§7.
An extension L/K of nonarchimedean local fields with compatible valuations is
unramified when the normalized value group of K is carried onto that of L, that is
e(L/K) = 1, and the residue extension π[L] / π[K] is separable.
The separability condition is automatic for nonarchimedean local fields, whose residue fields
are finite and hence perfect; it is carried in the definition because it is what the notion means
for a general valued field, and it is one of the two halves of Mathlib's criterion
Algebra.FormallyUnramified.iff_map_maximalIdeal_eq.
The ramification index of an unramified extension is
1.- isSeparable_residueField : Algebra.IsSeparable (IsLocalRing.ResidueField β₯(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField β₯(ValuativeRel.valuation L).integer)
The residue extension of an unramified extension is separable.
Instances
An extension of nonarchimedean local fields is unramified exactly when e(L/K) = 1. The
residue extension of such an extension is automatically separable, its residue fields being
finite.
An extension of nonarchimedean local fields is unramified exactly when the normalized value
group of K is carried onto the normalized value group of L. This is the form the definition
takes for a general valued field: the map of value groups is injective in any case, so
unramifiedness is exactly its surjectivity.
An extension of nonarchimedean local fields is unramified exactly when the normalized
valuation of L restricts along the algebra map to the normalized valuation of K.
In an unramified extension the normalized valuation of L extends that of K.
An extension of nonarchimedean local fields is unramified exactly when the maximal ideal of
πͺ[K] generates the maximal ideal of πͺ[L].
In an unramified extension the maximal ideal of πͺ[K] generates the maximal ideal of
πͺ[L].
In an unramified extension a uniformizer of K stays a uniformizer of L.
An extension of nonarchimedean local fields is unramified exactly when its residue degree
is its degree, that is f(L/K) = [L : K].
In an unramified extension the residue degree is the degree of the extension.
An unramified extension of nonarchimedean local fields is tamely ramified: its ramification
index 1 is prime to the residue characteristic.
Unramifiedness in a tower M/L/K: the extension M/K is unramified exactly when both
L/K and M/L are.
Unramifiedness is transitive in a tower M/L/K.
The bottom step of an unramified tower is unramified.
The top step of an unramified tower is unramified.
Over an unramified L/K, the top step of a tower M/L/K has the ramification index of the
whole extension: e(M/L) = e(M/K).
Over an unramified L/K, the residue degree of a tower M/L/K factors as
f(M/K) = [L : K] Β· f(M/L).
Over an unramified L/K, the top step of a tower M/L/K is totally ramified exactly when
L/K already has the full residue degree f(M/K).
An extension of nonarchimedean local fields is unramified exactly when πͺ[L] is formally
unramified over πͺ[K].
An extension of nonarchimedean local fields is unramified exactly when πͺ[L] is unramified
over πͺ[K] at π[L], in Mathlib's sense.
An extension of nonarchimedean local fields is unramified exactly when πͺ[L] is Γ©tale over
πͺ[K].
The integral basis attached to a residue basis #
In an unramified extension the rank of πͺ[L] over πͺ[K] is the degree of the residue
extension. Both are the degree [L : K]. This is Mathlib's
IsLocalRing.finrank_eq_finrank_residueField for the Γ©tale extension πͺ[L]/πͺ[K] of
isUnramified_iff_etale, stated for local fields.
The integral basis of an unramified extension attached to a residue basis: a family in
πͺ[L] whose residues form a basis of π[L] over π[K] is a basis of πͺ[L] over πͺ[K].
Equations
- TauCeti.IsUnramified.basisOfResidueBasis b x hx = basisOfTopLeSpanOfCardEqFinrank x β― β―
Instances For
The residue basis of an integral basis of an unramified extension: the reduction of a
basis of πͺ[L] over πͺ[K] is a basis of π[L] over π[K]. This is Mathlib's
IsLocalRing.basisQuotient for the quotients by π[K] and π[K] πͺ[L], stated for the residue
fields themselves, which it identifies because π[K] πͺ[L] = π[L].
Equations
- TauCeti.IsUnramified.residueBasis B = basisOfTopLeSpanOfCardEqFinrank (β(IsLocalRing.residue β₯(ValuativeRel.valuation L).integer) β βB) β― β―
Instances For
The coordinates of the residue of x in the residue basis of B are the residues of the
coordinates of x in B.
Reducing the integral basis lifting a residue basis returns that residue basis.
Lifting the reduction of an integral basis returns that integral basis.
Every basis of the residue extension of an unramified extension is the reduction of a basis
of πͺ[L] over πͺ[K].