Hahn series with strictly negative support

This file defines the series denoted by K((G^{<0})) in LM24, Section 2.1. Inside the ring of nonpositive Hahn series, they are exactly the kernel of the constant-coefficient homomorphism. This realizes them simultaneously as a two-sided ideal and as a nonunital ring.

For a coefficient subring Z, the truncation integer part is proved to have the source presentation Z + K((G^{<0})). The Lean definition remains the intrinsic pullback along the constant-coefficient homomorphism; the presentation theorem supplies the exact printed form without replacing the carrier by a chosen pair of summands.

noncomputable def HahnSeries.negativeIdeal (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] : Ideal (Nonpositive Γ R)

The ideal of nonpositive Hahn series with zero constant coefficient. Its elements are exactly the Hahn series with strictly negative support.

Equations

• HahnSeries.negativeIdeal Γ R = RingHom.ker HahnSeries.Nonpositive.constantCoeff

@[simp]

theorem HahnSeries.mem_negativeIdeal (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : Nonpositive Γ R} : x ∈ negativeIdeal Γ R ↔ (↑x).support ⊆ Set.Iio 0

Membership in negativeIdeal means that every support exponent is strictly negative.

@[reducible, inline]

abbrev HahnSeries.Negative (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] : Type (max u v)

Strictly negative Hahn series, represented as the subtype of negativeIdeal.

Equations

• HahnSeries.Negative Γ R = ↥(HahnSeries.negativeIdeal Γ R)

instance HahnSeries.negativeIdealIsTwoSided (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] : (negativeIdeal Γ R).IsTwoSided

theorem HahnSeries.Negative.constantCoeff_eq_zero {Γ : Type u} {R : Type v} [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Negative Γ R) : Nonpositive.constantCoeff ↑x = 0

A strictly negative Hahn series has zero constant coefficient.

@[simp]

theorem HahnSeries.Negative.coeff_zero {Γ : Type u} {R : Type v} [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Negative Γ R) : (↑↑x).coeff 0 = 0

The coefficient at exponent zero of a strictly negative Hahn series is zero.

theorem HahnSeries.Negative.support_subset {Γ : Type u} {R : Type v} [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Negative Γ R) : (↑↑x).support ⊆ Set.Iio 0

The support of a strictly negative Hahn series is contained in Set.Iio 0.

noncomputable def HahnSeries.Negative.single {Γ : Type u} {R : Type v} [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (g : Γ) (r : R) (hg : g < 0) : Negative Γ R

A single monomial with strictly negative exponent, regarded as a strictly negative Hahn series.

Equations

• HahnSeries.Negative.single g r hg = ⟨HahnSeries.Nonpositive.single g r ⋯, ⋯⟩

@[simp]

theorem HahnSeries.Negative.coe_single {Γ : Type u} {R : Type v} [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (g : Γ) (r : R) (hg : g < 0) : ↑↑(single g r hg) = (HahnSeries.single g) r

noncomputable def HahnSeries.Nonpositive.negativePart (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] : Nonpositive Γ R →+ Negative Γ R

Remove the constant coefficient from a nonpositive Hahn series.

Equations

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

@[simp]

theorem HahnSeries.Nonpositive.coe_negativePart (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Nonpositive Γ R) : ↑((negativePart Γ R) x) = x - C (constantCoeff x)

theorem HahnSeries.Nonpositive.support_negativePart (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Nonpositive Γ R) : (↑↑((negativePart Γ R) x)).support = (↑x).support ∩ Set.Iio 0

The support of the strictly negative part is the intersection of the original support with the strict negative cone.

theorem HahnSeries.Nonpositive.constant_add_negativePart (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Nonpositive Γ R) : C (constantCoeff x) + ↑((negativePart Γ R) x) = x

A nonpositive Hahn series is the sum of its constant term and its strictly negative part.

@[simp]

theorem HahnSeries.Nonpositive.negativePart_C (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (r : R) : (negativePart Γ R) (C r) = 0

The strictly negative part of a constant series is zero.

@[simp]

theorem HahnSeries.Nonpositive.negativePart_coe (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : Negative Γ R) : (negativePart Γ R) ↑x = x

Removing the constant coefficient from a strictly negative series leaves it unchanged.

noncomputable def HahnSeries.constantSubring (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (Z : Subring R) : Subring (Nonpositive Γ R)

The image in the nonpositive Hahn ring of a subring of the coefficient ring.

Equations

• HahnSeries.constantSubring Γ R Z = Subring.map HahnSeries.Nonpositive.C Z

theorem HahnSeries.mem_constantSubring (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {Z : Subring R} {x : Nonpositive Γ R} : x ∈ constantSubring Γ R Z ↔ ∃ (z : ↥Z), Nonpositive.C ↑z = x

Membership in the constant copy of Z means equality with the constant series attached to some element of Z.

theorem HahnSeries.mem_truncationIntegerPart_iff_exists_add_negative (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {Z : Subring R} {x : Nonpositive Γ R} : x ∈ truncationIntegerPart Γ Z ↔ ∃ (z : ↥Z) (n : Negative Γ R), x = Nonpositive.C ↑z + ↑n

A nonpositive Hahn series belongs to the truncation integer part exactly when it is the sum of a constant series from Z and a strictly negative Hahn series.

theorem HahnSeries.constant_add_negative_eq_iff (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {Z : Subring R} {z z' : ↥Z} {n n' : Negative Γ R} : Nonpositive.C ↑z + ↑n = Nonpositive.C ↑z' + ↑n' ↔ z = z' ∧ n = n'

The expression of a nonpositive Hahn series as a constant series from Z plus a strictly negative series is unique.

theorem HahnSeries.coe_truncationIntegerPart_eq_constantSubring_add_negativeIdeal (Γ : Type u) (R : Type v) [AddCommGroup Γ] [PartialOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (Z : Subring R) : ↑(truncationIntegerPart Γ Z) = ↑(constantSubring Γ R Z) + ↑(negativeIdeal Γ R)

The carrier of a truncation integer part is the pointwise sum of the constant copy of Z and the ideal of strictly negative Hahn series. This is the equality Z + K((G^{<0})) used in LM24.