The polar part of a Hahn series

For a linearly ordered cancellative monoid Γ, the truncation HahnSeries.truncLT 0 keeps the coefficients of a Hahn series at the negative exponents. On Laurent series it is the projection onto the polar part, and it is a Rota–Baxter operator of weight -1: since exponents add under multiplication, the series supported on the negative exponents form a subring, and so do the series supported on the nonnegative ones.

Main results

• HahnSeries.isRotaBaxter_truncLT: truncLT 0 is a Rota–Baxter operator of weight -1.
• HahnSeries.truncLT_truncLT, HahnSeries.truncLT_single: truncation is idempotent, and it keeps or kills a monomial.
• HahnSeries.truncLT_neg, HahnSeries.truncLT_sub: truncation commutes with negation and subtraction.

The four truncation lemmas are [UPSTREAM] candidates for Mathlib/RingTheory/HahnSeries/Basic.lean and Mathlib/RingTheory/HahnSeries/Addition.lean, beside truncLT_add.

References

• [CK00]
• [EFGK04]

@[simp]

theorem HahnSeries.truncLT_truncLT {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [DecidableLT Γ] [Zero R] (c : Γ) (x : HahnSeries Γ R) : (truncLT c) ((truncLT c) x) = (truncLT c) x

theorem HahnSeries.truncLT_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [DecidableLT Γ] [Zero R] (c d : Γ) (r : R) : (truncLT c) ((single d) r) = if d < c then (single d) r else 0

theorem HahnSeries.truncLT_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [DecidableLT Γ] [AddGroup R] (c : Γ) (x : HahnSeries Γ R) : (truncLT c) (-x) = -(truncLT c) x

theorem HahnSeries.truncLT_sub {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [DecidableLT Γ] [AddGroup R] (c : Γ) (x y : HahnSeries Γ R) : (truncLT c) (x - y) = (truncLT c) x - (truncLT c) y

theorem HahnSeries.truncLT_single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] {c d : Γ} {r : R} (hr : r ≠ 0) : (truncLT c) ((single d) r) = 0 ↔ c ≤ d

theorem HahnSeries.isRotaBaxter_truncLT {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] (k : Type u_3) [Ring k] [Module k (HahnSeries Γ R)] : IsRotaBaxter (-1) ⇑(truncLT 0)

The projection onto the polar part is a Rota–Baxter operator of weight -1, from the ring identity R a * b + a * R b - a * b = R a * R b - (a - R a) * (b - R b): R fixes the first term, a product of polar parts, and kills the second, a product of nonpolar parts.