Documentation

Mathlib.RingTheory.LaurentSeries

Laurent Series #

In this file we define LaurentSeries R, the formal Laurent series over R, here an arbitrary type with a zero. They are denoted R⸨X⸩.

Main Definitions #

Main Results #

About the X-Adic valuation: #

Implementation details #

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

LaurentSeries R is the type of formal Laurent series with coefficients in R, denoted R⸨X⸩.

It is implemented as a HahnSeries with value group .

Equations
Instances For

    R⸨X⸩ is notation for LaurentSeries R.

    Equations
    Instances For

      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
        @[simp]
        theorem LaurentSeries.hasseDeriv_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ) (f : LaurentSeries V) (n : ) :
        ((hasseDeriv R k) f).coeff n = Ring.choose (n + k) k f.coeff (n + k)
        @[simp]
        theorem LaurentSeries.hasseDeriv_single_add {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ) (n : ) (x : V) :
        (hasseDeriv R k) ((HahnSeries.single (n + k)) x) = (HahnSeries.single n) (Ring.choose (n + k) k x)
        @[simp]
        theorem LaurentSeries.hasseDeriv_single {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ) (n : ) (x : V) :
        theorem LaurentSeries.hasseDeriv_comp_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k l : ) (f : LaurentSeries V) (n : ) :
        ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k (hasseDeriv R (k + l)) f).coeff n
        @[simp]
        theorem LaurentSeries.hasseDeriv_comp {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k l : ) (f : LaurentSeries V) :
        (hasseDeriv R k) ((hasseDeriv R l) f) = (k + l).choose k (hasseDeriv R (k + l)) f

        The derivative of a Laurent series.

        Equations
        Instances For
          @[simp]
          theorem LaurentSeries.derivative_apply {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (f : LaurentSeries V) :
          (derivative R) f = (hasseDeriv R 1) f
          theorem LaurentSeries.derivative_iterate {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ) (f : LaurentSeries V) :
          (⇑(derivative R))^[k] f = k.factorial (hasseDeriv R k) f
          @[simp]
          theorem LaurentSeries.derivative_iterate_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ) (f : LaurentSeries V) (n : ) :
          ((⇑(derivative R))^[k] f).coeff n = (descPochhammer k).smeval (n + k) f.coeff (n + k)

          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

            The localization map from power series to Laurent series.

            theorem PowerSeries.coeff_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) (i : ) :
            @[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) :
            @[simp]
            theorem RatFunc.single_inv {F : Type u} [Field F] (d : ) {α : F} ( : α 0) :

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

            Equations
            Instances For
              @[simp]

              The integral valuation of the power series X : K⟦X⟧ equals (ofAdd -1) : ℤᵐ⁰.

              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.eq_coeff_of_valuation_sub_lt (K : Type u_2) [Field K] {d n : } {f g : LaurentSeries K} (H : Valued.v (g - f) (Multiplicative.ofAdd (-d))) :
              n < dg.coeff n = f.coeff n
              def LaurentSeries.Cauchy.coeff {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) :
              K

              Since extracting coefficients is uniformly continuous, every Cauchy filter in K⸨X⸩ gives rise to a Cauchy filter in K for every d : ℤ, and such Cauchy filter in K converges to a principal filter

              Equations
              Instances For
                theorem LaurentSeries.Cauchy.coeff_tendsto {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) (D : ) :
                Filter.Tendsto (fun (f : LaurentSeries K) => f.coeff D) (Filter.principal {coeff hℱ D})
                theorem LaurentSeries.Cauchy.exists_lb_eventual_support {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) :
                ∃ (N : ), ∀ᶠ (f : LaurentSeries K) in , n < N, f.coeff n = 0
                theorem LaurentSeries.Cauchy.exists_lb_support {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) :
                ∃ (N : ), n < N, coeff hℱ n = 0
                def LaurentSeries.Cauchy.limit {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) :

                To any Cauchy filter ℱ of K⸨X⸩, we can attach a laurent series that is the limit of the filter. Its d-th coefficient is defined as the limit of Cauchy.coeff hℱ d, which is again Cauchy but valued in the discrete space K. That sufficiently negative coefficients vanish follows from Cauchy.coeff_support_bddBelow

                Equations
                Instances For
                  theorem LaurentSeries.Cauchy.exists_lb_coeff_ne {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) :
                  ∃ (N : ), ∀ᶠ (f : LaurentSeries K) in , d < N, coeff hℱ d = f.coeff d
                  theorem LaurentSeries.Cauchy.coeff_eventually_equal {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) {D : } :
                  ∀ᶠ (f : LaurentSeries K) in , d < D, coeff hℱ d = f.coeff d
                  theorem LaurentSeries.Cauchy.eventually_mem_nhds {K : Type u_2} [Field K] { : Filter (LaurentSeries K)} (hℱ : Cauchy ) {U : Set (LaurentSeries K)} (hU : U nhds (limit hℱ)) :
                  ∀ᶠ (f : LaurentSeries K) in , f U
                  theorem LaurentSeries.exists_ratFunc_val_lt {K : Type u_2} [Field K] (f : LaurentSeries K) (γ : (WithZero (Multiplicative ))ˣ) :
                  ∃ (Q : RatFunc K), Valued.v (f - (algebraMap (RatFunc K) (LaurentSeries K)) Q) < γ

                  For every Laurent series f and every γ : ℤᵐ⁰ one can find a rational function Q such that the X-adic valuation v satisfies v (f - Q) < γ.

                  @[reducible, inline]

                  The X-adic completion as an abstract completion of RatFunc K

                  Equations
                  Instances For

                    Having established that the K⸨X⸩ is complete and contains RatFunc K as a dense subspace, it gives rise to an abstract completion of RatFunc K.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible, inline]

                      Reinterpret the extension of coe : RatFunc K → K⸨X⸩ as a ring homomorphism

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev LaurentSeries.RatFuncAdicCompl (K : Type u_2) [Field K] :
                        Type u_2

                        An abbreviation for the X-adic completion of RatFunc K

                        Equations
                        Instances For
                          @[reducible, inline]

                          The uniform space isomorphism between two abstract completions of ratfunc K

                          Equations
                          Instances For
                            @[reducible, inline]

                            The uniform space equivalence between two abstract completions of ratfunc K as a ring equivalence: this will be the inverse of the fundamental one.

                            Equations
                            Instances For
                              @[reducible, inline]

                              The uniform space equivalence between two abstract completions of ratfunc K as a ring equivalence: it goes from K⸨X⸩ to RatFuncAdicCompl K

                              Equations
                              Instances For

                                The algebra equivalence between K⸨X⸩ and the X-adic completion of RatFunc X

                                Equations
                                Instances For
                                  @[reducible, inline]

                                  In order to compare K⟦X⟧ with the valuation subring in the X-adic completion of RatFunc K we consider its alias as a subring of K⸨X⸩.

                                  Equations
                                  Instances For
                                    @[reducible, inline]

                                    The ring isomorphism between K⟦X⟧ and the unit ball inside the X-adic completion of RatFunc K.

                                    Equations
                                    Instances For

                                      The algebra isomorphism between K⟦X⟧ and the unit ball inside the X-adic completion of RatFunc K.

                                      Equations
                                      Instances For