Rational tail quotients of the surreals

For a family of finite Archimedean classes, its common tail is a rational subspace of the surreals. Quotienting by that subspace gives the usual ordered tail quotient together with its native rational-vector-space structure. At a nonempty limit family, the quotient is Cauchy complete for its additive uniformity: the canonical representatives of the family are a small positive coinitial family, and surreal simplicity fills every cut indexed by that family.

This presentation is used when a small closed rational subspace of the tail quotient must be formed. Its additive subgroup is exactly the tail kernel used by the older additive presentation.

@[reducible, inline]

abbrev Surreal.RationalTailQuotient (T : Set (FiniteArchimedeanClass Surreal)) : Type (u + 1)

The quotient by the rational subspace underlying a family of Archimedean tails.

Equations

• Surreal.RationalTailQuotient T = (Surreal ⧸ FiniteArchimedeanClass.tailSubmodule ℚ T)

@[instance_reducible]

noncomputable instance Surreal.rationalTailQuotientLinearOrder (T : Set (FiniteArchimedeanClass Surreal)) : LinearOrder (RationalTailQuotient T)

Equations

• Surreal.rationalTailQuotientLinearOrder T = ConvexQuotient.instLinearOrder

instance Surreal.rationalTailQuotientIsOrderedAddMonoid (T : Set (FiniteArchimedeanClass Surreal)) : IsOrderedAddMonoid (RationalTailQuotient T)

instance Surreal.rationalTailQuotientPosSMulMono (T : Set (FiniteArchimedeanClass Surreal)) : PosSMulMono ℚ (RationalTailQuotient T)

instance Surreal.rationalTailQuotientPosSMulStrictMono (T : Set (FiniteArchimedeanClass Surreal)) : PosSMulStrictMono ℚ (RationalTailQuotient T)

theorem Surreal.rationalTailQuotient_abs (T : Set (FiniteArchimedeanClass Surreal)) (x : Surreal) : |Submodule.Quotient.mk x| = Submodule.Quotient.mk |x|

Absolute value commutes with projection to a rational tail quotient.

theorem Surreal.archimedeanClass_mk_lt_of_rationalTailQuotient_mk_lt (T : Set (FiniteArchimedeanClass Surreal)) {x y : Surreal} (h : ArchimedeanClass.mk (Submodule.Quotient.mk x) < ArchimedeanClass.mk (Submodule.Quotient.mk y)) : ArchimedeanClass.mk x < ArchimedeanClass.mk y

A strict comparison of quotient Archimedean classes reflects to the chosen surreal representatives.

theorem Surreal.exists_nonzeroSupportClass_bound (T : Set (FiniteArchimedeanClass Surreal)) (q : FiniteArchimedeanClass (RationalTailQuotient T)) (S W : Set Surreal) (hqocc : ↑q ∈ ArchimedeanClass.mk '' Submodule.Quotient.mk '' S) (hW : ∀ g ∈ W, g ≠ 0 → Submodule.Quotient.mk g ∉ q.closedBallAddSubgroup) (hWocc : ∀ g ∈ W, g ≠ 0 → ArchimedeanClass.mk g ∈ ArchimedeanClass.mk '' S) : ∃ c ∈ ArchimedeanClass.mk '' (S \ {0}), ArchimedeanClass.mk '' (W \ {0}) ⊆ ArchimedeanClass.mk '' (S \ {0}) ∩ Set.Iio c

Suppose a chosen quotient class is met by S, and every nonzero member of W lies outside its quotient closed ball while retaining a class met by S. Then the nonzero support classes of W form a strict initial segment of the support classes of S.

@[instance_reducible]

noncomputable instance Surreal.rationalTailQuotientTopologicalSpace (T : Set (FiniteArchimedeanClass Surreal)) : TopologicalSpace (RationalTailQuotient T)

Equations

• Surreal.rationalTailQuotientTopologicalSpace T = Preorder.topology (Surreal.RationalTailQuotient T)

instance Surreal.rationalTailQuotientOrderTopology (T : Set (FiniteArchimedeanClass Surreal)) : OrderTopology (RationalTailQuotient T)

instance Surreal.rationalTailQuotientDenselyOrdered (T : Set (FiniteArchimedeanClass Surreal)) : DenselyOrdered (RationalTailQuotient T)

instance Surreal.rationalTailQuotientIsTopologicalAddGroup (T : Set (FiniteArchimedeanClass Surreal)) : IsTopologicalAddGroup (RationalTailQuotient T)

@[instance_reducible]

noncomputable instance Surreal.rationalTailQuotientUniformSpace (T : Set (FiniteArchimedeanClass Surreal)) : UniformSpace (RationalTailQuotient T)

Equations

• Surreal.rationalTailQuotientUniformSpace T = IsTopologicalAddGroup.rightUniformSpace (Surreal.RationalTailQuotient T)

instance Surreal.rationalTailQuotientIsUniformAddGroup (T : Set (FiniteArchimedeanClass Surreal)) : IsUniformAddGroup (RationalTailQuotient T)

noncomputable def Surreal.rationalTailQuotientScale (T : Set (FiniteArchimedeanClass Surreal)) [Small.{u, u + 1} ↑T] (i : Shrink.{u, u + 1} ↑T) : RationalTailQuotient T

Canonical positive scales in a rational tail quotient, indexed by a small copy of the class family.

Equations

• Surreal.rationalTailQuotientScale T i = Submodule.Quotient.mk (↑((equivShrink ↑T).symm i)).positiveRepresentative

@[simp]

theorem Surreal.rationalTailQuotientScale_apply (T : Set (FiniteArchimedeanClass Surreal)) [Small.{u, u + 1} ↑T] (i : Shrink.{u, u + 1} ↑T) : rationalTailQuotientScale T i = Submodule.Quotient.mk (↑((equivShrink ↑T).symm i)).positiveRepresentative

The canonical quotient scale is represented by the positive representative of its class.

theorem Surreal.rationalTailQuotientScale_pos (T : Set (FiniteArchimedeanClass Surreal)) [Small.{u, u + 1} ↑T] (hT : ∀ c ∈ T, ∃ d ∈ T, c < d) (i : Shrink.{u, u + 1} ↑T) : 0 < rationalTailQuotientScale T i

At a limit family, every canonical tail-quotient scale is positive.

theorem Surreal.exists_rationalTailQuotientScale_le (T : Set (FiniteArchimedeanClass Surreal)) [Small.{u, u + 1} ↑T] {x : RationalTailQuotient T} (hx : 0 < x) : ∃ (i : Shrink.{u, u + 1} ↑T), rationalTailQuotientScale T i ≤ x

The canonical scales are coinitial among the positive elements of the tail quotient.

theorem Surreal.rationalTailQuotientScale_pos_and_coinitial (T : Set (FiniteArchimedeanClass Surreal)) [Small.{u, u + 1} ↑T] (hT : ∀ c ∈ T, ∃ d ∈ T, c < d) : (∀ (i : Shrink.{u, u + 1} ↑T), 0 < rationalTailQuotientScale T i) ∧ ∀ (x : RationalTailQuotient T), 0 < x → ∃ (i : Shrink.{u, u + 1} ↑T), rationalTailQuotientScale T i ≤ x

The positive representatives of a limit family give a small coinitial family in its rational tail quotient.

theorem Surreal.completeSpace_rationalTailQuotient (T : Set (FiniteArchimedeanClass Surreal)) [Small.{u, u + 1} ↑T] [Nonempty ↑T] (hT : ∀ c ∈ T, ∃ d ∈ T, c < d) : CompleteSpace (RationalTailQuotient T)

A rational tail quotient at a nonempty limit family is Cauchy complete for its additive uniformity.