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

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

Instances

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

TODO

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

References

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

@[simp]

theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] (f : PowerSeries R) (n : ℕ) : (HahnSeries.toPowerSeries.symm 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

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

The ring HahnSeries ℕ R is isomorphic to PowerSeries R.

Equations

• One or more equations did not get rendered due to their size.

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 : ℕ} : (HahnSeries.toPowerSeries.symm f).coeff n = (PowerSeries.coeff R n) f

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

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

Equations

• HahnSeries.ofPowerSeries Γ R = (HahnSeries.embDomainRingHom (Nat.castAddMonoidHom Γ) ⋯ ⋯).comp HahnSeries.toPowerSeries.symm.toRingHom

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

theorem HahnSeries.ofPowerSeries_apply {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] (x : PowerSeries R) : (HahnSeries.ofPowerSeries Γ R) x = HahnSeries.embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (HahnSeries.toPowerSeries.symm 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

theorem HahnSeries.ofPowerSeries_X_pow {Γ : Type u_1} [StrictOrderedSemiring Γ] {R : Type u_3} [Semiring 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) : (HahnSeries.toMvPowerSeries.symm 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

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

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.

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 HahnSeries (σ →₀ ℕ) R has no zero divisors

Equations

• ⋯ = ⋯

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 : σ →₀ ℕ} : (HahnSeries.toMvPowerSeries.symm f).coeff n = (MvPowerSeries.coeff R 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) : (HahnSeries.toPowerSeriesAlg R) f = PowerSeries.mk f.coeff

@[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 : ℕ) : ((HahnSeries.toPowerSeriesAlg R).symm f).coeff n = (PowerSeries.coeff A 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 HahnSeries ℕ A is isomorphic to PowerSeries A.

Equations

• HahnSeries.toPowerSeriesAlg R = { toEquiv := HahnSeries.toPowerSeries.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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 : b ∈ Nat.cast '' ((HahnSeries.toPowerSeriesAlg R).symm a).support then (PowerSeries.coeff A (Classical.choose ⋯)) a else 0

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

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

Equations

• HahnSeries.ofPowerSeriesAlg Γ R = (HahnSeries.embDomainAlgHom (Nat.castAddMonoidHom Γ) ⋯ ⋯).comp ↑(HahnSeries.toPowerSeriesAlg R).symm

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

Equations

• HahnSeries.powerSeriesAlgebra Γ R = ((HahnSeries.ofPowerSeries Γ R).comp (algebraMap S (PowerSeries R))).toAlgebra

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

@[simp]

theorem Polynomial.algebraMap_hahnSeries_apply (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [StrictOrderedSemiring Γ] (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] [StrictOrderedSemiring Γ] : Function.Injective ⇑(algebraMap (Polynomial R) (HahnSeries Γ R))