Comparison between Hahn series and power series

If Γ is ordered and R has zero, then 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 R⟦Γ⟧. When R is a semiring and Γ = ℕ, then we get the more familiar semiring of formal power series with coefficients in R.

Main Definitions

• toPowerSeries the isomorphism from R⟦ℕ⟧ to PowerSeries R.
• ofPowerSeries the inverse, casting a PowerSeries R to a R⟦ℕ⟧.

Instances

• For Finite σ, the instance NoZeroDivisors R⟦σ →₀ ℕ⟧, deduced from the case of MvPowerSeries The case of R⟦ℕ⟧ is taken care of by instNoZeroDivisors.

TODO

• Build an API for the variable X (defined to be single 1 1 : R⟦Γ⟧) in analogy to X : R[X] and X : PowerSeries R

References

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]

def HahnSeries.toPowerSeries {R : Type u_2} [Semiring R] : HahnSeries ℕ R ≃+* PowerSeries R

The ring R⟦ℕ⟧ is isomorphic to PowerSeries R.

@[simp]

theorem HahnSeries.toPowerSeries_apply {R : Type u_2} [Semiring R] (f : HahnSeries ℕ R) : toPowerSeries f = PowerSeries.mk f.coeff

@[simp]

theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] (f : PowerSeries R) (n : ℕ) : (toPowerSeries.symm f).coeff n = (PowerSeries.coeff n) f

theorem HahnSeries.coeff_toPowerSeries {R : Type u_2} [Semiring R] {f : HahnSeries ℕ R} {n : ℕ} : (PowerSeries.coeff n) (toPowerSeries f) = f.coeff n

theorem HahnSeries.coeff_toPowerSeries_symm {R : Type u_2} [Semiring R] {f : PowerSeries R} {n : ℕ} : (toPowerSeries.symm f).coeff n = (PowerSeries.coeff n) f

def HahnSeries.ofPowerSeries (Γ : Type u_1) (R : Type u_2) [Semiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] : PowerSeries R →+* HahnSeries Γ R

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

theorem HahnSeries.ofPowerSeries_injective {Γ : Type u_1} {R : Type u_2} [Semiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] : Function.Injective ⇑(ofPowerSeries Γ R)

theorem HahnSeries.ofPowerSeries_apply {Γ : Type u_1} {R : Type u_2} [Semiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] (x : PowerSeries R) : (ofPowerSeries Γ R) x = embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm x)

theorem HahnSeries.ofPowerSeries_apply_coeff {Γ : Type u_1} {R : Type u_2} [Semiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] (x : PowerSeries R) (n : ℕ) : ((ofPowerSeries Γ R) x).coeff ↑n = (PowerSeries.coeff n) x

@[simp]

theorem HahnSeries.ofPowerSeries_C {Γ : Type u_1} {R : Type u_2} [Semiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] (r : R) : (ofPowerSeries Γ R) (PowerSeries.C r) = C r

@[simp]

theorem HahnSeries.ofPowerSeries_X {Γ : Type u_1} {R : Type u_2} [Semiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] : (ofPowerSeries Γ R) PowerSeries.X = (single 1) 1

theorem HahnSeries.ofPowerSeries_X_pow {Γ : Type u_1} [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] {R : Type u_3} [Semiring R] (n : ℕ) : (ofPowerSeries Γ R) (PowerSeries.X ^ n) = (single ↑n) 1

def HahnSeries.toMvPowerSeries {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R

The ring 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 Mathlib/Algebra/Order/Pi.lean the ring R⟦σ → ℕ⟧ could be constructed instead.

@[simp]

theorem HahnSeries.toMvPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] (f : MvPowerSeries σ R) : (toMvPowerSeries.symm f).coeff = f

@[simp]

theorem HahnSeries.toMvPowerSeries_apply {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] (f : HahnSeries (σ →₀ ℕ) R) (a✝ : σ →₀ ℕ) : toMvPowerSeries f a✝ = f.coeff a✝

instance HahnSeries.instNoZeroDivisorsFinsuppNat {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] [NoZeroDivisors R] : NoZeroDivisors (HahnSeries (σ →₀ ℕ) R)

If R has no zero divisors and σ is finite, then R⟦σ →₀ ℕ⟧ has no zero divisors

theorem HahnSeries.coeff_toMvPowerSeries {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] {f : HahnSeries (σ →₀ ℕ) R} {n : σ →₀ ℕ} : (MvPowerSeries.coeff n) (toMvPowerSeries f) = f.coeff n

theorem HahnSeries.coeff_toMvPowerSeries_symm {R : Type u_2} [Semiring R] {σ : Type u_3} [Finite σ] {f : MvPowerSeries σ R} {n : σ →₀ ℕ} : (toMvPowerSeries.symm f).coeff n = (MvPowerSeries.coeff n) f

def HahnSeries.toPowerSeriesAlg (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] : HahnSeries ℕ A ≃ₐ[R] PowerSeries A

The R-algebra A⟦ℕ⟧ is isomorphic to PowerSeries A.

@[simp]

theorem HahnSeries.toPowerSeriesAlg_symm_apply_coeff (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] (f : PowerSeries A) (n : ℕ) : ((toPowerSeriesAlg R).symm f).coeff n = (PowerSeries.coeff n) f

@[simp]

theorem HahnSeries.toPowerSeriesAlg_apply (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] (f : HahnSeries ℕ A) : (toPowerSeriesAlg R) f = PowerSeries.mk f.coeff

def HahnSeries.ofPowerSeriesAlg (Γ : Type u_1) (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] : PowerSeries A →ₐ[R] HahnSeries Γ A

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

@[simp]

theorem HahnSeries.ofPowerSeriesAlg_apply_coeff (Γ : Type u_1) (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] (a✝ : PowerSeries A) (b : Γ) : ((ofPowerSeriesAlg Γ R) a✝).coeff b = if h : b ∈ Nat.cast '' ((toPowerSeriesAlg R).symm a✝).support then (PowerSeries.coeff (Classical.choose ⋯)) a✝ else 0

instance HahnSeries.powerSeriesAlgebra (Γ : Type u_1) (R : Type u_2) [CommSemiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] {S : Type u_4} [CommSemiring S] [Algebra S (PowerSeries R)] : Algebra S (HahnSeries Γ R)

theorem HahnSeries.algebraMap_apply' (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] {S : Type u_4} [CommSemiring S] [Algebra S (PowerSeries R)] (x : S) : (algebraMap S (HahnSeries Γ R)) x = (ofPowerSeries Γ R) ((algebraMap S (PowerSeries R)) x)

@[simp]

theorem Polynomial.algebraMap_hahnSeries_apply (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] (f : Polynomial R) : (algebraMap (Polynomial R) (HahnSeries Γ R)) f = (HahnSeries.ofPowerSeries Γ R) ↑f

theorem Polynomial.algebraMap_hahnSeries_injective (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] : Function.Injective ⇑(algebraMap (Polynomial R) (HahnSeries Γ R))