Summable families of Hahn Series

We introduce a notion of formal summability for families of Hahn series, and define a formal sum function. This theory is applied to characterize invertible Hahn series whose coefficients are in a commutative domain.

Main Definitions

• A HahnSeries.SummableFamily is a family of Hahn series such that the union of the supports is partially well-ordered and only finitely many are nonzero at any given coefficient. Note that this is different from Summable in the valuation topology, because there are topologically summable families that do not satisfy the axioms of HahnSeries.SummableFamily, and formally summable families whose sums do not converge topologically.
• The formal sum, HahnSeries.SummableFamily.hsum can be bundled as a LinearMap via HahnSeries.SummableFamily.lsum.

Main results

• If R is a commutative domain, and Γ is a linearly ordered additive commutative group, then a Hahn series is a unit if and only if its leading term is a unit in R.

TODO

• Remove unnecessary domain hypotheses.
• More general summable families, e.g., define the evaluation homomorphism from a power series ring taking X to a positive order element.
• Generalize SMul to Hahn modules.

References

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

theorem HahnSeries.isPWO_iUnion_support_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (⋃ (n : ℕ), (x ^ n).support).IsPWO

structure HahnSeries.SummableFamily (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [AddCommMonoid R] (α : Type u_3) : Type (max (max u_1 u_2) u_3)

A family of Hahn series whose formal coefficient-wise sum is a Hahn series. For each coefficient of the sum to be well-defined, we require that only finitely many series are nonzero at any given coefficient. For the formal sum to be a Hahn series, we require that the union of the supports of the constituent series is partially well-ordered.

• toFun : α → HahnSeries Γ R

  A parametrized family of Hahn series.

• isPWO_iUnion_support' : (⋃ (a : α), (self.toFun a).support).IsPWO
• finite_co_support' : ∀ (g : Γ), {a : α | (self.toFun a).coeff g ≠ 0}.Finite

theorem HahnSeries.SummableFamily.isPWO_iUnion_support' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (self : HahnSeries.SummableFamily Γ R α) : (⋃ (a : α), (self.toFun a).support).IsPWO

theorem HahnSeries.SummableFamily.finite_co_support' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (self : HahnSeries.SummableFamily Γ R α) (g : Γ) : {a : α | (self.toFun a).coeff g ≠ 0}.Finite

instance HahnSeries.SummableFamily.instFunLike {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : FunLike (HahnSeries.SummableFamily Γ R α) α (HahnSeries Γ R)

Equations

• HahnSeries.SummableFamily.instFunLike = { coe := HahnSeries.SummableFamily.toFun, coe_injective' := ⋯ }

theorem HahnSeries.SummableFamily.isPWO_iUnion_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) : (⋃ (a : α), (s a).support).IsPWO

theorem HahnSeries.SummableFamily.finite_co_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) (g : Γ) : (Function.support fun (a : α) => (s a).coeff g).Finite

theorem HahnSeries.SummableFamily.coe_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Function.Injective DFunLike.coe

theorem HahnSeries.SummableFamily.ext {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} (h : ∀ (a : α), s a = t a) : s = t

instance HahnSeries.SummableFamily.instAdd {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Add (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instAdd = { add := fun (x y : HahnSeries.SummableFamily Γ R α) => { toFun := ⇑x + ⇑y, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }

instance HahnSeries.SummableFamily.instZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Zero (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instZero = { zero := { toFun := 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }

instance HahnSeries.SummableFamily.instInhabited {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Inhabited (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instInhabited = { default := 0 }

@[simp]

theorem HahnSeries.SummableFamily.coe_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : ⇑(s + t) = ⇑s + ⇑t

theorem HahnSeries.SummableFamily.add_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} {a : α} : (s + t) a = s a + t a

@[simp]

theorem HahnSeries.SummableFamily.coe_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : ⇑0 = 0

theorem HahnSeries.SummableFamily.zero_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {a : α} : 0 a = 0

instance HahnSeries.SummableFamily.instAddCommMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : AddCommMonoid (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instAddCommMonoid = AddCommMonoid.mk ⋯

def HahnSeries.SummableFamily.hsum {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) : HahnSeries Γ R

The infinite sum of a SummableFamily of Hahn series.

Equations

• s.hsum = { coeff := fun (g : Γ) => ∑ᶠ (i : α), (s i).coeff g, isPWO_support' := ⋯ }

@[simp]

theorem HahnSeries.SummableFamily.hsum_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {g : Γ} : s.hsum.coeff g = ∑ᶠ (i : α), (s i).coeff g

theorem HahnSeries.SummableFamily.support_hsum_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} : s.hsum.support ⊆ ⋃ (a : α), (s a).support

@[simp]

theorem HahnSeries.SummableFamily.hsum_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : (s + t).hsum = s.hsum + t.hsum

instance HahnSeries.SummableFamily.instNeg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} : Neg (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instNeg = { neg := fun (s : HahnSeries.SummableFamily Γ R α) => { toFun := fun (a : α) => -s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }

instance HahnSeries.SummableFamily.instAddCommGroup {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} : AddCommGroup (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instAddCommGroup = let __src := inferInstanceAs (AddCommMonoid (HahnSeries.SummableFamily Γ R α)); AddCommGroup.mk ⋯

@[simp]

theorem HahnSeries.SummableFamily.coe_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} : ⇑(-s) = -⇑s

theorem HahnSeries.SummableFamily.neg_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {a : α} : (-s) a = -s a

@[simp]

theorem HahnSeries.SummableFamily.coe_sub {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : ⇑(s - t) = ⇑s - ⇑t

theorem HahnSeries.SummableFamily.sub_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} {a : α} : (s - t) a = s a - t a

instance HahnSeries.SummableFamily.instSMul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} : SMul (HahnSeries Γ R) (HahnSeries.SummableFamily Γ R α)

Equations

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

@[simp]

theorem HahnSeries.SummableFamily.smul_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ R α} {a : α} : (x • s) a = x * s a

instance HahnSeries.SummableFamily.instModule {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} : Module (HahnSeries Γ R) (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instModule = Module.mk ⋯ ⋯

@[simp]

theorem HahnSeries.SummableFamily.hsum_smul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ R α} : (x • s).hsum = x * s.hsum

@[simp]

theorem HahnSeries.SummableFamily.lsum_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) : HahnSeries.SummableFamily.lsum s = s.hsum

def HahnSeries.SummableFamily.lsum {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} : HahnSeries.SummableFamily Γ R α →ₗ[HahnSeries Γ R] HahnSeries Γ R

The summation of a summable_family as a LinearMap.

Equations

• HahnSeries.SummableFamily.lsum = { toFun := HahnSeries.SummableFamily.hsum, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HahnSeries.SummableFamily.hsum_sub {Γ : Type u_1} [OrderedCancelAddCommMonoid Γ] {α : Type u_3} {R : Type u_4} [Ring R] {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : (s - t).hsum = s.hsum - t.hsum

def HahnSeries.SummableFamily.ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (f : α →₀ HahnSeries Γ R) : HahnSeries.SummableFamily Γ R α

A family with only finitely many nonzero elements is summable.

Equations

• HahnSeries.SummableFamily.ofFinsupp f = { toFun := ⇑f, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[simp]

theorem HahnSeries.SummableFamily.coe_ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {f : α →₀ HahnSeries Γ R} : ⇑(HahnSeries.SummableFamily.ofFinsupp f) = ⇑f

@[simp]

theorem HahnSeries.SummableFamily.hsum_ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {f : α →₀ HahnSeries Γ R} : (HahnSeries.SummableFamily.ofFinsupp f).hsum = f.sum fun (x : α) => id

def HahnSeries.SummableFamily.embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) : HahnSeries.SummableFamily Γ R β

A summable family can be reindexed by an embedding without changing its sum.

Equations

• s.embDomain f = { toFun := fun (b : β) => if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

theorem HahnSeries.SummableFamily.embDomain_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β} : (s.embDomain f) b = if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0

@[simp]

theorem HahnSeries.SummableFamily.embDomain_image {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {a : α} : (s.embDomain f) (f a) = s a

@[simp]

theorem HahnSeries.SummableFamily.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β} (h : b ∉ Set.range ⇑f) : (s.embDomain f) b = 0

@[simp]

theorem HahnSeries.SummableFamily.hsum_embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) : (s.embDomain f).hsum = s.hsum

def HahnSeries.SummableFamily.powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] (x : HahnSeries Γ R) (hx : 0 < x.orderTop) : HahnSeries.SummableFamily Γ R ℕ

The powers of an element of positive valuation form a summable family.

Equations

• HahnSeries.SummableFamily.powers x hx = { toFun := fun (n : ℕ) => x ^ n, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[simp]

theorem HahnSeries.SummableFamily.coe_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : ⇑(HahnSeries.SummableFamily.powers x hx) = HPow.hPow x

theorem HahnSeries.SummableFamily.embDomain_succ_smul_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (x • HahnSeries.SummableFamily.powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = HahnSeries.SummableFamily.powers x hx - HahnSeries.SummableFamily.ofFinsupp (Finsupp.single 0 1)

theorem HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (1 - x) * (HahnSeries.SummableFamily.powers x hx).hsum = 1

theorem HahnSeries.unit_aux {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R] (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1) : 0 < (1 - (HahnSeries.single (-x.order)) r * x).orderTop

theorem HahnSeries.isUnit_iff {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} : IsUnit x ↔ IsUnit x.leadingCoeff

instance HahnSeries.instField {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [Field R] : Field (HahnSeries Γ R)

Equations

• HahnSeries.instField = let __spread.0 := ⋯; Field.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯