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 #
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 fromSummable
in the valuation topology, because there are topologically summable families that do not satisfy the axioms ofHahnSeries.SummableFamily
, and formally summable families whose sums do not converge topologically.HahnSeries.SummableFamily.hsum
is the formal sum of a summable family.HahnSeries.SummableFamily.lsum
is the formal sum bundled as aLinearMap
.HahnSeries.SummableFamily.smul
is the summable family given by pointwise scalar multiplication of component Hahn series.HahnSeries.SummableFamily.mul
is the summable family given by pointwise multiplication.HahnSeries.SummableFamily.powers
is the summable family given by non-negative powers of a Hahn series, if the series has strictly positive order. If the series has non-positive order, then the summable family takes the junk value of zero.
Main results #
HahnSeries.isUnit_iff
: IfR
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 inR
.HahnSeries.SummableFamily.hsum_smul
:smul
is compatible withhsum
.HahnSeries.SummableFamily.hsum_mul
:mul
is compatible withhsum
. That is, the product of sums is equal to the sum of pointwise products.
TODO #
- Summable Pi families
References #
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.
Instances For
Equations
- HahnSeries.SummableFamily.instFunLike = { coe := HahnSeries.SummableFamily.toFun, coe_injective' := ⋯ }
Equations
- HahnSeries.SummableFamily.instAdd = { add := fun (x y : HahnSeries.SummableFamily Γ R α) => { toFun := ⇑x + ⇑y, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
Equations
- HahnSeries.SummableFamily.instInhabited = { default := 0 }
Equations
- One or more equations did not get rendered due to their size.
The coefficient function of a summable family, as a finsupp on the parameter type.
Equations
Instances For
The infinite sum of a SummableFamily
of Hahn series.
Instances For
Alias of HahnSeries.SummableFamily.coeff_hsum
.
Alias of HahnSeries.SummableFamily.coeff_hsum_eq_sum_of_subset
.
The summable family made of a single Hahn series.
Equations
- HahnSeries.SummableFamily.single x = { toFun := fun (x_1 : Unit) => x, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
A summable family induced by an equivalence of the parametrizing type.
Equations
- HahnSeries.SummableFamily.Equiv e s = { toFun := fun (b : β) => s (e.symm b), isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
The summable family given by multiplying every series in a summable family by a scalar.
Equations
- HahnSeries.SummableFamily.smulFamily f s = { toFun := fun (a : α) => f a • s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
Equations
- HahnSeries.SummableFamily.instNeg = { neg := fun (s : HahnSeries.SummableFamily Γ R α) => { toFun := fun (a : α) => -s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
An elementwise scalar multiplication of one summable family on another.
Equations
- s.smul t = { toFun := fun (ab : α × β) => (HahnModule.of R).symm (s ab.1 • (HahnModule.of R) (t ab.2)), isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
Alias of HahnSeries.SummableFamily.smul
.
An elementwise scalar multiplication of one summable family on another.
Instances For
Alias of HahnSeries.SummableFamily.coeff_smul
.
Alias of HahnSeries.SummableFamily.smul_hsum
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The summation of a summable_family
as a LinearMap
.
Equations
- HahnSeries.SummableFamily.lsum = { toFun := HahnSeries.SummableFamily.hsum, map_add' := ⋯, map_smul' := ⋯ }
Instances For
A summable family given by pointwise multiplication of a pair of summable families.
Equations
Instances For
Alias of HahnSeries.SummableFamily.coeff_hsum_mul
.
A family with only finitely many nonzero elements is summable.
Equations
- HahnSeries.SummableFamily.ofFinsupp f = { toFun := ⇑f, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
A summable family can be reindexed by an embedding without changing its sum.
Equations
Instances For
A summable family of powers of a Hahn series x
. If x
has non-positive orderTop
, then
return a junk value given by pretending x = 0
.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.