Discrete valuation rings as power series quotients

TheoremPower series over a DVR modulo \(X - \varpi^e\) form a DVR#✓fully proved

Modulo X - ϖ ^ e, a power series ring over a discrete valuation ring is a discrete valuation ring, with uniformizer the image of ϖ.

theorem PowerSeries.isDiscreteValuationRing_quotient_span_X_sub_C_pow_of_irreducible
    {W : Type*} [CommRing W] [IsDomain W] [IsDiscreteValuationRing W]
    (ϖ : W) (hϖ : Irreducible ϖ) (e : ℕ) (he : 1 ≤ e) :
    ∃ (_ : IsDomain (PowerSeries W ⧸
        Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)}))
      (_ : IsDiscreteValuationRing (PowerSeries W ⧸
        Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)})),
      Irreducible (Ideal.Quotient.mk
        (Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)})
        (PowerSeries.C ϖ))

Used by 1

Used byPower series over a DVR modulo \(X - \varpi^e\) form a local PID

TheoremPower series over a DVR modulo \(X - \varpi^e\) form a local PID#✓fully proved

Modulo X - ϖ ^ e, a power series ring over a discrete valuation ring is a principal ideal ring and a local ring, and the image of ϖ is irreducible.

theorem PowerSeries.quotient_span_X_sub_C_pow_of_irreducible
    {W : Type*} [CommRing W] [IsDomain W] [IsDiscreteValuationRing W]
    (ϖ : W) (hϖ : Irreducible ϖ) (e : ℕ) (he : 1 ≤ e) :
    (Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)}).IsPrime ∧
    IsPrincipalIdealRing (PowerSeries W ⧸
      Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)}) ∧
    IsLocalRing (PowerSeries W ⧸
      Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)}) ∧
    Irreducible (Ideal.Quotient.mk
      (Ideal.span {(PowerSeries.X : PowerSeries W) - PowerSeries.C (ϖ ^ e)})
      (PowerSeries.C ϖ))

Uses 1 · Used by 1

Proof usesPower series over a DVR modulo \(X - \varpi^e\) form a DVR

Used byPower series over a DVR modulo \(X - \varpi\) form a complete DVR

TheoremPower series over a DVR modulo \(X - \varpi\) form a complete DVR#✓fully proved

Modulo X - ϖ, a power series ring over a discrete valuation ring is a discrete valuation ring, adically complete at its maximal ideal, with uniformizer the image of ϖ.

PowerSeries.isAdicComplete_quotient_span_X_sub_C_of_irreducible · 15 lines

theorem PowerSeries.isAdicComplete_quotient_span_X_sub_C_of_irreducible
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] (ϖ : O)
    (hϖ : Irreducible ϖ) :
    ∃ (_ : IsDomain (PowerSeries O ⧸
        Ideal.span {(PowerSeries.X : PowerSeries O) - PowerSeries.C ϖ}))
      (_ : IsDiscreteValuationRing (PowerSeries O ⧸
        Ideal.span {(PowerSeries.X : PowerSeries O) - PowerSeries.C ϖ}))
      (_ : IsAdicComplete
        (IsLocalRing.maximalIdeal (PowerSeries O ⧸
          Ideal.span {(PowerSeries.X : PowerSeries O) - PowerSeries.C ϖ}))
        (PowerSeries O ⧸
          Ideal.span {(PowerSeries.X : PowerSeries O) - PowerSeries.C ϖ})),
      Irreducible (Ideal.Quotient.mk
        (Ideal.span {(PowerSeries.X : PowerSeries O) - PowerSeries.C ϖ})
        (PowerSeries.C ϖ))

Uses 1

Proof usesPower series over a DVR modulo \(X - \varpi^e\) form a local PID

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.