Translated-truncation spans modulo J + K in Pommersheim--Shahriari

Pommersheim--Shahriari [PS06] study the vector space K((ℝ⁽≤0⁾)) / (J + K). This differs from Berarducci's germ ring, whose denominator is only J: the extra quotient by constant series is essential to their degree-two irreducibility criterion.

The submodule nearConstantSubmodule is proved to have exactly the carrier of Berarducci's additive subgroup nearConstantSubgroup. Thus the two developments use the same J + K, while this module exposes the scalar quotient needed for linear spans and dimensions.

For a series a, translatedTruncationSpan a is the space denoted V(a) in [PS06]: the span, modulo J + K, of its translated truncations at negative exponents.

References

• J. Pommersheim, S. Shahriari, Unique factorization in generalized power series rings, Proc. Amer. Math. Soc. 134 (2006), 1277–1287, cited as [PS06].

@[instance_reducible]

noncomputable instance PommersheimShahriari.seriesAlgebra {K : Type v} [Field K] : Algebra K (Berarducci.Series K)

Scalar multiplication on nonpositive Hahn series through the constant-series embedding.

Equations

• PommersheimShahriari.seriesAlgebra = HahnSeries.Nonpositive.C.toAlgebra

noncomputable def PommersheimShahriari.constantLinearMap {K : Type v} [Field K] : K →ₗ[K] Berarducci.Series K

The constant-series embedding as a linear map.

Equations

• PommersheimShahriari.constantLinearMap = { toFun := ⇑HahnSeries.Nonpositive.C, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def PommersheimShahriari.nearConstantSubmodule (K : Type v) [Field K] : Submodule K (Berarducci.Series K)

The scalar submodule J + K of negative-monomial-ideal elements plus constants.

Equations

• PommersheimShahriari.nearConstantSubmodule K = Submodule.restrictScalars K (HahnSeries.Nonpositive.negativeMonomialIdeal K) ⊔ PommersheimShahriari.constantLinearMap.range

theorem PommersheimShahriari.mem_nearConstantSubmodule_iff {K : Type v} [Field K] {b : Berarducci.Series K} : b ∈ nearConstantSubmodule K ↔ b ∈ Berarducci.nearConstantSubgroup K

The scalar submodule J + K has exactly the carrier of Berarducci's additive subgroup with the same name.

@[reducible, inline]

abbrev PommersheimShahriari.SeriesQuotientByJAddConstants (K : Type v) [Field K] : Type v

The [PS06] vector space K((ℝ⁽≤0⁾)) / (J + K).

Equations

• PommersheimShahriari.SeriesQuotientByJAddConstants K = (Berarducci.Series K ⧸ PommersheimShahriari.nearConstantSubmodule K)

noncomputable def PommersheimShahriari.toSeriesQuotientByJAddConstants {K : Type v} [Field K] : Berarducci.Series K →ₗ[K] SeriesQuotientByJAddConstants K

The quotient map from nonpositive Hahn series to the quotient by J + K.

Equations

• PommersheimShahriari.toSeriesQuotientByJAddConstants = (PommersheimShahriari.nearConstantSubmodule K).mkQ

theorem PommersheimShahriari.toSeriesQuotientByJAddConstants_eq_iff {K : Type v} [Field K] {b c : Berarducci.Series K} : toSeriesQuotientByJAddConstants b = toSeriesQuotientByJAddConstants c ↔ b - c ∈ Berarducci.nearConstantSubgroup K

Two series have the same class modulo J + K exactly when their difference lies in Berarducci's subgroup J + K.

theorem PommersheimShahriari.toSeriesQuotientByJAddConstants_eq_zero_iff {K : Type v} [Field K] {b : Berarducci.Series K} : toSeriesQuotientByJAddConstants b = 0 ↔ b ∈ Berarducci.nearConstantSubgroup K

A series has zero image modulo constants exactly when it lies in J + K.

noncomputable def PommersheimShahriari.translatedTruncationClass {K : Type v} [Field K] (b : HahnSeries ℝ K) (x : ℝ) : SeriesQuotientByJAddConstants K

The class modulo J + K of the translated truncation at x.

Equations

• PommersheimShahriari.translatedTruncationClass b x = PommersheimShahriari.toSeriesQuotientByJAddConstants (Berarducci.translatedTruncation b x)

theorem PommersheimShahriari.translatedTruncationClass_apply {K : Type v} [Field K] (b : HahnSeries ℝ K) (x : ℝ) : translatedTruncationClass b x = toSeriesQuotientByJAddConstants (Berarducci.translatedTruncation b x)

Evaluate a translated-truncation class modulo J + K.

noncomputable def PommersheimShahriari.translatedTruncationSpan {K : Type v} [Field K] (a : Berarducci.Series K) : Submodule K (SeriesQuotientByJAddConstants K)

[PS06]'s space V(a), spanned modulo J + K by translated truncations at negative exponents.

Equations

• PommersheimShahriari.translatedTruncationSpan a = Submodule.span K (PommersheimShahriari.translatedTruncationClass ↑a '' Set.Iio 0)

theorem PommersheimShahriari.translatedTruncationClass_mem_translatedTruncationSpan {K : Type v} [Field K] (a : Berarducci.Series K) {x : ℝ} (hx : x < 0) : translatedTruncationClass (↑a) x ∈ translatedTruncationSpan a

Every translated-truncation class at a negative exponent belongs to V(a).

theorem PommersheimShahriari.translatedTruncationSpan_le_iff {K : Type v} [Field K] {a : Berarducci.Series K} {p : Submodule K (SeriesQuotientByJAddConstants K)} : translatedTruncationSpan a ≤ p ↔ ∀ x < 0, translatedTruncationClass (↑a) x ∈ p

A subspace contains V(a) exactly when it contains every negative translated-truncation class used to generate V(a).