Uniformizer coordinates on maximal-ideal graded pieces

Let R be a discrete valuation ring with maximal ideal 𝔪 and residue field k. Fixing a uniformizer π identifies k with the graded piece 𝔪^m / 𝔪^(m+1) by sending the residue of x to the class of x * π ^ m. This file constructs that identification explicitly and computes how it changes when the uniformizer is replaced.

If π' = π * a for a unit a of R, then the identification for π' is the identification for π precomposed with multiplication by the residue of a ^ m. Thus it is independent of the uniformizer up to the additive automorphism of the residue field induced by that residue.

The explicit principal-power equivalence below follows the construction of Mathlib's Ideal.quotEquivPowQuotPowSucc, retaining a specified generator in order to expose the change-of-uniformizer formula.

Main results

• TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer: the identification of the residue field with a maximal-ideal graded piece determined by a uniformizer.
• TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer_change: changing the uniformizer scales the residue 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.uniformizerChangeUnit {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') : Rˣ

The unique unit a such that π * a = π', for two uniformizers π and π' of a discrete valuation ring.

Equations

• TauCeti.uniformizerChangeUnit π π' hπ hπ' = Exists.choose ⋯

@[simp]

theorem TauCeti.mul_uniformizerChangeUnit {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') : π * ↑(uniformizerChangeUnit π π' hπ hπ') = π'

The unit uniformizerChangeUnit π π' carries π to π'.

@[simp]

theorem TauCeti.uniformizerChangeUnit_self {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π : R) (hπ : Irreducible π) : uniformizerChangeUnit π π hπ hπ = 1

The change unit from a uniformizer to itself is one.

theorem TauCeti.uniformizerChangeUnit_mul {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π₁ π₂ π₃ : R) (h₁ : Irreducible π₁) (h₂ : Irreducible π₂) (h₃ : Irreducible π₃) : uniformizerChangeUnit π₁ π₂ h₁ h₂ * uniformizerChangeUnit π₂ π₃ h₂ h₃ = uniformizerChangeUnit π₁ π₃ h₁ h₃

Change units compose when passing through a third uniformizer.

noncomputable def TauCeti.uniformizerChangeResidueAddEquiv {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') (m : ℕ) : IsLocalRing.ResidueField R ≃+ IsLocalRing.ResidueField R

Multiplication by the mth power of the change unit, acting on the residue field. This is the additive coordinate change between the degree-m coordinates associated to two uniformizers.

Equations

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

@[simp]

theorem TauCeti.uniformizerChangeResidueAddEquiv_apply {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') (m : ℕ) (x : IsLocalRing.ResidueField R) : (uniformizerChangeResidueAddEquiv π π' hπ hπ' m) x = (IsLocalRing.residue R) ↑(uniformizerChangeUnit π π' hπ hπ') ^ m * x

The coordinate-change automorphism acts by multiplication by the residue of the change unit to the indicated power.

noncomputable def TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π : R) (hπ : Irreducible π) (m : ℕ) : IsLocalRing.ResidueField R ≃ₗ[R] ↥(IsLocalRing.maximalIdeal R ^ m) ⧸ IsLocalRing.maximalIdeal R • ⊤

Multiplication by a chosen uniformizer to the mth power identifies the residue field with the mth graded piece 𝔪^m / 𝔪^(m+1) of the maximal-ideal filtration.

Equations

• TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer π hπ m = LinearEquiv.ofBijective (TauCeti.residueToMaximalIdealGradedOfUniformizer✝ π hπ m) ⋯

@[simp]

theorem TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer_mk {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π : R) (hπ : Irreducible π) (m : ℕ) (x : R) : (residueFieldEquivMaximalIdealGradedOfUniformizer π hπ m) ((IsLocalRing.residue R) x) = Submodule.Quotient.mk ⟨x * π ^ m, ⋯⟩

The explicit principal-power equivalence sends the residue of x to the class of x * π ^ m.

theorem TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer_change {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') (m : ℕ) (x : IsLocalRing.ResidueField R) : (residueFieldEquivMaximalIdealGradedOfUniformizer π' hπ' m) x = (residueFieldEquivMaximalIdealGradedOfUniformizer π hπ m) ((uniformizerChangeResidueAddEquiv π π' hπ hπ' m) x)

Replacing π by π' = π * a in the principal-power equivalence is the same as first multiplying the residue coordinate by a ^ m.

theorem TauCeti.residueFieldEquivMaximalIdealGradedOfUniformizer_symm_change {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') (m : ℕ) (z : ↥(IsLocalRing.maximalIdeal R ^ m) ⧸ IsLocalRing.maximalIdeal R • ⊤) : (residueFieldEquivMaximalIdealGradedOfUniformizer π hπ m).symm z = (uniformizerChangeResidueAddEquiv π π' hπ hπ' m) ((residueFieldEquivMaximalIdealGradedOfUniformizer π' hπ' m).symm z)

In inverse coordinates, when π' = π * a, the coordinate relative to π equals the residue of a ^ m times the coordinate relative to π'.