Documentation

Mathlib.RingTheory.HahnSeries.PowerSeries

Comparison between Hahn series and power series #

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on HahnSeries Γ R. When R is a semiring and Γ = ℕ, then we get the more familiar semiring of formal power series with coefficients in R.

Main Definitions #

TODO #

References #

@[simp]
theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] (f : PowerSeries R) (n : ) :
((RingEquiv.symm HahnSeries.toPowerSeries) f).coeff n = (PowerSeries.coeff R n) f
@[simp]
theorem HahnSeries.toPowerSeries_apply {R : Type u_2} [Semiring R] (f : HahnSeries R) :
HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff

The ring HahnSeries ℕ R is isomorphic to PowerSeries R.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem HahnSeries.coeff_toPowerSeries {R : Type u_2} [Semiring R] {f : HahnSeries R} {n : } :
    (PowerSeries.coeff R n) (HahnSeries.toPowerSeries f) = f.coeff n
    theorem HahnSeries.coeff_toPowerSeries_symm {R : Type u_2} [Semiring R] {f : PowerSeries R} {n : } :
    ((RingEquiv.symm HahnSeries.toPowerSeries) f).coeff n = (PowerSeries.coeff R n) f

    Casts a power series as a Hahn series with coefficients from a StrictOrderedSemiring.

    Equations
    Instances For
      theorem HahnSeries.ofPowerSeries_apply {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] (x : PowerSeries R) :
      (HahnSeries.ofPowerSeries Γ R) x = HahnSeries.embDomain { toEmbedding := { toFun := Nat.cast, inj' := }, map_rel_iff' := } ((RingEquiv.symm HahnSeries.toPowerSeries) x)
      theorem HahnSeries.ofPowerSeries_apply_coeff {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] (x : PowerSeries R) (n : ) :
      ((HahnSeries.ofPowerSeries Γ R) x).coeff n = (PowerSeries.coeff R n) x
      @[simp]
      theorem HahnSeries.ofPowerSeries_C {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] (r : R) :
      (HahnSeries.ofPowerSeries Γ R) ((PowerSeries.C R) r) = HahnSeries.C r
      @[simp]
      theorem HahnSeries.ofPowerSeries_X {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] :
      (HahnSeries.ofPowerSeries Γ R) PowerSeries.X = (HahnSeries.single 1) 1
      @[simp]
      theorem HahnSeries.ofPowerSeries_X_pow {Γ : Type u_1} [StrictOrderedSemiring Γ] {R : Type u_3} [CommSemiring R] (n : ) :
      (HahnSeries.ofPowerSeries Γ R) (PowerSeries.X ^ n) = (HahnSeries.single n) 1
      @[simp]
      theorem HahnSeries.toMvPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] (f : MvPowerSeries σ R) :
      ((RingEquiv.symm HahnSeries.toMvPowerSeries) f).coeff = f
      @[simp]
      theorem HahnSeries.toMvPowerSeries_apply {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] (f : HahnSeries (σ →₀ ) R) :
      ∀ (a : σ →₀ ), HahnSeries.toMvPowerSeries f a = f.coeff a

      The ring HahnSeries (σ →₀ ℕ) R is isomorphic to MvPowerSeries σ R for a Finite σ. We take the index set of the hahn series to be Finsupp rather than pi, even though we assume Finite σ as this is more natural for alignment with MvPowerSeries. After importing Algebra.Order.Pi the ring HahnSeries (σ → ℕ) R could be constructed instead.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem HahnSeries.coeff_toMvPowerSeries {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] {f : HahnSeries (σ →₀ ) R} {n : σ →₀ } :
        (MvPowerSeries.coeff R n) (HahnSeries.toMvPowerSeries f) = f.coeff n
        theorem HahnSeries.coeff_toMvPowerSeries_symm {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] {f : MvPowerSeries σ R} {n : σ →₀ } :
        ((RingEquiv.symm HahnSeries.toMvPowerSeries) f).coeff n = (MvPowerSeries.coeff R n) f

        The R-algebra HahnSeries ℕ A is isomorphic to PowerSeries A.

        Equations
        • HahnSeries.toPowerSeriesAlg R = let __src := HahnSeries.toPowerSeries; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
        Instances For
          @[simp]
          theorem HahnSeries.ofPowerSeriesAlg_apply_coeff (Γ : Type u_1) (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] [StrictOrderedSemiring Γ] :
          ∀ (a : PowerSeries A) (b : Γ), ((HahnSeries.ofPowerSeriesAlg Γ R) a).coeff b = if h : ∃ (x : ), ¬(PowerSeries.coeff A x) a = 0 x = b then (PowerSeries.coeff A (Classical.choose )) a else 0

          Casting a power series as a Hahn series with coefficients from a StrictOrderedSemiring is an algebra homomorphism.

          Equations
          Instances For