Uniformizer coordinates on unit-filtration graded pieces

Fixing a uniformizer π identifies the mth positive graded piece of the unit filtration with the additive residue field: the class of u has coordinate (u - 1) / π ^ m modulo the maximal ideal. This file constructs that coordinate by composing the unit-filtration graded equivalence with the discrete-valuation-ring identification TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer, and computes how it changes when the uniformizer is replaced.

If π' = π * a for a unit a of the integer ring, then the coordinate relative to π is a ^ m times the coordinate relative to π'. Thus the identification is independent of the uniformizer up to the additive automorphism of the residue field induced by multiplication by the residue of a ^ m.

Main results

• TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer: the residue coordinate determined by a uniformizer.
• TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_ofMul_mk_eq_residue: its value on a representative whose difference from one is given explicitly.
• TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_change: changing the uniformizer scales the coordinate by the corresponding residue-field unit.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §2.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5.

noncomputable def TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (π : ↥(ValuativeRel.valuation K).integer) (hπ : Irreducible π) : Additive (UnitFiltrationGraded K (n + 1)) ≃+ IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer

The positive-depth unit-filtration coordinate associated to a uniformizer. The class of u ∈ U(K,n+1) is sent to the residue of (u - 1) / π^(n+1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_ofMul_mk {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (π : ↥(ValuativeRel.valuation K).integer) (hπ : Irreducible π) (x : ↥(unitFiltration K (n + 1))) : (residueFieldEquivMaximalIdealGradedOfUniformizer π hπ (n + 1)) ((unitFiltrationGradedSuccEquivResidueFieldOfUniformizer n π hπ) (Additive.ofMul ↑x)) = Submodule.Quotient.mk (unitFiltrationDifference n x)

The uniformizer coordinate of the class of u is characterized by multiplying it by π^(n+1): the result is the class of u - 1 in the maximal-ideal graded piece.

theorem TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_ofMul_mk_eq_residue {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (π : ↥(ValuativeRel.valuation K).integer) (hπ : Irreducible π) (x : ↥(unitFiltration K (n + 1))) (y : ↥(ValuativeRel.valuation K).integer) (hxy : ↑(unitFiltrationDifference n x) = y * π ^ (n + 1)) : (unitFiltrationGradedSuccEquivResidueFieldOfUniformizer n π hπ) (Additive.ofMul ↑x) = (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) y

If u - 1 = y * π^(n+1), then the uniformizer coordinate of the class of u is the residue of y. This is the representative form of the positive-depth graded equivalence used in ramification computations.

theorem TauCeti.unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_change {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (π π' : ↥(ValuativeRel.valuation K).integer) (hπ : Irreducible π) (hπ' : Irreducible π') (x : Additive (UnitFiltrationGraded K (n + 1))) : (unitFiltrationGradedSuccEquivResidueFieldOfUniformizer n π hπ) x = (uniformizerChangeResidueAddEquiv π π' hπ hπ' (n + 1)) ((unitFiltrationGradedSuccEquivResidueFieldOfUniformizer n π' hπ') x)

Coordinates attached to π and π' differ by multiplication by the residue of the (n+1)st power of the unit carrying π to π'.