The unit filtration of a nonarchimedean local field #
For a nonarchimedean local field K this file defines the unit filtration
TauCeti.unitFiltration K i : Subgroup KΛ£,
the subgroup U(K,i) of those units of πͺ[K] that are congruent to 1 modulo π[K] ^ i.
The indexing is by natural numbers, and the depth-zero case is part of the definition rather
than a separate convention: π[K] ^ 0 = β€, so U(K,0) is the whole image of πͺ[K]Λ£ in KΛ£,
while U(K,i) = 1 + π[K] ^ i for i β₯ 1.
The filtration is the standard tool for resolving the multiplicative structure of K near 1.
Its steps are a neighbourhood basis of 1 in KΛ£, so they carry the topology of the unit group
and reduce statements about KΛ£ to statements about the finite quotients πͺ[K]Λ£ β§Έ U(K,i). Its
successive quotients are where ramification is measured: U(K,0) β§Έ U(K,1) is the multiplicative
group of the residue field and U(K,i) β§Έ U(K,i+1) is its additive group for i β₯ 1. Later work
uses the filtration in that role, through its graded pieces, its stability under the Galois
action on a finite extension, and its behaviour under a field embedding.
Main definitions #
TauCeti.unitFiltration: the unit filtrationU(K,i)of a nonarchimedean local field, as a subgroup ofKΛ£.TauCeti.unitFiltrationZeroEquivIntegerUnits: the depth-zero stepU(K,0)is the unit group ofπͺ[K].TauCeti.unitFiltrationToIntegerUnits: a unit ofKlying inU(K,i), read as a unit ofπͺ[K].
Main results #
TauCeti.mem_unitFiltration_iff_existsandTauCeti.mem_unitFiltration_succ_congr: the congruence form of membership,x β‘ 1 mod π[K] ^ iinsideπͺ[K].TauCeti.mem_unitFiltration_one_iff_residue_eq_one: a unit ofπͺ[K]lies inU(K,1)exactly when it reduces to1.TauCeti.mem_unitFiltration_iff_valuation_le,TauCeti.mem_unitFiltration_succ_valuationandTauCeti.mem_unitFiltration_iff_valuation_sub_one_le: the valuation form of membership, an inequality onx - 1measured against a uniformizer. At positive depth the inequality alone already forcesxto be a unit ofπͺ[K].TauCeti.unitFiltration_zeroandTauCeti.unitFiltration_one: the two shallow steps are Mathlib'sValuationSubring.unitGroupandValuationSubring.principalUnitGroup.TauCeti.unitFiltrationGradedZeroEquivResidueFieldUnits: reduction identifies the depth-zero graded piece with the multiplicative group of the residue field.TauCeti.unitFiltration_antitone: the filtration is decreasing.TauCeti.iInf_unitFiltration: the filtration separates points,β¨ i, U(K,i) = β₯.TauCeti.isOpen_unitFiltration,TauCeti.isCompact_unitFiltrationandTauCeti.hasBasis_nhds_one_unitFiltration: everyU(K,i)is an open compact subgroup ofKΛ£, and the family is a neighbourhood basis of1; in particularKΛ£is Hausdorff.TauCeti.unitFiltration_le_of_isClosed_of_le_sup: successive one-step approximations by a closed subgroup imply containment of the entire filtration step.
Implementation notes #
Two membership criteria are maintained. The congruence form is definitional and is the one used
for the algebraic statements; the valuation form is stated against an arbitrary uniformizer Ο
of K, which simultaneously records that the criterion does not depend on the choice of Ο.
The valuation appearing in the criteria is Mathlib's multiplicative ValuativeRel.valuation K,
for which greater depth means a smaller value and for which 0 is the smallest value; this is
what lets 1 belong to every step.
References #
- J.-P. Serre, Corps Locaux, Chapter IV, Β§2.
- J. Neukirch, Algebraic Number Theory, Chapter II, §§3β5.
The unit filtration U(K,i) of a nonarchimedean local field K: the units of πͺ[K] that
are congruent to 1 modulo π[K] ^ i, viewed inside KΛ£. The depth-zero step is included in
the definition through π[K] ^ 0 = β€, so that U(K,0) is the image of πͺ[K]Λ£, while
U(K,i) = 1 + π[K] ^ i for i β₯ 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in the unit filtration, congruence form: x is the image of a unit u of πͺ[K]
with u β‘ 1 mod π[K] ^ i.
Membership in the unit filtration at positive depth for a unit of πͺ[K]: the congruence
u β‘ 1 mod π[K] ^ (i + 1). The general-depth statement is mem_unitFiltration_iff_exists.
The depth-zero step of the unit filtration is the image of πͺ[K]Λ£ in KΛ£, that is, the set
of units of valuation one.
The depth-zero step of the unit filtration is Mathlib's unit group of the valuation subring
of K.
Membership in the unit filtration, valuation form: an inequality on x - 1 measured against
an arbitrary uniformizer Ο of K. The right-hand side is therefore independent of the choice
of Ο.
Membership in the unit filtration at positive depth, valuation form: the inequality on
x - 1 already forces x to be a unit of πͺ[K], so no further hypothesis is needed.
Membership in a positive-depth step of the unit filtration, as an inequality on x - 1
measured against a power of the valuation of a uniformizer Ο.
The depth-one step of the unit filtration is Mathlib's principal unit group of the valuation
subring of K.
The depth-zero graded piece #
Reduction modulo π[K] carries U(K,0), the units of πͺ[K], onto the multiplicative group
π[K]Λ£ of the residue field, and a unit reduces to 1 exactly when it lies in U(K,1). So
reduction has kernel U(K,1) and identifies the depth-zero graded piece U(K,0) / U(K,1) with
π[K]Λ£; in particular that quotient is finite of order q - 1, where q = #π[K].
The successive quotient U(K,i) / U(K,i+1) of the unit filtration.
Equations
- TauCeti.UnitFiltrationGraded K i = (β₯(TauCeti.unitFiltration K i) β§Έ (TauCeti.unitFiltration K (i + 1)).subgroupOf (TauCeti.unitFiltration K i))
Instances For
The depth-zero graded piece U(K,0) / U(K,1) is the multiplicative group of the residue
field. The isomorphism is induced by reduction modulo the maximal ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On a class represented by x β U(K,0), the depth-zero graded equivalence is reduction of
x modulo the maximal ideal.
The depth-zero graded piece is finite.
The first positive-depth step has finite relative index in the depth-zero step.
The depth-zero graded piece has q - 1 elements, where q is the cardinality of the residue
field.
The relative index [U(K,0) : U(K,1)] is one less than the cardinality of the residue
field.
The unit filtration is decreasing.
The unit filtration separates points: an element lying in every step is 1.
The filtration inside the units of πͺ[K] #
Every step of the filtration consists of units of πͺ[K], and at depth zero the step is exactly
the unit group of πͺ[K].
The depth-zero step U(K,0) of the unit filtration, as the unit group of πͺ[K].
Equations
Instances For
The identification of U(K,0) with πͺ[K]Λ£ does not move the underlying element of K.
The inverse identification of πͺ[K]Λ£ with U(K,0) does not move the underlying element of
K.
Every step of the unit filtration consists of units of πͺ[K]; this is the resulting
homomorphism U(K,i) β* πͺ[K]Λ£.
Equations
Instances For
Reading a step of the unit filtration in πͺ[K]Λ£ does not move the underlying element of
K.
Reading a step of the unit filtration in πͺ[K]Λ£ and back into KΛ£ is the identity.
Reading a step of the unit filtration in πͺ[K]Λ£ is injective.
A unit of πͺ[K] lies in the depth-one step U(K,1) of the unit filtration exactly when it
reduces to 1: the principal units are the kernel of reduction.
A principal unit reduces to 1.
On a class represented by x β U(K,0), the depth-zero graded equivalence is the residue of
x, read as an element of πͺ[K].
Each step of the unit filtration is a neighbourhood of 1 in KΛ£.
Each step of the unit filtration is an open subgroup of KΛ£.
The multiplicative group KΛ£ is Hausdorff: its identity {1} = β i, U(K,i) is closed.
Each step of the unit filtration is a compact subset of KΛ£.
The unit filtration is a neighbourhood basis of 1 in KΛ£.
A closed subgroup containing each U(K,n) modulo U(K,n+1) for i β€ n contains
U(K,i). Successive approximation gives containment modulo every deeper step, and the
unit-filtration neighbourhood basis then gives containment in the subgroup's closure.