Cardinal-bounded leading-class integer-part splitting

This module restricts LM24, Fact 2.4.2(5) to Hahn series with support cardinality less than κ. The forward split always respects the bound on every inner coefficient. For the inverse, regularity of κ ensures that flattening the countable outer support over the Archimedean stratum, whose coefficients each have support smaller than κ, again has support smaller than κ.

The regularity hypothesis records the exact set-sized cardinal closure used here. It is not folded into the printed statement of LM24, where the intended omnific Hahn field has a proper-class exponent group and every individual support remains a set.

noncomputable def HahnSeries.Nonpositive.cardSuppLTInnerFieldSubtypeRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) : CardSuppLTField →+* HahnSeries (↥(FiniteArchimedeanClass.ball K c)) R

Embed the bounded inner Hahn field into the full inner Hahn field.

Equations

• HahnSeries.Nonpositive.cardSuppLTInnerFieldSubtypeRingHom c = (HahnSeries.cardSuppLTSubfield (↥(FiniteArchimedeanClass.ball K c)) R κ).subtype

noncomputable def HahnSeries.Nonpositive.forgetCardSuppLTInnerCoefficients {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (u : HahnEmbedding.ArchimedeanStrata K G) : Nonpositive (↥(u.stratum c)) CardSuppLTField →+* Nonpositive (↥(u.stratum c)) (HahnSeries (↥(FiniteArchimedeanClass.ball K c)) R)

Forget the cardinal bound on every coefficient of an outer nonpositive Hahn series.

Equations

• HahnSeries.Nonpositive.forgetCardSuppLTInnerCoefficients c u = HahnSeries.Nonpositive.coefficientMapRingHom (HahnSeries.Nonpositive.cardSuppLTInnerFieldSubtypeRingHom c)

@[simp]

theorem HahnSeries.Nonpositive.coeff_forgetCardSuppLTInnerCoefficients {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (u : HahnEmbedding.ArchimedeanStrata K G) (y : Nonpositive (↥(u.stratum c)) CardSuppLTField) (s : ↥(u.stratum c)) : (↑((forgetCardSuppLTInnerCoefficients c u) y)).coeff s = ↑((↑y).coeff s)

Forgetting bounded inner coefficients preserves their underlying Hahn series.

noncomputable def HahnSeries.Nonpositive.forgetSplitCardSuppLTIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) : ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z)) →+* ↥(truncationIntegerPart (↥(u.stratum c)) (innerIntegerPartSubring c Z))

Forget the inner cardinal bounds on a split truncation integer part.

Equations

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

@[simp]

theorem HahnSeries.Nonpositive.coe_forgetSplitCardSuppLTIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (y : ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))) : ↑((forgetSplitCardSuppLTIntegerPartRingHom u c Z) y) = (forgetCardSuppLTInnerCoefficients c u) ↑y

Forgetting the target bound acts by forgetting every inner coefficient.

theorem HahnSeries.Nonpositive.forget_splitTruncationCardSuppLTIntegerPart {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (b : ↥(cardSuppLTTruncationIntegerPart Z)) : (forgetSplitCardSuppLTIntegerPartRingHom u c Z) (splitTruncationCardSuppLTIntegerPart u c Z b) = (splitIntegerPartRingHom u c Z) ((CardSuppLTTruncationIntegerPart.toTruncationIntegerPartRingHom Z) b)

Forgetting bounds after the bounded split recovers the full integer-part split.

theorem HahnSeries.Nonpositive.forgetSplitCardSuppLTIntegerPartRingHom_injective {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) : Function.Injective ⇑(forgetSplitCardSuppLTIntegerPartRingHom u c Z)

Forgetting bounded inner coefficients is injective on the split integer part.

noncomputable def HahnSeries.Nonpositive.splitCardSuppLTIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) : ↥(cardSuppLTTruncationIntegerPart Z) →+* ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))

The leading-class split as a ring homomorphism on cardinal-bounded integer parts.

Equations

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

@[simp]

theorem HahnSeries.Nonpositive.splitCardSuppLTIntegerPartRingHom_apply {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (b : ↥(cardSuppLTTruncationIntegerPart Z)) : (splitCardSuppLTIntegerPartRingHom u c Z) b = splitTruncationCardSuppLTIntegerPart u c Z b

The bounded split ring homomorphism applies by the bounded split construction.

noncomputable def HahnSeries.Nonpositive.cardSuppLTFixedIntegerPartSubring {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (Z : Subring R) : Subring ↥(cardSuppLTTruncationIntegerPart Z)

The bounded fixed integer part is the preimage of the full fixed integer part under the bound-forgetting homomorphism.

Equations

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

def HahnSeries.Nonpositive.forgetCardSuppLTFixedIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (Z : Subring R) : ↥(cardSuppLTFixedIntegerPartSubring c Z) →+* ↥(fixedIntegerPartSubring c Z)

Forget the cardinal bound on a bounded fixed integer-part element.

Equations

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

@[simp]

theorem HahnSeries.Nonpositive.coe_forgetCardSuppLTFixedIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (Z : Subring R) (x : ↥(cardSuppLTFixedIntegerPartSubring c Z)) : ↑((forgetCardSuppLTFixedIntegerPartRingHom c Z) x) = (CardSuppLTTruncationIntegerPart.toTruncationIntegerPartRingHom Z) ↑x

Forgetting a bounded fixed element uses the underlying bound-forgetting homomorphism.

theorem HahnSeries.Nonpositive.forgetCardSuppLTFixedIntegerPartRingHom_injective {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (Z : Subring R) : Function.Injective ⇑(forgetCardSuppLTFixedIntegerPartRingHom c Z)

Forgetting the bound is injective on bounded fixed integer-part elements.

noncomputable def HahnSeries.Nonpositive.splitCardSuppLTFixedIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) : ↥(cardSuppLTFixedIntegerPartSubring c Z) →+* ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))

Restrict the bounded split homomorphism to the bounded fixed integer part.

Equations

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

@[simp]

theorem HahnSeries.Nonpositive.splitCardSuppLTFixedIntegerPartRingHom_apply {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (x : ↥(cardSuppLTFixedIntegerPartSubring c Z)) : (splitCardSuppLTFixedIntegerPartRingHom u c Z) x = (splitCardSuppLTIntegerPartRingHom u c Z) ↑x

The fixed bounded split is the unrestricted bounded split of the underlying element.

theorem HahnSeries.Nonpositive.forget_splitCardSuppLTFixedIntegerPartRingHom {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (x : ↥(cardSuppLTFixedIntegerPartSubring c Z)) : (forgetSplitCardSuppLTIntegerPartRingHom u c Z) ((splitCardSuppLTFixedIntegerPartRingHom u c Z) x) = (splitFixedIntegerPartRingHom u c Z) ((forgetCardSuppLTFixedIntegerPartRingHom c Z) x)

Forgetting bounds commutes with the fixed integer-part split.

theorem HahnSeries.Nonpositive.cardSupp_unsplit_forgetSplitCardSuppLTIntegerPart_lt {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] [Fact κ.IsRegular] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (y : ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))) : (↑↑↑(unsplitIntegerPart u c Z ((forgetSplitCardSuppLTIntegerPartRingHom u c Z) y))).cardSupp < κ

The full unsplit of a bounded outer integer-part element still has support smaller than a regular κ.

noncomputable def HahnSeries.Nonpositive.unsplitCardSuppLTIntegerPart {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] [Fact κ.IsRegular] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (y : ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))) : ↥(cardSuppLTFixedIntegerPartSubring c Z)

Unsplit a bounded outer integer-part element and retain the support-cardinality witness.

Equations

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

theorem HahnSeries.Nonpositive.forget_unsplitCardSuppLTIntegerPart {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] [Fact κ.IsRegular] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (y : ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))) : (forgetCardSuppLTFixedIntegerPartRingHom c Z) (unsplitCardSuppLTIntegerPart u c Z y) = unsplitIntegerPart u c Z ((forgetSplitCardSuppLTIntegerPartRingHom u c Z) y)

Forgetting the source bound after bounded unsplitting recovers the full unsplit.

noncomputable def HahnSeries.Nonpositive.splitCardSuppLTFixedIntegerPartRingEquiv {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] [Fact κ.IsRegular] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) : ↥(cardSuppLTFixedIntegerPartSubring c Z) ≃+* ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))

For regular κ, the bounded fixed integer part is equivalent to the outer integer part over the bounded inner coefficient integer part.

Equations

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

@[simp]

theorem HahnSeries.Nonpositive.splitCardSuppLTFixedIntegerPartRingEquiv_apply {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] [Fact κ.IsRegular] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (x : ↥(cardSuppLTFixedIntegerPartSubring c Z)) : (splitCardSuppLTFixedIntegerPartRingEquiv u c Z) x = (splitCardSuppLTFixedIntegerPartRingHom u c Z) x

The bounded fixed equivalence applies by the bounded split ring homomorphism.

@[simp]

theorem HahnSeries.Nonpositive.splitCardSuppLTFixedIntegerPartRingEquiv_symm_apply {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] [Fact κ.IsRegular] (u : HahnEmbedding.ArchimedeanStrata K G) (c : FiniteArchimedeanClass G) (Z : Subring R) (y : ↥(truncationIntegerPart (↥(u.stratum c)) (cardSuppLTTruncationIntegerPart Z))) : (splitCardSuppLTFixedIntegerPartRingEquiv u c Z).symm y = unsplitCardSuppLTIntegerPart u c Z y

The inverse bounded fixed equivalence is the bounded unsplit construction.

theorem HahnSeries.Nonpositive.mem_cardSuppLTFixedIntegerPartSubring_iff {K : Type u_1} {G : Type u_2} {R : Type u_3} {κ : Cardinal.{u_2}} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module K G] [IsOrderedModule K G] [Field R] [Fact (Cardinal.aleph0 < κ)] (c : FiniteArchimedeanClass G) (Z : Subring R) (x : ↥(cardSuppLTTruncationIntegerPart Z)) : x ∈ cardSuppLTFixedIntegerPartSubring c Z ↔ (T c) ((CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) x) = (CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) x

Membership in the bounded fixed integer part is invariance under the closed-class cut.