Hahn 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
, with the most studied case being when Γ
is
a linearly ordered abelian group and R
is a field, in which case HahnSeries Γ R
is a
valued field, with value group Γ
.
These generalize Laurent series (with value group ℤ
), and Laurent series are implemented that way
in the file RingTheory/LaurentSeries
.
Main Definitions #
- If
Γ
is ordered andR
has zero, thenHahnSeries Γ R
consists of formal series overΓ
with coefficients inR
, whose supports are partially well-ordered. support x
is the subset ofΓ
whose coefficients are nonzero.single a r
is the Hahn series which has coefficientr
ata
and zero otherwise.orderTop x
is a minimal element ofWithTop Γ
wherex
has a nonzero coefficient ifx ≠ 0
, and is⊤
whenx = 0
.order x
is a minimal element ofΓ
wherex
has a nonzero coefficient ifx ≠ 0
, and is zero whenx = 0
.map
takes each coefficient of a Hahn series to its target under a zero-preserving map.embDomain
preserves coefficients, but embeds the index setΓ
in a larger poset.
References #
- [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]
If Γ
is linearly ordered and R
has zero, then HahnSeries Γ R
consists of
formal series over Γ
with coefficients in R
, whose supports are well-founded.
- coeff : Γ → R
The coefficient function of a Hahn Series.
- isPWO_support' : (Function.support self.coeff).IsPWO
Instances For
The support of a Hahn series is just the set of indices whose coefficients are nonzero. Notably, it is well-founded.
Equations
- x.support = Function.support x.coeff
Instances For
Equations
- HahnSeries.instZero = { zero := { coeff := 0, isPWO_support' := ⋯ } }
Equations
- HahnSeries.instInhabited = { default := 0 }
Equations
- ⋯ = ⋯
The map of Hahn series induced by applying a zero-preserving map to each coefficient.
Equations
- x.map f = { coeff := fun (g : Γ) => f (x.coeff g), isPWO_support' := ⋯ }
Instances For
Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product.
Equations
Instances For
Change a Hahn series on a lex product to a Hahn series with coefficients in a Hahn series.
Equations
- x.toIterate = { coeff := fun (g : Γ) => { coeff := fun (g' : Γ') => x.coeff (g, g'), isPWO_support' := ⋯ }, isPWO_support' := ⋯ }
Instances For
The equivalence between iterated Hahn series and Hahn series on the lex product.
Equations
- HahnSeries.iterateEquiv = { toFun := HahnSeries.ofIterate, invFun := HahnSeries.toIterate, left_inv := ⋯, right_inv := ⋯ }
Instances For
single a r
is the Hahn series which has coefficient r
at a
and zero otherwise.
Equations
- HahnSeries.single a = { toFun := fun (r : R) => { coeff := Pi.single a r, isPWO_support' := ⋯ }, map_zero' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The orderTop of a Hahn series x
is a minimal element of WithTop Γ
where x
has a nonzero
coefficient if x ≠ 0
, and is ⊤
when x = 0
.
Instances For
A leading coefficient of a Hahn series is the coefficient of a lowest-order nonzero term, or zero if the series vanishes.
Instances For
The order of a nonzero Hahn series x
is a minimal element of Γ
where x
has a
nonzero coefficient, the order of 0 is 0.
Instances For
Extends the domain of a HahnSeries
by an OrderEmbedding
.
Equations
- HahnSeries.embDomain f x = { coeff := fun (b : Γ') => if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }
Instances For
Construct a Hahn series from any function whose support is bounded below.
Equations
- HahnSeries.ofSuppBddBelow f hf = { coeff := f, isPWO_support' := ⋯ }