The spaces P_α

For an exponent α, this module defines the space P_α intrinsically as

J_{ω^(α+1)} / J_{ω^α}.

Here J_{ω^α} is the additive subgroup of series whose ordinal value is strictly below ω^α. In Lean, the quotient is the grade-α component of the multiplicative degree ordinalValueDegreeValuation K, the leading Cantor exponent of v_J. Thus the quotient structure and representative independence are inherited from the generic associated-graded construction; no basis, complement, or chosen family of representatives occurs in the definition.

The representative API proves that equality is congruence modulo J_{ω^α}. It also proves the characterization from LM24, Remark 7.2.4: every nonzero class has a principal Hahn series representative of exact degree α. This characterization is a theorem about the intrinsic quotient, not its primitive definition.

Constants act through the degree-zero residue ring, giving every homogeneous component its canonical K-module structure. Everything here holds over an arbitrary coefficient field: the components and their multiplication use only the max-additive degree structure of ordinalValueDegreeValuation, that is, Berarducci, Lemma 5.5, and never the multiplicativity of the ordinal value.

@[reducible, inline]

noncomputable abbrev Berarducci.ordinalValueCut (K : Type v) [Field K] (α : NatOrdinal) : AddSubgroup (Series K)

The source space J_{ω^α} of series whose ordinal value is below ω^α.

Equations

• Berarducci.ordinalValueCut K α = (Berarducci.ordinalValueDegreeValuation K).filtrationLT α

theorem Berarducci.mem_ordinalValueCut_iff {K : Type v} [Field K] (α : NatOrdinal) (b : Series K) : b ∈ ordinalValueCut K α ↔ ordinalValue b < ω^ α

theorem Berarducci.ordinalValueCut_add_one_eq_filtrationLE (K : Type v) [Field K] (α : NatOrdinal) : ordinalValueCut K (α + 1) = (ordinalValueDegreeValuation K).filtrationLE α

The source space J_{ω^(α+1)} is the weak degree filtration at α.

@[reducible, inline]

abbrev Berarducci.PrincipalComponent (K : Type v) [Field K] (α : NatOrdinal) : Type v

The space P_α = J_{ω^(α+1)} / J_{ω^α}.

Equations

• Berarducci.PrincipalComponent K α = (Berarducci.ordinalValueDegreeValuation K).Component α

noncomputable def Berarducci.principalComponentMk {K : Type v} [Field K] (α : NatOrdinal) (b : Series K) (hb : ordinalValue b < ω^ (α + 1)) : PrincipalComponent K α

The class in P_α of a series in J_{ω^(α+1)}.

Equations

• Berarducci.principalComponentMk α b hb = ((Berarducci.ordinalValueDegreeValuation K).componentMk α) ⟨b, ⋯⟩

theorem Berarducci.principalComponentMk_eq_componentMk {K : Type v} [Field K] (α : NatOrdinal) (b : Series K) (hb : ordinalValue b < ω^ (α + 1)) : principalComponentMk α b hb = ((ordinalValueDegreeValuation K).componentMk α) ⟨b, ⋯⟩

principalComponentMk is the associated-graded quotient map on the ordinal-value filtration.

@[simp]

theorem Berarducci.principalComponentMk_eq_zero_iff {K : Type v} [Field K] (α : NatOrdinal) (b : Series K) (hb : ordinalValue b < ω^ (α + 1)) : principalComponentMk α b hb = 0 ↔ ordinalValue b < ω^ α

theorem Berarducci.principalComponentMk_eq_iff {K : Type v} [Field K] (α : NatOrdinal) (b c : Series K) (hb : ordinalValue b < ω^ (α + 1)) (hc : ordinalValue c < ω^ (α + 1)) : principalComponentMk α b hb = principalComponentMk α c hc ↔ ordinalValue (b - c) < ω^ α

Equality in P_α is congruence modulo the strict cut J_{ω^α}.

theorem Berarducci.exists_principalComponentMk {K : Type v} [Field K] (α : NatOrdinal) (x : PrincipalComponent K α) : ∃ (b : Series K) (hb : ordinalValue b < ω^ (α + 1)), principalComponentMk α b hb = x

Every class in P_α has a representative in its weak ordinal-value cut.

theorem Berarducci.exists_principal_representative_of_ne_zero {K : Type v} [Field K] (α : NatOrdinal) (x : PrincipalComponent K α) (hx : x ≠ 0) : ∃ (p : Series K) (hpBound : ordinalValue p < ω^ (α + 1)), HahnSeries.Nonpositive.IsPrincipal p ∧ (↑p).degree = ↑α ∧ principalComponentMk α p hpBound = x

Every nonzero class in P_α has a principal representative of exact series degree α. This is the representative characterization in LM24, Remark 7.2.4.

noncomputable def Berarducci.principalComponentMul {K : Type v} [Field K] {α β : NatOrdinal} : PrincipalComponent K α → PrincipalComponent K β → PrincipalComponent K (α + β)

Multiplication P_α × P_β → P_{α + β}, where addition is the Hessenberg sum.

Equations

• Berarducci.principalComponentMul = (Berarducci.ordinalValueDegreeValuation K).componentMul

theorem Berarducci.principalComponentMul_eq_componentMul {K : Type v} [Field K] {α β : NatOrdinal} (x : PrincipalComponent K α) (y : PrincipalComponent K β) : principalComponentMul x y = (ordinalValueDegreeValuation K).componentMul x y

Intrinsic homogeneous multiplication is the associated-graded component multiplication.

theorem Berarducci.ordinalValue_mul_lt_wpow_add_one {K : Type v} [Field K] {α β : NatOrdinal} {b c : Series K} (hb : ordinalValue b < ω^ (α + 1)) (hc : ordinalValue c < ω^ (β + 1)) : ordinalValue (b * c) < ω^ (α + β + 1)

Products of representatives from the weak cuts at α and β lie in the weak cut at α + β.

@[simp]

theorem Berarducci.principalComponentMul_mk {K : Type v} [Field K] {α β : NatOrdinal} (b c : Series K) (hb : ordinalValue b < ω^ (α + 1)) (hc : ordinalValue c < ω^ (β + 1)) : principalComponentMul (principalComponentMk α b hb) (principalComponentMk β c hc) = principalComponentMk (α + β) (b * c) ⋯

Homogeneous multiplication is induced by multiplication of representatives.

theorem Berarducci.ordinalValue_C_lt_wpow_one {K : Type v} [Field K] (k : K) : ordinalValue (HahnSeries.Nonpositive.C k) < ω^ (0 + 1)

A constant has ordinal value below the first positive principal cut.

noncomputable def Berarducci.principalComponentScalarHom (K : Type v) [Field K] : K →+* (ordinalValueDegreeValuation K).ResidueRing

The scalar map from constants to the grade-zero residue ring of the exponent-valued order value.

Equations

• Berarducci.principalComponentScalarHom K = (Berarducci.ordinalValueDegreeValuation K).residueMap.comp (Berarducci.constantToOrdinalValueNonpositiveSubring✝ K)

theorem Berarducci.principalComponentScalarHom_apply {K : Type v} [Field K] (k : K) : (principalComponentScalarHom K) k = principalComponentMk 0 (HahnSeries.Nonpositive.C k) ⋯

The scalar map K → P_0 sends a coefficient to the class of the corresponding constant series.

theorem Berarducci.principalComponentScalarHom_injective (K : Type v) [Field K] : Function.Injective ⇑(principalComponentScalarHom K)

Distinct coefficients determine distinct classes in P_0.

theorem Berarducci.principalComponentScalarHom_surjective (K : Type v) [Field K] : Function.Surjective ⇑(principalComponentScalarHom K)

Every grade-zero principal class is represented by a unique coefficient.

instance Berarducci.principalComponentZeroNontrivial {K : Type v} [Field K] : Nontrivial (PrincipalComponent K 0)

The space P_0 is nontrivial because it contains the coefficient field.

@[instance_reducible]

noncomputable instance Berarducci.principalComponentModule {K : Type v} [Field K] (α : NatOrdinal) : Module K (PrincipalComponent K α)

Every P_α is canonically a vector space over K.

Equations

• Berarducci.principalComponentModule α = Module.compHom (Berarducci.PrincipalComponent K α) (Berarducci.principalComponentScalarHom K)

theorem Berarducci.smul_principalComponentMk {K : Type v} [Field K] (α : NatOrdinal) (k : K) (b : Series K) (hb : ordinalValue b < ω^ (α + 1)) : k • principalComponentMk α b hb = principalComponentMk α (HahnSeries.Nonpositive.C k * b) ⋯

Scalar multiplication on P_α is multiplication of a representative by the corresponding constant series.