Documentation

Mathlib.RingTheory.LaurentSeries

Laurent Series #

Main Definitions #

Main Results #

About the X-Adic valuation: #

Implementation details #

@[reducible, inline]
abbrev LaurentSeries (R : Type u) [Zero R] :

A LaurentSeries is implemented as a HahnSeries with value group .

Equations
Instances For
    @[simp]
    theorem LaurentSeries.hasseDeriv_apply (R : Type u_2) {V : Type u_3} [AddCommGroup V] [Semiring R] [Module R V] (k : ) (f : LaurentSeries V) :
    (LaurentSeries.hasseDeriv R k) f = HahnSeries.ofSuppBddBelow (fun (n : ) => Ring.choose (n + k) k f.coeff (n + k))

    The Hasse derivative of Laurent series, as a linear map.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem LaurentSeries.hasseDeriv_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ) (f : LaurentSeries V) (n : ) :
      ((LaurentSeries.hasseDeriv R k) f).coeff n = Ring.choose (n + k) k f.coeff (n + k)
      Equations
      @[simp]
      theorem LaurentSeries.coeff_coe_powerSeries {R : Type u_1} [Semiring R] (x : PowerSeries R) (n : ) :
      ((HahnSeries.ofPowerSeries R) x).coeff n = (PowerSeries.coeff R n) x

      This is a power series that can be multiplied by an integer power of X to give our Laurent series. If the Laurent series is nonzero, powerSeriesPart has a nonzero constant term.

      Equations
      Instances For
        @[simp]
        theorem LaurentSeries.powerSeriesPart_coeff {R : Type u_1} [Semiring R] (x : LaurentSeries R) (n : ) :
        (PowerSeries.coeff R n) x.powerSeriesPart = x.coeff (HahnSeries.order x + n)
        @[simp]
        theorem LaurentSeries.powerSeriesPart_eq_zero {R : Type u_1} [Semiring R] (x : LaurentSeries R) :
        x.powerSeriesPart = 0 x = 0
        Equations

        The localization map from power series to Laurent series.

        Equations
        • =
        theorem PowerSeries.coeff_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) (i : ) :
        ((HahnSeries.ofPowerSeries R) f).coeff i = if i < 0 then 0 else (PowerSeries.coeff R i.natAbs) f
        theorem PowerSeries.coe_C {R : Type u_1} [Semiring R] (r : R) :
        (HahnSeries.ofPowerSeries R) ((PowerSeries.C R) r) = HahnSeries.C r
        @[simp]
        theorem PowerSeries.coe_smul {R : Type u_1} [Semiring R] {S : Type u_3} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) :

        The coercion RatFunc F → LaurentSeries F as bundled alg hom.

        Equations
        Instances For

          The coercion RatFunc F → LaurentSeries F as a function.

          This is the implementation of coeToLaurentSeries.

          Equations
          Instances For
            Equations
            • RatFunc.coeToLaurentSeries = { coe := RatFunc.coeToLaurentSeries_fun }
            theorem RatFunc.coe_def {F : Type u} [Field F] (f : RatFunc F) :
            f = (RatFunc.coeAlgHom F) f
            theorem RatFunc.coe_num_denom {F : Type u} [Field F] (f : RatFunc F) :
            f = (HahnSeries.ofPowerSeries F) f.num / (HahnSeries.ofPowerSeries F) f.denom
            theorem RatFunc.coe_injective {F : Type u} [Field F] :
            Function.Injective RatFunc.coeToLaurentSeries_fun
            @[simp]
            theorem RatFunc.coe_apply {F : Type u} [Field F] (f : RatFunc F) :
            (RatFunc.coeAlgHom F) f = f
            theorem RatFunc.coe_coe {F : Type u} [Field F] (P : Polynomial F) :
            (HahnSeries.ofPowerSeries F) P = P
            @[simp]
            theorem RatFunc.coe_zero {F : Type u} [Field F] :
            0 = 0
            theorem RatFunc.coe_ne_zero {F : Type u} [Field F] {f : Polynomial F} (hf : f 0) :
            f 0
            @[simp]
            theorem RatFunc.coe_one {F : Type u} [Field F] :
            1 = 1
            @[simp]
            theorem RatFunc.coe_add {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
            (f + g) = f + g
            @[simp]
            theorem RatFunc.coe_sub {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
            (f - g) = f - g
            @[simp]
            theorem RatFunc.coe_neg {F : Type u} [Field F] (f : RatFunc F) :
            (-f) = -f
            @[simp]
            theorem RatFunc.coe_mul {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
            (f * g) = f * g
            @[simp]
            theorem RatFunc.coe_pow {F : Type u} [Field F] (f : RatFunc F) (n : ) :
            (f ^ n) = f ^ n
            @[simp]
            theorem RatFunc.coe_div {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
            (f / g) = f / g
            @[simp]
            theorem RatFunc.coe_C {F : Type u} [Field F] (r : F) :
            (RatFunc.C r) = HahnSeries.C r
            @[simp]
            theorem RatFunc.coe_smul {F : Type u} [Field F] (f : RatFunc F) (r : F) :
            (r f) = r f
            @[simp]
            theorem RatFunc.coe_X {F : Type u} [Field F] :
            RatFunc.X = (HahnSeries.single 1) 1
            theorem RatFunc.single_one_eq_pow {R : Type u_2} [Ring R] (n : ) :
            theorem RatFunc.single_inv {F : Type u} [Field F] (d : ) {α : F} (hα : α 0) :
            Equations

            The prime ideal (X) of PowerSeries K, when K is a field, as a term of the HeightOneSpectrum.

            Equations
            Instances For
              theorem PowerSeries.intValuation_eq_of_coe {K : Type u_2} [Field K] (P : Polynomial K) :
              (Polynomial.idealX K).intValuation P = (PowerSeries.idealX K).intValuation P
              @[simp]
              theorem PowerSeries.intValuation_X {K : Type u_2} [Field K] :
              (PowerSeries.idealX K).intValuationDef PowerSeries.X = (Multiplicative.ofAdd (-1))

              The integral valuation of the power series X : K⟦X⟧ equals (ofAdd -1) : ℤₘ₀

              theorem RatFunc.valuation_eq_LaurentSeries_valuation (K : Type u_2) [Field K] (P : RatFunc K) :
              (Polynomial.idealX K).valuation P = (PowerSeries.idealX K).valuation P
              theorem LaurentSeries.valuation_X_pow (K : Type u_2) [Field K] (s : ) :
              Valued.v ((HahnSeries.ofPowerSeries K) PowerSeries.X ^ s) = (Multiplicative.ofAdd (-s))
              theorem LaurentSeries.valuation_single_zpow (K : Type u_2) [Field K] (s : ) :
              Valued.v ((HahnSeries.single s) 1) = (Multiplicative.ofAdd (-s))
              theorem LaurentSeries.coeff_zero_of_lt_intValuation (K : Type u_2) [Field K] {n : } {d : } {f : PowerSeries K} (H : Valued.v ((HahnSeries.ofPowerSeries K) f) (Multiplicative.ofAdd (-d))) :
              n < d(PowerSeries.coeff K n) f = 0
              theorem LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {d : } (f : PowerSeries K) :
              Valued.v ((HahnSeries.ofPowerSeries K) f) (Multiplicative.ofAdd (-d)) n < d, (PowerSeries.coeff K n) f = 0
              theorem LaurentSeries.coeff_zero_of_lt_valuation (K : Type u_2) [Field K] {n : } {D : } {f : LaurentSeries K} (H : Valued.v f (Multiplicative.ofAdd (-D))) :
              n < Df.coeff n = 0
              theorem LaurentSeries.valuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {D : } {f : LaurentSeries K} :
              Valued.v f (Multiplicative.ofAdd (-D)) n < D, f.coeff n = 0
              theorem LaurentSeries.eq_coeff_of_valuation_sub_lt (K : Type u_2) [Field K] {d : } {n : } {f : LaurentSeries K} {g : LaurentSeries K} (H : Valued.v (g - f) (Multiplicative.ofAdd (-d))) :
              n < dg.coeff n = f.coeff n
              theorem LaurentSeries.val_le_one_iff_eq_coe (K : Type u_2) [Field K] (f : LaurentSeries K) :
              Valued.v f 1 ∃ (F : PowerSeries K), (HahnSeries.ofPowerSeries K) F = f