Reduction at an Archimedean class

LM24, Definition 8.2.4 divides the closed-class truncation T_σ(x) by the open-class truncation τ_σ(x) when the latter is nonzero. This module establishes the structural facts needed for that division. Under the iterated Hahn-series presentation ι_σ, τ_σ(x) is a coefficient-series scalar, while T_σ(x) has only nonpositive outer exponents.

The scalar statement is essential: the inverse of a negative monomial has positive exponent, so the quotient cannot be justified by claiming that the full nonpositive Hahn-series ring is closed under inversion.

def HahnSeries.Nonpositive.closedBallOrderEmbedding {K : Type u_1} {G : Type u_2} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] (c : FiniteArchimedeanClass G) : ↥(FiniteArchimedeanClass.closedBall K c) ↪o G

The ordered inclusion of a closed Archimedean ball into the ambient exponent group.

Equations

• HahnSeries.Nonpositive.closedBallOrderEmbedding c = { toFun := Subtype.val, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem HahnSeries.Nonpositive.closedBallOrderEmbedding_apply {K : Type u_1} {G : Type u_2} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] (c : FiniteArchimedeanClass G) (g : ↥(FiniteArchimedeanClass.closedBall K c)) : (closedBallOrderEmbedding c) g = ↑g

def HahnSeries.Nonpositive.ballOrderEmbedding {K : Type u_1} {G : Type u_2} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] (c : FiniteArchimedeanClass G) : ↥(FiniteArchimedeanClass.ball K c) ↪o G

The ordered inclusion of an open Archimedean ball into the ambient exponent group.

Equations

• HahnSeries.Nonpositive.ballOrderEmbedding c = { toFun := Subtype.val, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem HahnSeries.Nonpositive.ballOrderEmbedding_apply {K : Type u_1} {G : Type u_2} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] (c : FiniteArchimedeanClass G) (g : ↥(FiniteArchimedeanClass.ball K c)) : (ballOrderEmbedding c) g = ↑g

noncomputable def HahnSeries.Nonpositive.TClosed {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : HahnSeries (↥(FiniteArchimedeanClass.closedBall K c)) R

The closed-class truncation, with its exponent domain restricted to the closed ball.

Equations

• HahnSeries.Nonpositive.TClosed c x = HahnSeries.restrictDomain (HahnSeries.Nonpositive.closedBallOrderEmbedding c) ↑((HahnSeries.Nonpositive.T c) x)

theorem HahnSeries.Nonpositive.TClosed_eq {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : TClosed c x = restrictDomain (closedBallOrderEmbedding c) ↑((T c) x)

The closed-class truncation is exponent-domain restriction of the ambient truncation.

@[simp]

theorem HahnSeries.Nonpositive.TClosed_coeff {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (g : ↥(FiniteArchimedeanClass.closedBall K c)) : (TClosed c x).coeff g = (↑((T c) x)).coeff ↑g

noncomputable def HahnSeries.Nonpositive.tauBall {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : HahnSeries (↥(FiniteArchimedeanClass.ball K c)) R

The open-class truncation, with its exponent domain restricted to the open ball.

Equations

• HahnSeries.Nonpositive.tauBall c x = HahnSeries.restrictDomain (HahnSeries.Nonpositive.ballOrderEmbedding c) ↑((HahnSeries.Nonpositive.tau c) x)

@[simp]

theorem HahnSeries.Nonpositive.tauBall_coeff {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (g : ↥(FiniteArchimedeanClass.ball K c)) : (tauBall c x).coeff g = (↑((tau c) x)).coeff ↑g

noncomputable def HahnSeries.Nonpositive.tauClosed {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : HahnSeries (↥(FiniteArchimedeanClass.closedBall K c)) R

The open-class truncation, regarded as a series on the containing closed ball.

Equations

• HahnSeries.Nonpositive.tauClosed c x = HahnSeries.restrictDomain (HahnSeries.Nonpositive.closedBallOrderEmbedding c) ↑((HahnSeries.Nonpositive.tau c) x)

theorem HahnSeries.Nonpositive.archimedeanSplitRingEquiv_tauClosed {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : (archimedeanSplitRingEquiv u c) (tauClosed c x) = HahnSeries.C (tauBall c x)

Under the Archimedean splitting, the open-class truncation is a scalar coefficient series.

theorem HahnSeries.Nonpositive.coeff_zero_archimedeanSplitRingEquiv_TClosed {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : ((archimedeanSplitRingEquiv u c) (TClosed c x)).coeff 0 = tauBall c x

The outer constant coefficient of the split closed-class truncation is the open-class truncation. This is LM24's identity π(ισ(Tσ(x))) = τσ(x).

theorem HahnSeries.Nonpositive.support_archimedeanSplitRingEquiv_TClosed_subset {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : ((archimedeanSplitRingEquiv u c) (TClosed c x)).support ⊆ Set.Iic 0

The split closed-class truncation has no positive outer exponent.

theorem HahnSeries.Nonpositive.support_archimedeanSplitRingEquiv_TClosed_div_C_subset {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : ((archimedeanSplitRingEquiv u c) (TClosed c x) / HahnSeries.C (tauBall c x)).support ⊆ Set.Iic 0

Dividing the split closed-class truncation by the open-class scalar does not introduce positive outer exponents.

theorem HahnSeries.Nonpositive.coeff_zero_archimedeanSplitRingEquiv_TClosed_div_C {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : tauBall c x ≠ 0) : ((archimedeanSplitRingEquiv u c) (TClosed c x) / HahnSeries.C (tauBall c x)).coeff 0 = 1

In the nonzero branch of LM24's reduction, the outer-zero coefficient of the quotient is one. This rules out positive infinitesimal exponents at the only outer boundary where the outer support condition alone would be insufficient.

theorem HahnSeries.Nonpositive.support_archimedeanSplitRingEquiv_symm_subset_Iic {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (y : HahnSeries (↥(u.stratum c)) (HahnSeries (↥(FiniteArchimedeanClass.ball K c)) R)) (hyOuter : y.support ⊆ Set.Iic 0) (hyZero : (y.coeff 0).support ⊆ Set.Iic 0) : ((archimedeanSplitRingEquiv u c).symm y).support ⊆ Set.Iic 0

If an iterated Hahn series has no positive outer exponents and its coefficient at outer exponent zero has no positive inner exponents, then its image back on the closed Archimedean ball has no positive exponents.

noncomputable def HahnSeries.Nonpositive.reductionQuotient {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : tauBall c x ≠ 0) : Nonpositive G R

The nonzero quotient branch in LM24, Definition 8.2.4, as a nonpositive Hahn series.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.Nonpositive.coeff_zero_reductionQuotient {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : tauBall c x ≠ 0) : (↑(reductionQuotient u c x htau)).coeff 0 = 1

In the nonzero branch of LM24's reduction, the coefficient at the exponent zero is one: the outer-zero coefficient of the split quotient is the constant one.

noncomputable def HahnSeries.Nonpositive.rho {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : Nonpositive G R

LM24's ρ_σ: divide the closed-class truncation by the open-class truncation when the latter is nonzero, and otherwise retain the closed-class truncation.

Equations

• HahnSeries.Nonpositive.rho u c x = if htau : HahnSeries.Nonpositive.tauBall c x = 0 then (HahnSeries.Nonpositive.T c) x else HahnSeries.Nonpositive.reductionQuotient u c x htau

theorem HahnSeries.Nonpositive.tauBall_eq_zero_iff {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : tauBall c x = 0 ↔ (tau c) x = 0

The open-ball restriction vanishes exactly when the original open-class truncation does.

theorem HahnSeries.Nonpositive.tauBall_eq_one_of_tau_eq_one {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : (tau c) x = 1) : tauBall c x = 1

Restricting an open-class truncation equal to one to its open ball yields one.

theorem HahnSeries.Nonpositive.rho_of_tau_eq_zero {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : (tau c) x = 0) : rho u c x = (T c) x

In the zero branch, LM24's reduction is the closed-class truncation.

theorem HahnSeries.Nonpositive.rho_of_tau_ne_zero {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : (tau c) x ≠ 0) : rho u c x = reductionQuotient u c x ⋯

In the nonzero branch, LM24's reduction uses the quotient constructed through the Archimedean splitting.

theorem HahnSeries.Nonpositive.support_T_subset_range {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : (↑((T c) x)).support ⊆ Set.range ⇑(closedBallOrderEmbedding c)

theorem HahnSeries.Nonpositive.embDomain_TClosed {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : embDomain (closedBallOrderEmbedding c) (TClosed c x) = ↑((T c) x)

noncomputable def HahnSeries.Nonpositive.TClosedRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) : Nonpositive G R →+* HahnSeries (↥(FiniteArchimedeanClass.closedBall K c)) R

The closed-class truncation with its exponent domain restricted, as a ring homomorphism.

Equations

• HahnSeries.Nonpositive.TClosedRingHom c = { toFun := HahnSeries.Nonpositive.TClosed c, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem HahnSeries.Nonpositive.TClosedRingHom_apply {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (c : FiniteArchimedeanClass G) (x : Nonpositive G R) : (TClosedRingHom c) x = TClosed c x

theorem HahnSeries.Nonpositive.reductionQuotient_mul_tau {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (htau : tauBall c x ≠ 0) : reductionQuotient u c x htau * (tau c) x = (T c) x

The nonzero reduction quotient multiplied by the open-class truncation recovers the closed-class truncation. This is the defining quotient identity from LM24, Definition 8.2.4.

theorem HahnSeries.Nonpositive.rho_eq_self_iff_tau_eq_zero_or_one {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (x : Nonpositive G R) (hx : x ≠ 0) (hT : (T c) x = x) : rho u c x = x ↔ (tau c) x = 0 ∨ (tau c) x = 1

At a class containing the whole series, a nonzero fixed point of rho has open truncation zero or one. This is the fixed-class core of LM24, Proposition 8.2.5 (3) iff (4).

theorem HahnSeries.Nonpositive.rho_leadingClass_eq_self_iff_tau_eq_zero_or_one {K : Type u_1} {G : Type u_2} {R : Type u_3} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] (u : HahnEmbedding.ArchimedeanStrata K G) (x : Nonpositive G R) (hx : x ≠ 0) (horder : (↑x).order ≠ 0) : rho u (x.leadingClass horder) x = x ↔ (tau (x.leadingClass horder)) x = 0 ∨ (tau (x.leadingClass horder)) x = 1

At the class of a nonzero, nonconstant series' lowest exponent, LM24's reduction fixes the series exactly when its open-class truncation is zero or one. This is Proposition 8.2.5 (3) ↔ (4) away from the separate constant-series case.