Omnific integers and the bounded Hahn integer part

Every Conway normal form has support smaller than the universe cardinal bounding SurrealHahnSeries. Conversely, every bounded nonpositive Hahn series whose constant coefficient is an integer defines a small Conway normal form, hence an omnific integer.

This gives a ring equivalence between Conway's cut-defined omnific integers and the bounded Hahn truncation integer part used by the set-sized form of LM24, Proposition 9.2.2.

@[reducible, inline]

noncomputable abbrev Surreal.OmnificInteger.SmallSupportIntegerPart : Subring HahnSeries.CardSuppLTField

The universe-bounded Hahn truncation integer part corresponding to omnific integers.

Equations

• Surreal.OmnificInteger.SmallSupportIntegerPart = HahnSeries.cardSuppLTTruncationIntegerPart Surreal.realIntegerSubring

noncomputable def Surreal.OmnificInteger.ofSmallSupportIntegerPart (b : ↥SmallSupportIntegerPart) : OmnificInteger

Recover the omnific integer represented by a bounded nonpositive Hahn integer part.

Equations

• Surreal.OmnificInteger.ofSmallSupportIntegerPart b = ⟨Surreal.OmnificInteger.ofSmallSupportSurreal✝ b, ⋯⟩

noncomputable def Surreal.OmnificInteger.toSmallSupportIntegerPart (x : OmnificInteger) : ↥SmallSupportIntegerPart

Put an omnific integer into the universe-bounded Hahn truncation integer part.

Equations

• x.toSmallSupportIntegerPart = ⟨⟨(↑x).toFullHahnSeries, ⋯⟩, ⋯⟩

@[simp]

theorem Surreal.OmnificInteger.coe_toSmallSupportIntegerPart (x : OmnificInteger) : ↑↑x.toSmallSupportIntegerPart = (↑x).toFullHahnSeries

The bounded Hahn image has exactly the full Conway normal form as its underlying series.

@[simp]

theorem Surreal.OmnificInteger.toFullHahnSeries_ofSmallSupportIntegerPart (b : ↥SmallSupportIntegerPart) : (↑(ofSmallSupportIntegerPart b)).toFullHahnSeries = ↑↑b

Recovering a bounded Hahn integer part preserves its underlying full Hahn series.

@[simp]

theorem Surreal.OmnificInteger.ofSmallSupportIntegerPart_toSmallSupportIntegerPart (x : OmnificInteger) : ofSmallSupportIntegerPart x.toSmallSupportIntegerPart = x

Recovering the omnific integer after passing to bounded Hahn series is the identity.

@[simp]

theorem Surreal.OmnificInteger.toSmallSupportIntegerPart_ofSmallSupportIntegerPart (b : ↥SmallSupportIntegerPart) : (ofSmallSupportIntegerPart b).toSmallSupportIntegerPart = b

Returning to bounded Hahn series after recovering an omnific integer is the identity.

noncomputable def Surreal.OmnificInteger.smallSupportIntegerPartAddEquiv : OmnificInteger ≃+ ↥SmallSupportIntegerPart

Omnific integers are additively equivalent to the bounded Hahn truncation integer part.

Equations

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

@[simp]

theorem Surreal.OmnificInteger.smallSupportIntegerPartAddEquiv_apply (x : OmnificInteger) : smallSupportIntegerPartAddEquiv x = x.toSmallSupportIntegerPart

Evaluation of the additive Conway/Hahn equivalence.

noncomputable def Surreal.OmnificInteger.smallSupportIntegerPartRingEquiv : OmnificInteger ≃+* ↥SmallSupportIntegerPart

The Conway/Hahn ring equivalence for universe-bounded omnific integers.

Equations

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

@[simp]

theorem Surreal.OmnificInteger.smallSupportIntegerPartRingEquiv_apply (x : OmnificInteger) : smallSupportIntegerPartRingEquiv x = x.toSmallSupportIntegerPart

Evaluation of the Conway/Hahn ring equivalence.

Signed surreal exponents

@[reducible, inline]

noncomputable abbrev Surreal.OmnificInteger.SignedSmallSupportIntegerPart : Subring HahnSeries.CardSuppLTField

The bounded Hahn truncation integer part with t = ω⁻¹ exponents written as ordinary surreal numbers.

Equations

• Surreal.OmnificInteger.SignedSmallSupportIntegerPart = HahnSeries.cardSuppLTTruncationIntegerPart Surreal.realIntegerSubring

noncomputable def Surreal.OmnificInteger.smallSupportIntegerPartSignedRingEquiv : ↥SmallSupportIntegerPart ≃+* ↥SignedSmallSupportIntegerPart

Reindex the dual-exponent bounded integer part by sending a Conway exponent i to the ordinary surreal exponent -i.

Equations

• Surreal.OmnificInteger.smallSupportIntegerPartSignedRingEquiv = HahnSeries.cardSuppLTTruncationIntegerPartRingEquiv Surreal.dualExponentOrderAddMonoidIso Surreal.realIntegerSubring

@[simp]

theorem Surreal.OmnificInteger.smallSupportIntegerPartSignedRingEquiv_apply (b : ↥SmallSupportIntegerPart) : smallSupportIntegerPartSignedRingEquiv b = (HahnSeries.cardSuppLTTruncationIntegerPartRingEquiv dualExponentOrderAddMonoidIso realIntegerSubring) b

Evaluation of signed exponent reindexing on bounded integer parts.

noncomputable def Surreal.OmnificInteger.toSignedSmallSupportIntegerPart (x : OmnificInteger) : ↥SignedSmallSupportIntegerPart

Put an omnific integer into the bounded Hahn integer part with signed surreal exponents.

Equations

• x.toSignedSmallSupportIntegerPart = Surreal.OmnificInteger.smallSupportIntegerPartSignedRingEquiv x.toSmallSupportIntegerPart

@[simp]

theorem Surreal.OmnificInteger.coe_toSignedSmallSupportIntegerPart (x : OmnificInteger) : ↑↑x.toSignedSmallSupportIntegerPart = (↑x).toSignedFullHahnSeries

The signed bounded Hahn image has exactly the signed full Conway normal form.

noncomputable def Surreal.OmnificInteger.toSignedNonpositiveHahn (x : OmnificInteger) : HahnSeries.Nonpositive Surreal ℝ

The nonpositive signed Hahn series underlying an omnific integer.

Equations

• x.toSignedNonpositiveHahn = (HahnSeries.CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Surreal.realIntegerSubring) x.toSignedSmallSupportIntegerPart

@[simp]

theorem Surreal.OmnificInteger.coe_toSignedNonpositiveHahn (x : OmnificInteger) : ↑x.toSignedNonpositiveHahn = (↑x).toSignedFullHahnSeries

Coercing the signed nonpositive image recovers the signed full Conway normal form.

noncomputable def Surreal.OmnificInteger.signedSmallSupportIntegerPartRingEquiv : OmnificInteger ≃+* ↥SignedSmallSupportIntegerPart

The signed-exponent Conway/Hahn ring equivalence for universe-bounded omnific integers.

Equations

• Surreal.OmnificInteger.signedSmallSupportIntegerPartRingEquiv = Surreal.OmnificInteger.smallSupportIntegerPartRingEquiv.trans Surreal.OmnificInteger.smallSupportIntegerPartSignedRingEquiv

@[simp]

theorem Surreal.OmnificInteger.signedSmallSupportIntegerPartRingEquiv_apply (x : OmnificInteger) : signedSmallSupportIntegerPartRingEquiv x = x.toSignedSmallSupportIntegerPart

Evaluation of the signed Conway/Hahn ring equivalence.