Valuations on Hahn Series rings

If Γ is a linearly ordered cancellative monoid and R is a domain, then the domain R⟦Γ⟧ admits an additive valuation given by orderTop.

Main Definitions

• HahnSeries.addVal Γ R defines an AddValuation on R⟦Γ⟧ when Γ is linearly ordered.

TODO

• Multiplicative valuations
• Add any API for Laurent series valuations that do not depend on Γ = ℤ.

References

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

noncomputable def HahnSeries.addVal (Γ : Type u_1) (R : Type u_2) [AddCancelCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [IsDomain R] : AddValuation (HahnSeries Γ R) (WithTop Γ)

The additive valuation on R⟦Γ⟧ returning the smallest index at which a Hahn Series has a nonzero coefficient, or ⊤ for the 0 series.

Equations

• HahnSeries.addVal Γ R = AddValuation.of HahnSeries.orderTop ⋯ ⋯ ⋯ ⋯

theorem HahnSeries.addVal_apply {Γ : Type u_1} {R : Type u_2} [AddCancelCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} : (addVal Γ R) x = x.orderTop

@[simp]

theorem HahnSeries.addVal_apply_of_ne {Γ : Type u_1} {R : Type u_2} [AddCancelCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (hx : x ≠ 0) : (addVal Γ R) x = ↑x.order

theorem HahnSeries.addVal_le_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [AddCancelCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) : (addVal Γ R) x ≤ ↑g