Hahn embedding theorem on ordered modules

This file proves a variant of the Hahn embedding theorem:

For a linearly ordered module M over an Archimedean division ring K, there exists a strictly monotone linear map to lexicographically ordered HahnSeries (FiniteArchimedeanClass M) R with an archimedean K-module R, as long as there are embeddings from a certain family of Archimedean submodules to R.

The family of Archimedean submodules HahnEmbedding.ArchimedeanStrata K M is indexed by (c : ArchimedeanClass M), and each submodule is a complement of ArchimedeanClass.ball K c under ArchimedeanClass.closedBall K c. The embeddings from these submodules are specified by HahnEmbedding.Seed K M R.

By setting K = ℚ and R = ℝ, the condition can be trivially satisfied, leading to a proof of the classic Hahn embedding theorem. (TODO: implement this)

Main theorem

• hahnEmbedding_isOrderedModule: there exists a strictly monotone M →ₗ[K] Lex (HahnSeries (FiniteArchimedeanClass M) R) that maps ArchimedeanClass M to HahnSeries.orderTop in the expected way, as long as HahnEmbedding.Seed K M R is nonempty.

References

• M. Hausner, J.G. Wendel, Ordered vector spaces

Step 1: base embedding

We start with HahnEmbedding.ArchimedeanStrata that gives a family of Archimedean submodules, and a "seed" HahnEmbedding.Seed that specifies how to embed each HahnEmbedding.ArchimedeanStrata.stratum into R.

From these, we create a partial map from the direct sum of all stratum to HahnSeries Γ R. If ArchimedeanClass M is finite, the direct sum is the entire M and we are done (though we don't handle this case separately). Otherwise, we will extend the map to M in the following steps.

structure HahnEmbedding.ArchimedeanStrata (K : Type u_1) [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] (M : Type u_2) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] : Type u_2

A family of submodules indexed by ArchimedeanClass M that are complements between ArchimedeanClass.ball and ArchimedeanClass.closedBall.

• stratum : ArchimedeanClass M → Submodule K M

  For each ArchimedeanClass, specify a corresponding submodule.

• disjoint_ball_stratum (c : ArchimedeanClass M) : Disjoint (ArchimedeanClass.ball K c) (self.stratum c)

  stratum and ArchimedeanClass.ball are disjoint.

• ball_sup_stratum_eq (c : ArchimedeanClass M) : ArchimedeanClass.ball K c ⊔ self.stratum c = ArchimedeanClass.closedBall K c

  stratum and ArchimedeanClass.ball are codisjoint under ArchimedeanClass.closedBall.

@[simp]

theorem HahnEmbedding.ArchimedeanStrata.ball_eq_closedBall {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {c : ArchimedeanClass M} : ArchimedeanClass.ball K c = ArchimedeanClass.closedBall K c ↔ c = ⊤

@[simp]

theorem HahnEmbedding.ArchimedeanStrata.stratum_top {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) : u.stratum ⊤ = ⊥

theorem HahnEmbedding.ArchimedeanStrata.stratum_eq_bot_iff {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) {c : ArchimedeanClass M} : u.stratum c = ⊥ ↔ c = ⊤

theorem HahnEmbedding.ArchimedeanStrata.nontrivial_stratum {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) {c : ArchimedeanClass M} (h : c ≠ ⊤) : Nontrivial ↥(u.stratum c)

theorem HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) {c : ArchimedeanClass M} {a : M} (ha : a ∈ u.stratum c) (h0 : a ≠ 0) : ArchimedeanClass.mk a = c

instance HahnEmbedding.ArchimedeanStrata.archimedean_stratum {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) {c : ArchimedeanClass M} : Archimedean ↥(u.stratum c)

theorem HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) : iSupIndep u.stratum

def HahnEmbedding.ArchimedeanStrata.baseDomain {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) : Submodule K M

The minimal submodule that contains all strata.

This is the domain of our "base" embedding into Hahn series, which we will extend into a full embedding.

Equations

• u.baseDomain = ⨆ (c : ArchimedeanClass M), u.stratum c

@[reducible, inline]

abbrev HahnEmbedding.ArchimedeanStrata.stratum' {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) (c : ArchimedeanClass M) : Submodule K ↥u.baseDomain

ArchimedeanStrata.stratum as a submodule of ArchimedeanStrata.baseDomain.

Equations

• u.stratum' c = Submodule.comap u.baseDomain.subtype (u.stratum c)

theorem HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum' {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) : iSupIndep u.stratum'

theorem HahnEmbedding.ArchimedeanStrata.isInternal_stratum' {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) : DirectSum.IsInternal u.stratum'

noncomputable instance HahnEmbedding.ArchimedeanStrata.instDecompositionArchimedeanClassSubtypeMemSubmoduleBaseDomainStratum' {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (u : ArchimedeanStrata K M) : DirectSum.Decomposition u.stratum'

Equations

• u.instDecompositionArchimedeanClassSubtypeMemSubmoduleBaseDomainStratum' = DirectSum.IsInternal.chooseDecomposition u.stratum' ⋯

structure HahnEmbedding.Seed (K : Type u_1) [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] (M : Type u_2) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] (R : Type u_3) [AddCommGroup R] [LinearOrder R] [Module K R] extends HahnEmbedding.ArchimedeanStrata K M : Type (max u_2 u_3)

HahnEmbedding.Seed extends HahnEmbedding.ArchimedeanStrata by specifying strictly monotone linear maps from each stratum to module R.

• stratum : ArchimedeanClass M → Submodule K M
• disjoint_ball_stratum (c : ArchimedeanClass M) : Disjoint (ArchimedeanClass.ball K c) (self.stratum c)
• ball_sup_stratum_eq (c : ArchimedeanClass M) : ArchimedeanClass.ball K c ⊔ self.stratum c = ArchimedeanClass.closedBall K c
• coeff (c : ArchimedeanClass M) : ↥(self.stratum c) →ₗ[K] R

  For each stratum, specify a linear map to R as the Hahn series coefficient.

• strictMono_coeff (c : ArchimedeanClass M) : StrictMono ⇑(self.coeff c)

  coeff is strictly monotone.

def HahnEmbedding.Seed.coeff' {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) (c : ArchimedeanClass M) : ↥(seed.stratum' c) →ₗ[K] R

HahnEmbedding.Seed.coeff with ArchimedeanStrata.stratum' as domain.

Equations

• seed.coeff' c = seed.coeff c ∘ₗ seed.baseDomain.subtype.submoduleComap (seed.stratum c)

noncomputable def HahnEmbedding.Seed.hahnCoeff {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) : ↥seed.baseDomain →ₗ[K] DirectSum (ArchimedeanClass M) fun (x : ArchimedeanClass M) => R

Coefficients of Hahn series for each baseDomain element.

Equations

• seed.hahnCoeff = DirectSum.lmap seed.coeff' ∘ₗ ↑(DirectSum.decomposeLinearEquiv seed.stratum')

theorem HahnEmbedding.Seed.hahnCoeff_apply {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) {x : ↥seed.baseDomain} {f : Π₀ (c : ArchimedeanClass M), ↥(seed.stratum c)} (h : ↑x = f.sum fun (c : ArchimedeanClass M) => ⇑(seed.stratum c).subtype) (c : ArchimedeanClass M) : (seed.hahnCoeff x) c = (seed.coeff c) (f c)

noncomputable def HahnEmbedding.Seed.baseEmbedding {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)

Combining all HahnEmbedding.Seed.coeff as a partial linear map from HahnEmbedding.Seed.baseDomain to HahnSeries.

Equations

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

theorem HahnEmbedding.Seed.domain_baseEmbedding {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) : seed.baseEmbedding.domain = seed.baseDomain

theorem HahnEmbedding.Seed.coeff_baseEmbedding {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) {x : ↥seed.baseEmbedding.domain} {f : Π₀ (c : ArchimedeanClass M), ↥(seed.stratum c)} (h : ↑x = f.sum fun (c : ArchimedeanClass M) => ⇑(seed.stratum c).subtype) (c : FiniteArchimedeanClass M) : (ofLex (↑seed.baseEmbedding x)).coeff c = (seed.coeff ↑c) (f ↑c)

theorem HahnEmbedding.Seed.mem_domain_baseEmbedding {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) {x : M} {c : ArchimedeanClass M} (h : x ∈ seed.stratum c) : x ∈ seed.baseEmbedding.domain

Step 2: characterize partial embedding

We characterize the base embedding as a member of a class of partial linear embeddings HahnEmbedding.Partial. These embeddings share nice properties, including being strictly monotone, transferring ArchimedeanClass to HahnEmbedding.orderTop, and being "truncation-closed" (see HahnEmbedding.IsPartial.truncLT_mem_range).

structure HahnEmbedding.IsPartial {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) (f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)) : Prop

A partial linear map is called a "partial Hahn embedding" if it extends HahnEmbedding.Seed.baseEmbedding, is strictly monotone, and is truncation-closed.

• strictMono : StrictMono ↑f

  A partial Hahn embedding is strictly monotone.

• baseEmbedding_le : seed.baseEmbedding ≤ f

  A partial Hahn embedding always extends baseEmbedding.

• truncLT_mem_range (x : ↥f.domain) (c : FiniteArchimedeanClass M) : toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑f x))) ∈ LinearMap.range f.toFun

  If a Hahn series $f$ is in the range, then any truncation of $f$ is also in the range.

theorem HahnEmbedding.Seed.baseEmbedding_pos {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) {x : ↥seed.baseEmbedding.domain} (hx : 0 < x) : 0 < ↑seed.baseEmbedding x

theorem HahnEmbedding.Seed.baseEmbedding_strictMono {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) [IsOrderedAddMonoid R] : StrictMono ↑seed.baseEmbedding

theorem HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) (x : ↥seed.baseEmbedding.domain) (c : FiniteArchimedeanClass M) : toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ LinearMap.range seed.baseEmbedding.toFun

theorem HahnEmbedding.Seed.isPartial_baseEmbedding {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) [IsOrderedAddMonoid R] : IsPartial seed seed.baseEmbedding

HahnEmbedding.Seed.baseEmbedding is a partial Hahn embedding.

@[reducible, inline]

abbrev HahnEmbedding.Partial {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) : Type (max 0 u_2 u_3)

The type of all partial Hahn embeddings.

Equations

• HahnEmbedding.Partial seed = { f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R) // HahnEmbedding.IsPartial seed f }

noncomputable instance HahnEmbedding.Partial.instInhabitedOfIsOrderedAddMonoid {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} [IsOrderedAddMonoid R] : Inhabited (Partial seed)

Equations

• HahnEmbedding.Partial.instInhabitedOfIsOrderedAddMonoid = { default := ⟨seed.baseEmbedding, ⋯⟩ }

def HahnEmbedding.Partial.toOrderAddMonoidHom {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) : ↥(↑f).domain →+o Lex (HahnSeries (FiniteArchimedeanClass M) R)

HahnEmbedding.Partial as an OrderedAddMonoidHom.

Equations

• f.toOrderAddMonoidHom = { toFun := (↑f).toFun.toFun, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

theorem HahnEmbedding.Partial.toOrderAddMonoidHom_apply {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) (x : ↥(↑f).domain) : f.toOrderAddMonoidHom x = ↑↑f x

theorem HahnEmbedding.Partial.toOrderAddMonoidHom_injective {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) : Function.Injective ⇑f.toOrderAddMonoidHom

theorem HahnEmbedding.Partial.mem_domain {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) {x : M} {c : ArchimedeanClass M} (hx : x ∈ seed.stratum c) : x ∈ (↑f).domain

theorem HahnEmbedding.Partial.apply_of_mem_stratum {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) {x : ↥(↑f).domain} {c : FiniteArchimedeanClass M} (hx : ↑x ∈ seed.stratum ↑c) : ↑↑f x = toLex ((HahnSeries.single c) ((seed.coeff ↑c) ⟨↑x, hx⟩))

theorem HahnEmbedding.Partial.archimedeanClassMk_eq_iff {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] (x y : ↥(↑f).domain) : ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y) ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Archimedean equivalence is preserved by f.

theorem HahnEmbedding.Partial.orderTop_eq_iff {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (x y : ↥(↑f).domain) : (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Archimedean equivalence of input is transferred to HahnSeries.orderTop equality.

theorem HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (x : ↥(↑f).domain) : (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Archimedean class of the input is transferred to HahnSeries.orderTop.

theorem HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : ↥(↑f).domain} (hx0 : ↑x ≠ 0) : (ofLex (↑↑f x)).orderTop = ↑(FiniteArchimedeanClass.mk (↑x) hx0)

theorem HahnEmbedding.Partial.coeff_eq_zero_of_mem {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {c : ArchimedeanClass M} {x : ↥(↑f).domain} (hx : ↑x ∈ ArchimedeanClass.ball K c) {d : FiniteArchimedeanClass M} (hd : ↑d ≤ c) : (ofLex (↑↑f x)).coeff d = 0

For x within a ball of Archimedean class c, f.val x'coefficient at d vanishes for d ≤ c.

theorem HahnEmbedding.Partial.coeff_ne_zero {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : ↥(↑f).domain} (hx0 : ↑x ≠ 0) : (ofLex (↑↑f x)).coeff (FiniteArchimedeanClass.mk (↑x) hx0) ≠ 0

f.val x has a non-zero coefficient at the position of the Archimedean class of x.

theorem HahnEmbedding.Partial.coeff_eq_of_mem {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (x : M) {y z : ↥(↑f).domain} {c : ArchimedeanClass M} (hy : ↑y - x ∈ ArchimedeanClass.ball K c) (hz : ↑z - x ∈ ArchimedeanClass.ball K c) {d : FiniteArchimedeanClass M} (hd : ↑d ≤ c) : (ofLex (↑↑f y)).coeff d = (ofLex (↑↑f z)).coeff d

When y and z are both near x (the difference is in a ball), initial coefficients of f.val y and f.val z agree.

Step 3: extend the embedding

We create a larger HahnEmbedding.Partial from an existing one by adding a new element to the domain and assigning an appropriate output that preserves all HahnEmbedding.Partial's properties.

noncomputable def HahnEmbedding.Partial.evalCoeff {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) (x : M) (c : FiniteArchimedeanClass M) : R

Evaluate coefficients of the HahnSeries given an arbitrary input that's not necessarily in f's domain. The coefficient is picked from y that is "close enough" to x (their difference is in a higher ArchimedeanClass). If no such y exists (in other words, x is "isolated"), set the coefficient to 0.

This doesn't immediately extend f's domain to the entire module in a consistent way. Such extension isn't necessarily linear.

Equations

• f.evalCoeff x c = if h : ∃ (y : ↥(↑f).domain), ↑y - x ∈ ArchimedeanClass.ball K ↑c then (ofLex (↑↑f h.choose)).coeff c else 0

theorem HahnEmbedding.Partial.evalCoeff_eq {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : ↥(↑f).domain} (hy : ↑y - x ∈ ArchimedeanClass.ball K ↑c) : f.evalCoeff x c = (ofLex (↑↑f y)).coeff c

The coefficient is well-defined regardless of which y we pick in evalCoeff.

theorem HahnEmbedding.Partial.evalCoeff_eq_zero {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) {x : M} {c : FiniteArchimedeanClass M} (h : ¬∃ (y : ↥(↑f).domain), ↑y - x ∈ ArchimedeanClass.ball K ↑c) : f.evalCoeff x c = 0

theorem HahnEmbedding.Partial.isWF_support_evalCoeff {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (x : M) : (Function.support (f.evalCoeff x)).IsWF

noncomputable def HahnEmbedding.Partial.eval {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (x : M) : Lex (HahnSeries (FiniteArchimedeanClass M) R)

Promote HahnEmbedding.Partial.evalCoeff's output to a new HahnSeries.

Equations

• f.eval x = toLex { coeff := f.evalCoeff x, isPWO_support' := ⋯ }

@[simp]

theorem HahnEmbedding.Partial.eval_zero {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] : f.eval 0 = 0

theorem HahnEmbedding.Partial.eval_smul {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (k : K) (x : M) : f.eval (k • x) = k • f.eval x

theorem HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} {y : ↥(↑f).domain} (h : f.eval x = ↑↑f y) (z : ↥(↑f).domain) : ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (x - ↑y)

If f.eval x = f.val y, then for any z in the domain, x - z can't be closer than x - y in terms of Archimedean classes.

theorem HahnEmbedding.Partial.eval_ne {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) (y : ↥(↑f).domain) : f.eval x ≠ ↑↑f y

If x isn't in f's domain, f.eval x produces a brand new value not in f's range.

theorem HahnEmbedding.Partial.eval_eq_truncLT {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : ↥(↑f).domain} (hy : ArchimedeanClass.mk (↑y - x) = ↑c) (h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ArchimedeanClass.ball K ↑c) : f.eval x = toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑↑f y)))

If there is a y in f's domain with c = ArchimedeanClass (y - x), but there is no closer z to x where the difference is of a higher ArchimedeanClass, then f.eval x is simply f.val y truncated at c.

This doesn't mean every x can be evaluated this way: it is possible that one can find an infinite chain of y that keeps getting closer to x in terms of Archimedean classes, yet x is still isolated within a very high Archimedean class. In fact, in the next theorem, we will show that there is always such chain for x not in f's domain.

theorem HahnEmbedding.Partial.exists_sub_mem_ball {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) (y : ↥(↑f).domain) : ∃ (z : ↥(↑f).domain), ↑z - x ∈ ArchimedeanClass.ball K (ArchimedeanClass.mk (↑y - x))

For x not in f's domain, there is an infinite chain of y from f's domain that keeps getting closer to x in terms of Archimedean classes.

theorem HahnEmbedding.Partial.eval_lt {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) (y : ↥(↑f).domain) (h : x < ↑y) : f.eval x < ↑↑f y

For x not in f's domain, f.eval x is consistent with f's monotonicity.

noncomputable def HahnEmbedding.Partial.extendFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)

Extend f to a larger partial linear map by adding a new x.

Equations

• f.extendFun hx = (↑f).supSpanSingleton x (f.eval x) hx

theorem HahnEmbedding.Partial.extendFun_strictMono {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) : StrictMono ↑(f.extendFun hx)

theorem HahnEmbedding.Partial.baseEmbedding_le_extendFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) : seed.baseEmbedding ≤ f.extendFun hx

theorem HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) (c : FiniteArchimedeanClass M) : toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (f.eval x))) ∈ LinearMap.range (f.extendFun hx).toFun

theorem HahnEmbedding.Partial.truncLT_mem_range_extendFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) (y : ↥(f.extendFun hx).domain) (c : FiniteArchimedeanClass M) : toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) y))) ∈ LinearMap.range (f.extendFun hx).toFun

theorem HahnEmbedding.Partial.isPartial_extendFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) : IsPartial seed (f.extendFun hx)

noncomputable def HahnEmbedding.Partial.extend {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) : Partial seed

Promote HahnEmbedding.Partial.extendFun to a new HahnEmbedding.Partial.

Equations

• f.extend hx = ⟨f.extendFun hx, ⋯⟩

theorem HahnEmbedding.Partial.lt_extend {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} (f : Partial seed) [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ (↑f).domain) : f < f.extend hx

Step 4: use Zorn's lemma

We show that sSup makes sense on HahnEmbedding.Partial, which allows us to use Zorn's lemma to assert the existence of maximal embedding. Since we already show that we can create greater embeddings by adding new elements, the maximal embedding must have the maximal domain.

noncomputable def HahnEmbedding.Partial.sSupFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} {c : Set (Partial seed)} (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)

A partial linear map that contains every element in a directed set of HahnEmbedding.Partial.

Equations

• HahnEmbedding.Partial.sSupFun hc = LinearPMap.sSup ((fun (x : HahnEmbedding.Partial seed) => ↑x) '' c) ⋯

theorem HahnEmbedding.Partial.sSupFun_strictMono {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} [IsOrderedAddMonoid R] {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) : StrictMono ↑(sSupFun hc)

theorem HahnEmbedding.Partial.le_sSupFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} {c : Set (Partial seed)} (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) {f : Partial seed} (hf : f ∈ c) : ↑f ≤ sSupFun hc

theorem HahnEmbedding.Partial.baseEmbedding_le_sSupFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) : seed.baseEmbedding ≤ sSupFun hc

theorem HahnEmbedding.Partial.truncLT_mem_range_sSupFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) (x : ↥(sSupFun hc).domain) (c✝ : FiniteArchimedeanClass M) : toLex ((HahnSeries.truncLTLinearMap K c✝) (ofLex (↑(sSupFun hc) x))) ∈ LinearMap.range (sSupFun hc).toFun

theorem HahnEmbedding.Partial.isPartial_sSupFun {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} [IsOrderedAddMonoid R] {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) : IsPartial seed (sSupFun hc)

noncomputable def HahnEmbedding.Partial.sSup {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : Seed K M R} [IsOrderedAddMonoid R] {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : Partial seed) => x1 ≤ x2) c) : Partial seed

Promote HahnEmbedding.Partial.sSupFun to a HahnEmbedding.Partial.

Equations

• HahnEmbedding.Partial.sSup hnonempty hc = ⟨HahnEmbedding.Partial.sSupFun hc, ⋯⟩

theorem HahnEmbedding.Partial.exists_isMax {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) [IsOrderedAddMonoid R] : ∃ (f : Partial seed), IsMax f

theorem HahnEmbedding.Partial.exists_domain_eq_top {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] (seed : Seed K M R) [IsOrderedAddMonoid R] [Archimedean R] : ∃ (f : Partial seed), (↑f).domain = ⊤

There exists a HahnEmbedding.Partial whose domain is the whole module.

theorem hahnEmbedding_isOrderedModule {K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] [IsOrderedAddMonoid R] [Archimedean R] [h : Nonempty (HahnEmbedding.Seed K M R)] : ∃ (f : M →ₗ[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)), StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Hahn embedding theorem for an ordered module

There exists a strictly monotone M →ₗ[K] Lex (HahnSeries (FiniteArchimedeanClass M) R) that maps ArchimedeanClass M to HahnSeries.orderTop in the expected way, as long as HahnEmbedding.Seed K M R is nonempty. The HahnEmbedding.Partial with maximal domain is the desired embedding.