Support order type and degree of a Hahn series

LM24 orders the support of a generalized power series by increasing exponent. Accordingly, HahnSeries.supportOrderType is the ordinal type of the strict order < on the support; no order reversal occurs in this module. For a linearly ordered exponent type, Mathlib's IsPWO support condition is equivalent to the well-foundedness needed for this ordinal type.

If the exponent type belongs to Type u, the order type and degree belong to Ordinal.{u} and WithBot NatOrdinal.{u}, independently of the universe of the coefficients. The degree uses LM24's convention: a nonzero series has the leading Cantor exponent of its support order type, whereas the zero series has degree ⊥.

These definitions formalize LM24, Sections 1.2, 1.5, 2.2, and 3.1. Multiplicativity is a later theorem and is not built into the definitions.

The support-decomposition theorems use the strict lower-to-upper relation HahnSeries.SupportBelow and the generic support lemmas in ConwayRefinement.HahnSeries.SeparatedSupport.

def HahnSeries.supportOrderType {R : Type v} {G : Type u} [LinearOrder G] [Zero R] (x : HahnSeries G R) : Ordinal.{u}

The ordinary ordinal order type of a Hahn series support, ordered by increasing exponent.

Equations

• x.supportOrderType = ⋯.orderType

theorem HahnSeries.supportOrderType_eq_setOrderType {R : Type v} {G : Type u} [LinearOrder G] [Zero R] (x : HahnSeries G R) : x.supportOrderType = ⋯.orderType

Support order type is the generic order type of the partially well-ordered support.

theorem HahnSeries.supportOrderType_eq_typeLT {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} {A : Type u} [LinearOrder A] [WellFoundedLT A] (e : ↑x.support ≃o A) : x.supportOrderType = Ordinal.type fun (x1 x2 : A) => x1 < x2

Compute supportOrderType from an order isomorphism out of the support.

theorem HahnSeries.supportOrderType_eq_type_of_relIso {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} {A : Type u} {r : A → A → Prop} [IsWellOrder A r] (e : (Subrel (fun (x1 x2 : G) => x1 < x2) fun (x_1 : G) => x_1 ∈ x.support) ≃r r) : x.supportOrderType = Ordinal.type r

Compute supportOrderType from a relation isomorphism to an arbitrary well-order.

@[simp]

theorem HahnSeries.supportOrderType_eq_zero {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : x.supportOrderType = 0 ↔ x = 0

@[simp]

theorem HahnSeries.supportOrderType_zero {R : Type v} {G : Type u} [LinearOrder G] [Zero R] : supportOrderType 0 = 0

theorem HahnSeries.supportOrderType_single {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {a : G} {r : R} (hr : r ≠ 0) : ((single a) r).supportOrderType = 1

A nonzero single-term Hahn series has ordinary support order type one.

theorem HahnSeries.supportOrderType_mono {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x y : HahnSeries G R} (h : x.support ⊆ y.support) : x.supportOrderType ≤ y.supportOrderType

Inclusion of supports cannot decrease their ordinary ordinal order type.

theorem HahnSeries.support_finite_iff_supportOrderType_lt_omega {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : x.support.Finite ↔ x.supportOrderType < Ordinal.omega0

A Hahn series has finite support exactly when its support order type is below ω.

noncomputable def HahnSeries.degree {R : Type v} {G : Type u} [LinearOrder G] [Zero R] (x : HahnSeries G R) : WithBot NatOrdinal

The leading Cantor exponent of the support order type, with value ⊥ at zero.

Equations

• x.degree = x.supportOrderType.cantorDegree

theorem HahnSeries.degree_eq_cantorDegree {R : Type v} {G : Type u} [LinearOrder G] [Zero R] (x : HahnSeries G R) : x.degree = x.supportOrderType.cantorDegree

Degree is the leading Cantor exponent of the support order type.

@[simp]

theorem HahnSeries.degree_eq_bot {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : x.degree = ⊥ ↔ x = 0

@[simp]

theorem HahnSeries.degree_zero {R : Type v} {G : Type u} [LinearOrder G] [Zero R] : degree 0 = ⊥

@[simp]

theorem HahnSeries.degree_eq_zero {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : x.degree = 0 ↔ x ≠ 0 ∧ x.support.Finite

Degree zero is equivalent to nonzero finite support.

theorem HahnSeries.zero_le_degree_of_ne_zero {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} (hx : x ≠ 0) : 0 ≤ x.degree

The degree of a nonzero Hahn series is nonnegative.

@[simp]

theorem HahnSeries.degree_le_zero_iff {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : x.degree ≤ 0 ↔ x.support.Finite

Degree is at most zero exactly for finite-support Hahn series, including the zero series.

theorem HahnSeries.degree_pos_iff_support_infinite {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : 0 < x.degree ↔ x.support.Infinite

A Hahn series has positive degree exactly when its support is infinite.

@[simp]

theorem HahnSeries.degree_lt_zero_iff {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} : x.degree < 0 ↔ x = 0

Degree is strictly below zero exactly at the zero Hahn series.

theorem HahnSeries.coe_le_degree_iff {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x : HahnSeries G R} {a : Ordinal.{u}} (hx : x ≠ 0) : ↑(NatOrdinal.of a) ≤ x.degree ↔ Ordinal.omega0 ^ a ≤ x.supportOrderType

This is LM24's maximum characterization of the degree of a nonzero Hahn series.

theorem HahnSeries.degree_lt_coe_iff_supportOrderType_lt_wpow {R : Type v} {G : Type u} [LinearOrder G] [Zero R] (x : HahnSeries G R) (α : NatOrdinal) : x.degree < ↑α ↔ x.supportOrderType < NatOrdinal.val (ω^ α)

A degree lies strictly below α exactly when the support order type lies strictly below ω^α.

theorem HahnSeries.degree_mono_support {R : Type v} {G : Type u} [LinearOrder G] [Zero R] {x y : HahnSeries G R} (h : x.support ⊆ y.support) : x.degree ≤ y.degree

Inclusion of supports cannot decrease degree.

theorem HahnSeries.degree_truncLE_le {R : Type v} {G : Type u} [LinearOrder G] [Zero R] (c : G) (x : HahnSeries G R) : ((truncLE c) x).degree ≤ x.degree

Weak lower truncation cannot increase degree. This strengthens the final consequence following LM24, Definition 3.2.2 by removing its unnecessary properness hypothesis.

theorem HahnSeries.supportOrderType_eq_add_iff {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] (x : HahnSeries G R) (a b : Ordinal.{u}) : x.supportOrderType = a + b ↔ ∃ (y : HahnSeries G R) (z : HahnSeries G R), y.SupportBelow z ∧ y.supportOrderType = a ∧ z.supportOrderType = b ∧ x = y + z

A Hahn series has support order type a + b exactly when it is a sum whose first support lies strictly below its second support and whose summands have support order types a and b. This is LM24, Proposition 3.2.1, generalized from field coefficients and a fixed cardinal support bound to additive-monoid coefficients and unrestricted Hahn series. The constructed summands have supports contained in the original support, so the result restricts to the source's support regime.

theorem HahnSeries.add_decomposition_unique {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] {x₀ x₁ y₀ y₁ : HahnSeries G R} (hx : x₀.SupportBelow x₁) (hy : y₀.SupportBelow y₁) (htype : x₀.supportOrderType = y₀.supportOrderType) (hsum : x₀ + x₁ = y₀ + y₁) : x₀ = y₀ ∧ x₁ = y₁

A decomposition from supportOrderType_eq_add_iff is uniquely determined by the order type of its lower summand. This is the uniqueness used when LM24 iterates Proposition 3.2.1.

theorem HahnSeries.supportOrderType_list_sum {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] {l : List (HahnSeries G R)} (hpair : List.Pairwise SupportBelow l) : l.sum.supportOrderType = (List.map supportOrderType l).sum

The support order type of a pairwise support-separated finite sum is the ordinary ordinal sum of the support order types, in list order.

theorem HahnSeries.supportOrderType_eq_truncLT_add_truncGE {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] (c : G) (x : HahnSeries G R) : x.supportOrderType = ((truncLT c) x).supportOrderType + ((truncGE c) x).supportOrderType

The support order type splits at a strict lower and weak upper truncation. This is the first order-type equality following LM24, Definition 3.2.2.

theorem HahnSeries.supportOrderType_eq_truncLE_add_truncGT {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] (c : G) (x : HahnSeries G R) : x.supportOrderType = ((truncLE c) x).supportOrderType + ((truncGT c) x).supportOrderType

The support order type splits at a weak lower and strict upper truncation. This is the second order-type equality following LM24, Definition 3.2.2.

theorem HahnSeries.supportOrderType_truncLE_lt {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] (c : G) {x : HahnSeries G R} (h : (truncLE c) x ≠ x) : ((truncLE c) x).supportOrderType < x.supportOrderType

A proper weak lower truncation has strictly smaller support order type. This is the strict inequality following LM24, Definition 3.2.2.

theorem HahnSeries.supportOrderType_add_le_naturalAdd {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] (x y : HahnSeries G R) : (x + y).supportOrderType ≤ NatOrdinal.val (NatOrdinal.of x.supportOrderType + NatOrdinal.of y.supportOrderType)

The order type of the support of a sum is at most the Hessenberg sum of the two support order types. This is LM24, Proposition 3.1.1(1), generalized from a field of coefficients.

theorem HahnSeries.degree_add_le {R : Type v} {G : Type u} [LinearOrder G] [AddMonoid R] (x y : HahnSeries G R) : (x + y).degree ≤ max x.degree y.degree

The degree of a sum is at most the maximum of the two degrees. This is LM24, Corollary 3.1.2(1), generalized from a field of coefficients.

@[simp]

theorem HahnSeries.supportOrderType_neg {R : Type v} {G : Type u} [LinearOrder G] [AddGroup R] (x : HahnSeries G R) : (-x).supportOrderType = x.supportOrderType

Negation preserves ordinary support order type.

@[simp]

theorem HahnSeries.degree_neg {R : Type v} {G : Type u} [LinearOrder G] [AddGroup R] (x : HahnSeries G R) : (-x).degree = x.degree

Negation preserves degree.

theorem HahnSeries.degree_add_eq_left_of_lt {R : Type v} {G : Type u} [LinearOrder G] [AddGroup R] {x y : HahnSeries G R} (h : y.degree < x.degree) : (x + y).degree = x.degree

Adding a series of strictly smaller degree does not change the larger degree.

theorem HahnSeries.supportOrderType_mul_le_naturalMul {R : Type v} {G : Type u} [LinearOrder G] [AddCommMonoid G] [IsOrderedCancelAddMonoid G] [NonUnitalNonAssocSemiring R] (x y : HahnSeries G R) : (x * y).supportOrderType ≤ NatOrdinal.val (NatOrdinal.of x.supportOrderType * NatOrdinal.of y.supportOrderType)

The order type of the support of a product is at most the Hessenberg product of the two support order types. This is LM24, Proposition 3.1.1(2), generalized from an ordered abelian exponent group and a field of coefficients.

theorem HahnSeries.degree_mul_le {R : Type v} {G : Type u} [LinearOrder G] [AddCommMonoid G] [IsOrderedCancelAddMonoid G] [NonUnitalNonAssocSemiring R] (x y : HahnSeries G R) : (x * y).degree ≤ x.degree + y.degree

The degree of a product is at most the Hessenberg sum of the two degrees. This is LM24, Corollary 3.1.2(2), generalized from an ordered abelian exponent group and a field of coefficients.

theorem HahnSeries.supportOrderType_lt_omega_one {R : Type v} {G : Type u} [LinearOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] [Archimedean G] [Zero R] (x : HahnSeries G R) : x.supportOrderType < Ordinal.omega 1

Over an Archimedean exponent group every support is countable, so every support order type is below ω₁.

theorem HahnSeries.degree_lt_omega_one {R : Type v} {G : Type u} [LinearOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] [Archimedean G] [Zero R] (x : HahnSeries G R) : x.degree < ↑(NatOrdinal.of (Ordinal.omega 1))

Over an Archimedean exponent group every degree is a countable ordinal.