Documentation

Mathlib.RingTheory.HahnSeries.Basic

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 and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered.
Laurent series over R are implemented as HahnSeries ℤ R in the file RingTheory/LaurentSeries.

References #

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

theorem HahnSeries.ext_iff {Γ : Type u_1} {R : Type u_2} :

∀ {inst : PartialOrder Γ} {inst_1 : Zero R} (x y : HahnSeries Γ R), x = y ↔ x.coeff = y.coeff

theorem HahnSeries.ext {Γ : Type u_1} {R : Type u_2} :

∀ {inst : PartialOrder Γ} {inst_1 : Zero R} (x y : HahnSeries Γ R), x.coeff = y.coeff → x = y

structure HahnSeries (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [Zero R] :

Type (max u_1 u_2)

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
isPWO_support' : Set.IsPWO (Function.support self.coeff)

Instances For

theorem HahnSeries.coeff_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] :

Function.Injective HahnSeries.coeff

@[simp]

theorem HahnSeries.coeff_inj {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} :

x.coeff = y.coeff ↔ x = y

def HahnSeries.support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

Set Γ

The support of a Hahn series is just the set of indices whose coefficients are nonzero. Notably, it is well-founded.

Equations

HahnSeries.support x = Function.support x.coeff

Instances For

@[simp]

theorem HahnSeries.isPWO_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

Set.IsPWO (HahnSeries.support x)

@[simp]

theorem HahnSeries.isWF_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

Set.IsWF (HahnSeries.support x)

@[simp]

theorem HahnSeries.mem_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) (a : Γ) :

a ∈ HahnSeries.support x ↔ x.coeff a ≠ 0

instance HahnSeries.instZeroHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] :

Zero (HahnSeries Γ R)

Equations

HahnSeries.instZeroHahnSeries = { zero := { coeff := 0, isPWO_support' := ⋯ } }

instance HahnSeries.instInhabitedHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] :

Inhabited (HahnSeries Γ R)

Equations

HahnSeries.instInhabitedHahnSeries = { default := 0 }

instance HahnSeries.instSubsingletonHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Subsingleton R] :

Subsingleton (HahnSeries Γ R)

Equations

⋯ = ⋯

@[simp]

theorem HahnSeries.zero_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} :

0.coeff a = 0

@[simp]

theorem HahnSeries.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.coeff = 0 ↔ x = 0

theorem HahnSeries.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) :

x ≠ 0

@[simp]

theorem HahnSeries.support_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] :

HahnSeries.support 0 = ∅

@[simp]

theorem HahnSeries.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

Set.Nonempty (HahnSeries.support x) ↔ x ≠ 0

@[simp]

theorem HahnSeries.support_eq_empty_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

HahnSeries.support x = ∅ ↔ x = 0

/-- Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product. -/ def of_iterate {Γ' : Type*} [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) : HahnSeries (Γ ×ₗ Γ') R where coeff := fun g => coeff (coeff x g.1) g.2 isPWO_support' := by intro f hf simp_all only have hf' : ∀ n, (f n).1 ∈ Function.support fun g ↦ x.coeff g := by intro n hn simp_all only [Function.mem_support, ne_eq] specialize hf n rw [hn] at hf exact hf rfl sorry -- See Mathlib.Data.MvPolynomial.Monad for join and bind operations need a monotone pair. have: nonrec theorem IsPWO.exists_monotone_subseq (h : s.IsPWO) (f : ℕ → α) (hf : ∀ n, f n ∈ s) : ∃ g : ℕ ↪o ℕ, Monotone (f ∘ g) := h.exists_monotone_subseq f hf #align set.is_pwo.exists_monotone_subseq Set.IsPWO.exists_monotone_subseq map sequence to Γ, get monotone subsequence (use ext property) if stationary at a ∈ Γ, look inside {a} × Γ', get monotone subsequence. if not stationary, use lex order. /-- Change a Hahn series on a lex product to a Hahn series with coefficients in a Hahn series. -/ def to_iterate {Γ' : Type*} [PartialOrder Γ'] (x : HahnSeries (Γ ×ₗ Γ') R) : HahnSeries Γ (HahnSeries Γ' R) where coeff := fun g => { coeff := fun g' => coeff x (g, g') isPWO_support' := sorry } isPWO_support' := sorry

Equivalence between HahnSeries Γ (HahnSeries Γ' R) and HahnSeries (Γ × Γ') R
Use Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber to iterate. (need PWO version)

def HahnSeries.single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) :

ZeroHom R (HahnSeries Γ R)

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

@[simp]

theorem HahnSeries.single_coeff_same {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) (r : R) :

((HahnSeries.single a) r).coeff a = r

@[simp]

theorem HahnSeries.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} (h : b ≠ a) :

((HahnSeries.single a) r).coeff b = 0

theorem HahnSeries.single_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} :

((HahnSeries.single a) r).coeff b = if b = a then r else 0

@[simp]

theorem HahnSeries.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) :

HahnSeries.support ((HahnSeries.single a) r) = {a}

theorem HahnSeries.support_single_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :

HahnSeries.support ((HahnSeries.single a) r) ⊆ {a}

theorem HahnSeries.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} {b : Γ} (h : b ∈ HahnSeries.support ((HahnSeries.single a) r)) :

b = a

theorem HahnSeries.single_eq_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} :

(HahnSeries.single a) 0 = 0

theorem HahnSeries.single_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) :

Function.Injective ⇑(HahnSeries.single a)

theorem HahnSeries.single_ne_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) :

(HahnSeries.single a) r ≠ 0

@[simp]

theorem HahnSeries.single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :

(HahnSeries.single a) r = 0 ↔ r = 0

instance HahnSeries.instNontrivialHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Nonempty Γ] [Nontrivial R] :

Nontrivial (HahnSeries Γ R)

Equations

⋯ = ⋯

def HahnSeries.order {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] (x : HahnSeries Γ R) :

Γ

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.

Equations

HahnSeries.order x = if h : x = 0 then 0 else Set.IsWF.min ⋯ ⋯

Instances For

@[simp]

theorem HahnSeries.order_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] :

HahnSeries.order 0 = 0

theorem HahnSeries.order_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) :

HahnSeries.order x = Set.IsWF.min ⋯ ⋯

theorem HahnSeries.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.coeff (HahnSeries.order x) ≠ 0

theorem HahnSeries.order_le_of_coeff_ne_zero {R : Type u_2} [Zero R] {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) :

HahnSeries.order x ≤ g

@[simp]

theorem HahnSeries.order_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} [Zero Γ] (h : r ≠ 0) :

HahnSeries.order ((HahnSeries.single a) r) = a

theorem HahnSeries.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} {i : Γ} (hi : i < HahnSeries.order x) :

x.coeff i = 0

def HahnSeries.embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] (f : Γ ↪o Γ') :

HahnSeries Γ R → HahnSeries Γ' R

Extends the domain of a HahnSeries by an OrderEmbedding.

Equations

HahnSeries.embDomain f x = { coeff := fun (b : Γ') => if h : b ∈ ⇑f '' HahnSeries.support x then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.embDomain_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ} :

(HahnSeries.embDomain f x).coeff (f a) = x.coeff a

@[simp]

theorem HahnSeries.embDomain_mk_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ → Γ'} (hfi : Function.Injective f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') {x : HahnSeries Γ R} {a : Γ} :

(HahnSeries.embDomain { toEmbedding := { toFun := f, inj' := hfi }, map_rel_iff' := ⋯ } x).coeff (f a) = x.coeff a

theorem HahnSeries.embDomain_notin_image_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ ⇑f '' HahnSeries.support x) :

(HahnSeries.embDomain f x).coeff b = 0

theorem HahnSeries.support_embDomain_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :

HahnSeries.support (HahnSeries.embDomain f x) ⊆ ⇑f '' HahnSeries.support x

theorem HahnSeries.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ Set.range ⇑f) :

(HahnSeries.embDomain f x).coeff b = 0

@[simp]

theorem HahnSeries.embDomain_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} :

HahnSeries.embDomain f 0 = 0

@[simp]

theorem HahnSeries.embDomain_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {g : Γ} {r : R} :

HahnSeries.embDomain f ((HahnSeries.single g) r) = (HahnSeries.single (f g)) r

theorem HahnSeries.embDomain_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} :

Function.Injective (HahnSeries.embDomain f)

theorem HahnSeries.suppBddBelow_supp_PWO {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R) (hf : BddBelow (Function.support f)) :

Set.IsPWO (Function.support f)

theorem HahnSeries.forallLTEqZero_supp_BddBelow {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] (f : Γ → R) (n : Γ) (hn : ∀ m < n, f m = 0) :

BddBelow (Function.support f)

@[simp]

theorem HahnSeries.ofSuppBddBelow_coeff {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R) (hf : BddBelow (Function.support f)) :

∀ (a : Γ), (HahnSeries.ofSuppBddBelow f hf).coeff a = f a

def HahnSeries.ofSuppBddBelow {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R) (hf : BddBelow (Function.support f)) :

HahnSeries Γ R

Construct a Hahn series from any function whose support is bounded below.

Equations

HahnSeries.ofSuppBddBelow f hf = { coeff := f, isPWO_support' := ⋯ }

Instances For

theorem HahnSeries.BddBelow_zero {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] [Nonempty Γ] :

BddBelow (Function.support 0)

@[simp]

theorem HahnSeries.zero_ofSuppBddBelow {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] [Nonempty Γ] :

HahnSeries.ofSuppBddBelow 0 ⋯ = 0

theorem HahnSeries.order_ofForallLtEqZero {Γ : Type u_1} {R : Type u_2} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ) (hn : ∀ m < n, f m = 0) :

n ≤ HahnSeries.order (HahnSeries.ofSuppBddBelow f ⋯)