Lexicographical order on Hahn series

In this file, we define lexicographical ordered Lex R⟦Γ⟧, and show this is a LinearOrder when Γ and R themselves are linearly ordered. Additionally, it is an ordered group when R is.

Main definitions

• HahnSeries.finiteArchimedeanClassOrderIsoLex: FiniteArchimedeanClass of Lex R⟦Γ⟧ can be decomposed by Γ.

instance HahnSeries.instPartialOrderLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [PartialOrder R] : PartialOrder (Lex (HahnSeries Γ R))

Equations

• HahnSeries.instPartialOrderLex = PartialOrder.lift (fun (x : Lex (HahnSeries Γ R)) => toLex (ofLex x).coeff) ⋯

theorem HahnSeries.lt_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [PartialOrder R] (a b : Lex (HahnSeries Γ R)) : a < b ↔ ∃ (i : Γ), (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i

noncomputable instance HahnSeries.instLinearOrderLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] : LinearOrder (Lex (HahnSeries Γ R))

Equations

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

@[simp]

theorem HahnSeries.leadingCoeff_pos_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : 0 < (ofLex x).leadingCoeff ↔ 0 < x

theorem HahnSeries.leadingCoeff_nonneg_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : 0 ≤ (ofLex x).leadingCoeff ↔ 0 ≤ x

theorem HahnSeries.leadingCoeff_neg_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : (ofLex x).leadingCoeff < 0 ↔ x < 0

theorem HahnSeries.leadingCoeff_nonpos_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Zero R] [LinearOrder R] {x : Lex (HahnSeries Γ R)} : (ofLex x).leadingCoeff ≤ 0 ↔ x ≤ 0

instance HahnSeries.instIsOrderedAddMonoidLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] [AddCommMonoid R] [AddLeftStrictMono R] : IsOrderedAddMonoid (Lex (HahnSeries Γ R))

@[simp]

theorem HahnSeries.support_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).support = (ofLex x).support

@[simp]

theorem HahnSeries.orderTop_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).orderTop = (ofLex x).orderTop

theorem HahnSeries.order_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Zero Γ] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).order = (ofLex x).order

theorem HahnSeries.leadingCoeff_abs {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

theorem HahnSeries.abs_lt_abs_of_orderTop_ofLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)} (h : (ofLex y).orderTop < (ofLex x).orderTop) : |x| < |y|

theorem HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)} (h : (ofLex x).orderTop = (ofLex y).orderTop) : ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

theorem HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)} : ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ (ofLex x).orderTop < (ofLex y).orderTop ∨ (ofLex x).orderTop = (ofLex y).orderTop ∧ ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

theorem HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)} : ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔ (ofLex x).orderTop = (ofLex y).orderTop ∧ ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff

noncomputable def HahnSeries.finiteArchimedeanClassOrderHomLex (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] : FiniteArchimedeanClass (Lex (HahnSeries Γ R)) →o Lex (Γ × FiniteArchimedeanClass R)

Finite archimedean classes of Lex R⟦Γ⟧ decompose into lexicographical pairs of order and the finite archimedean class of leadingCoeff.

Equations

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

noncomputable def HahnSeries.finiteArchimedeanClassOrderHomInvLex (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] : Lex (Γ × FiniteArchimedeanClass R) →o FiniteArchimedeanClass (Lex (HahnSeries Γ R))

The inverse of finiteArchimedeanClassOrderHomLex.

Equations

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

noncomputable def HahnSeries.finiteArchimedeanClassOrderIsoLex (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] : FiniteArchimedeanClass (Lex (HahnSeries Γ R)) ≃o Lex (Γ × FiniteArchimedeanClass R)

The correspondence between finite archimedean classes of Lex R⟦Γ⟧ and lexicographical pairs of HahnSeries.orderTop and the finite archimedean class of HahnSeries.leadingCoeff.

Equations

• HahnSeries.finiteArchimedeanClassOrderIsoLex Γ R = OrderIso.ofHomInv (HahnSeries.finiteArchimedeanClassOrderHomLex Γ R) (HahnSeries.finiteArchimedeanClassOrderHomInvLex Γ R) ⋯ ⋯

@[simp]

theorem HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] {x : Lex (HahnSeries Γ R)} (h : x ≠ 0) : ↑(ofLex ((finiteArchimedeanClassOrderIsoLex Γ R) (FiniteArchimedeanClass.mk x h))).1 = (ofLex x).orderTop

@[simp]

theorem HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] {x : Lex (HahnSeries Γ R)} (h : x ≠ 0) : ↑(ofLex ((finiteArchimedeanClassOrderIsoLex Γ R) (FiniteArchimedeanClass.mk x h))).2 = ArchimedeanClass.mk (ofLex x).leadingCoeff

noncomputable def HahnSeries.finiteArchimedeanClassOrderIso (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] : FiniteArchimedeanClass (Lex (HahnSeries Γ R)) ≃o Γ

For Archimedean coefficients, there is a correspondence between finite archimedean classes and HahnSeries.orderTop without the top element.

Equations

• HahnSeries.finiteArchimedeanClassOrderIso Γ R = (HahnSeries.finiteArchimedeanClassOrderIsoLex Γ R).trans (Prod.Lex.prodUnique Γ (FiniteArchimedeanClass R))

@[simp]

theorem HahnSeries.finiteArchimedeanClassOrderIso_apply {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] {x : Lex (HahnSeries Γ R)} (h : x ≠ 0) : ↑((finiteArchimedeanClassOrderIso Γ R) (FiniteArchimedeanClass.mk x h)) = (ofLex x).orderTop

noncomputable def HahnSeries.archimedeanClassOrderIsoWithTop (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] : ArchimedeanClass (Lex (HahnSeries Γ R)) ≃o WithTop Γ

For Archimedean coefficients, there is a correspondence between archimedean classes (with top) and HahnSeries.orderTop.

Equations

• HahnSeries.archimedeanClassOrderIsoWithTop Γ R = (FiniteArchimedeanClass.withTopOrderIso (Lex (HahnSeries Γ R))).symm.trans (HahnSeries.finiteArchimedeanClassOrderIso Γ R).withTopCongr

@[simp]

theorem HahnSeries.archimedeanClassOrderIsoWithTop_apply {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] (x : Lex (HahnSeries Γ R)) : (archimedeanClassOrderIsoWithTop Γ R) (ArchimedeanClass.mk x) = (ofLex x).orderTop

noncomputable def HahnSeries.embDomainOrderEmbedding {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] {Γ' : Type u_3} [LinearOrder Γ'] (f : Γ ↪o Γ') [Zero R] : Lex (HahnSeries Γ R) ↪o Lex (HahnSeries Γ' R)

HahnSeries.embDomain as an OrderEmbedding.

Equations

• HahnSeries.embDomainOrderEmbedding f = { toFun := fun (a : Lex (HahnSeries Γ R)) => toLex (HahnSeries.embDomain f (ofLex a)), inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem HahnSeries.embDomainOrderEmbedding_apply {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] {Γ' : Type u_3} [LinearOrder Γ'] (f : Γ ↪o Γ') [Zero R] (a : Lex (HahnSeries Γ R)) : (embDomainOrderEmbedding f) a = toLex (embDomain f (ofLex a))

noncomputable def HahnSeries.embDomainOrderAddMonoidHom {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] {Γ' : Type u_3} [LinearOrder Γ'] (f : Γ ↪o Γ') [AddMonoid R] : Lex (HahnSeries Γ R) →+o Lex (HahnSeries Γ' R)

HahnSeries.embDomain as an OrderAddMonoidHom.

Equations

• HahnSeries.embDomainOrderAddMonoidHom f = { toFun := (HahnSeries.embDomainOrderEmbedding f).toOrderHom.toFun, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

@[simp]

theorem HahnSeries.embDomainOrderAddMonoidHom_apply {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] {Γ' : Type u_3} [LinearOrder Γ'] (f : Γ ↪o Γ') [AddMonoid R] (a✝ : Lex (HahnSeries Γ R)) : (embDomainOrderAddMonoidHom f) a✝ = (embDomainOrderEmbedding f).toOrderHom.toFun a✝

theorem HahnSeries.embDomainOrderAddMonoidHom_injective {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [PartialOrder R] {Γ' : Type u_3} [LinearOrder Γ'] (f : Γ ↪o Γ') [AddMonoid R] : Function.Injective ⇑(embDomainOrderAddMonoidHom f)