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.

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 : ℕ) : ((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

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 : ℕ} : ((RingEquiv.symm HahnSeries.toPowerSeries) 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 = RingHom.comp (HahnSeries.embDomainRingHom (Nat.castAddMonoidHom Γ) ⋯ ⋯) (RingEquiv.toRingHom (RingEquiv.symm HahnSeries.toPowerSeries))

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 { 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

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.

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

@[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 : ℕ) : ((AlgEquiv.symm (HahnSeries.toPowerSeriesAlg R)) 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 = let __src := HahnSeries.toPowerSeries; { toEquiv := __src.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 : ∃ (x : ℕ), ¬(PowerSeries.coeff A x) a = 0 ∧ ↑x = b 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 = AlgHom.comp (HahnSeries.embDomainAlgHom (Nat.castAddMonoidHom Γ) ⋯ ⋯) ↑(AlgEquiv.symm (HahnSeries.toPowerSeriesAlg R))

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 = RingHom.toAlgebra (RingHom.comp (HahnSeries.ofPowerSeries Γ R) (algebraMap S (PowerSeries R)))

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))