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 or ring whenever 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))

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))

@[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

@[simp]

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

@[simp]

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

@[simp]

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.

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.

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.

@[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.

@[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.

@[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

instance HahnSeries.instIsOrderedRingLexOfNoZeroDivisors {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [Ring R] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [IsOrderedRing R] [NoZeroDivisors R] : IsOrderedRing (Lex (HahnSeries Γ R))

instance HahnSeries.instIsStrictOrderedRingLexOfIsDomain {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LinearOrder R] [Ring R] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [IsDomain R] [IsStrictOrderedRing R] : IsStrictOrderedRing (Lex (HahnSeries Γ R))

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.

@[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.

@[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)