Documentation

TauCeti.RingTheory.LaurentSeries.Valuation.Ring

The valuation ring of formal Laurent series #

For a field K, the valuation integers in K⸨X⸩ are the embedded power series LaurentSeries.powerSeries_as_subring K. This file identifies their local-ring structure with the X-adic structure of K⟦X⟧: the maximal ideal is generated by X, consists of the series of positive order, and is the kernel of the constant-coefficient map. Consequently, the residue field is canonically isomorphic to K, with the residue of a power series sent to its constant coefficient.

Main results #

source
instance TauCeti.LaurentSeries.powerSeriesAsSubringIsLocalRing (K : Type u_1) [Field K] :
IsLocalRing ↥(LaurentSeries.powerSeries_as_subring K)

The embedded power-series ring is local, by transport from the usual local-ring structure on K⟦X⟧.

source
theorem TauCeti.LaurentSeries.maximalIdeal_eq_idealOfDefinition (K : Type u_1) [Field K] :
IsLocalRing.maximalIdeal ↥(LaurentSeries.powerSeries_as_subring K) = Huber.LaurentSeries.idealOfDefinition K

The maximal ideal of the Laurent valuation ring is the ideal (X) used as its ideal of definition.

source
theorem TauCeti.LaurentSeries.mem_maximalIdeal_iff_valuation_lt_one (K : Type u_1) [Field K] (f : ↥(LaurentSeries.powerSeries_as_subring K)) :
f ∈ IsLocalRing.maximalIdeal ↥(LaurentSeries.powerSeries_as_subring K) ↔ Valued.v ↑f < 1

An element of the Laurent valuation ring is in its maximal ideal exactly when its valuation is strictly less than one.

source
theorem TauCeti.LaurentSeries.mem_maximalIdeal_iff_orderTop_pos (K : Type u_1) [Field K] (f : ↥(LaurentSeries.powerSeries_as_subring K)) :
f ∈ IsLocalRing.maximalIdeal ↥(LaurentSeries.powerSeries_as_subring K) ↔ 0 < HahnSeries.orderTop ↑f

An element of the Laurent valuation ring is in its maximal ideal exactly when it has positive Laurent order. This includes zero, whose orderTop is infinity.

source
noncomputable def TauCeti.LaurentSeries.constantCoeff (K : Type u_1) [Field K] :
↥(LaurentSeries.powerSeries_as_subring K) →+* K

The constant-coefficient homomorphism on the Laurent valuation ring.

Instances For
    source
    @[simp]
    theorem TauCeti.LaurentSeries.constantCoeff_apply (K : Type u_1) [Field K] (f : ↥(LaurentSeries.powerSeries_as_subring K)) :
    (constantCoeff K) f = (↑f).coeff 0

    The constant coefficient read through the power-series presentation equals the coefficient at Laurent exponent zero.

    source
    theorem TauCeti.LaurentSeries.constantCoeff_surj (K : Type u_1) [Field K] :
    Function.Surjective ⇑(constantCoeff K)

    Every coefficient occurs as the constant coefficient of a Laurent valuation integer.

    source
    theorem TauCeti.LaurentSeries.ker_constantCoeff_eq_maximalIdeal (K : Type u_1) [Field K] :
    RingHom.ker (constantCoeff K) = IsLocalRing.maximalIdeal ↥(LaurentSeries.powerSeries_as_subring K)

    The kernel of the constant-coefficient map is the maximal ideal of the Laurent valuation ring.

    source
    theorem TauCeti.LaurentSeries.mem_maximalIdeal_iff_constantCoeff_eq_zero (K : Type u_1) [Field K] (f : ↥(LaurentSeries.powerSeries_as_subring K)) :
    f ∈ IsLocalRing.maximalIdeal ↥(LaurentSeries.powerSeries_as_subring K) ↔ (constantCoeff K) f = 0

    An element of the Laurent valuation ring belongs to its maximal ideal exactly when its constant coefficient vanishes.

    source
    noncomputable def TauCeti.LaurentSeries.residueFieldEquiv (K : Type u_1) [Field K] :
    IsLocalRing.ResidueField ↥(LaurentSeries.powerSeries_as_subring K) ≃+* K

    The residue field of the Laurent valuation ring is canonically the coefficient field.

    Instances For
      source
      @[simp]
      theorem TauCeti.LaurentSeries.residueFieldEquiv_residue (K : Type u_1) [Field K] (f : ↥(LaurentSeries.powerSeries_as_subring K)) :
      (residueFieldEquiv K) ((IsLocalRing.residue ↥(LaurentSeries.powerSeries_as_subring K)) f) = (↑f).coeff 0

      Under the residue-field equivalence, the residue of a valuation integer is its constant coefficient.

      source
      @[simp]
      theorem TauCeti.LaurentSeries.residueFieldEquiv_symm_apply (K : Type u_1) [Field K] (c : K) :
      (residueFieldEquiv K).symm c = (IsLocalRing.residue ↥(LaurentSeries.powerSeries_as_subring K)) ((LaurentSeries.powerSeriesEquivSubring K) (PowerSeries.C c))

      The inverse residue-field equivalence sends a coefficient to the residue of the corresponding constant power series.