Ordered structures on localizations of commutative monoids

@[instance_reducible]

instance Localization.le {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LE (Localization s)

Equations

• Localization.le = { le := fun (a b : Localization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ * a₁ ≤ ↑a₂ * b₁) ⋯ }

@[instance_reducible]

instance AddLocalization.le {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : LE (AddLocalization s)

Equations

• AddLocalization.le = { le := fun (a b : AddLocalization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) ⋯ }

@[instance_reducible]

instance Localization.lt {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LT (Localization s)

Equations

• Localization.lt = { lt := fun (a b : Localization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ * a₁ < ↑a₂ * b₁) ⋯ }

@[instance_reducible]

instance AddLocalization.lt {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : LT (AddLocalization s)

Equations

• AddLocalization.lt = { lt := fun (a b : AddLocalization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ < ↑a₂ + b₁) ⋯ }

theorem Localization.mk_le_mk {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : mk a₁ a₂ ≤ mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁

theorem AddLocalization.mk_le_mk {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : mk a₁ a₂ ≤ mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁

theorem Localization.mk_lt_mk {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : mk a₁ a₂ < mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁

theorem AddLocalization.mk_lt_mk {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : mk a₁ a₂ < mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁

@[instance_reducible]

instance Localization.partialOrder {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : PartialOrder (Localization s)

Equations

• Localization.partialOrder = { toLE := Localization.le, toLT := Localization.lt, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[instance_reducible]

instance AddLocalization.partialOrder {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : PartialOrder (AddLocalization s)

Equations

• AddLocalization.partialOrder = { toLE := AddLocalization.le, toLT := AddLocalization.lt, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

instance Localization.isOrderedCancelMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : IsOrderedCancelMonoid (Localization s)

instance AddLocalization.isOrderedAddCancelMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : IsOrderedCancelAddMonoid (AddLocalization s)

@[instance_reducible]

instance Localization.decidableLE {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} [DecidableLE α] : DecidableLE (Localization s)

Equations

• a.decidableLE b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 * x ≤ ↑x_2 * x_1) ⋯

@[instance_reducible]

instance AddLocalization.decidableLE {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} [DecidableLE α] : DecidableLE (AddLocalization s)

Equations

• a.decidableLE b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 + x ≤ ↑x_2 + x_1) ⋯

@[instance_reducible]

instance Localization.decidableLT {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} [DecidableLT α] : DecidableLT (Localization s)

Equations

• a.decidableLT b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 * x < ↑x_2 * x_1) ⋯

@[instance_reducible]

instance AddLocalization.decidableLT {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} [DecidableLT α] : DecidableLT (AddLocalization s)

Equations

• a.decidableLT b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 + x < ↑x_2 + x_1) ⋯

def Localization.mkOrderEmbedding {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} (b : ↥s) : α ↪o Localization s

An ordered cancellative monoid injects into its localization by sending a to a / b.

Equations

• Localization.mkOrderEmbedding b = { toFun := fun (a : α) => Localization.mk a b, inj' := ⋯, map_rel_iff' := ⋯ }

def AddLocalization.mkOrderEmbedding {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} (b : ↥s) : α ↪o AddLocalization s

An ordered cancellative monoid injects into its localization by sending a to a - b.

Equations

• AddLocalization.mkOrderEmbedding b = { toFun := fun (a : α) => AddLocalization.mk a b, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem AddLocalization.mkOrderEmbedding_apply {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} (b : ↥s) (a : α) : (mkOrderEmbedding b) a = mk a b

@[simp]

theorem Localization.mkOrderEmbedding_apply {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} (b : ↥s) (a : α) : (mkOrderEmbedding b) a = mk a b

@[instance_reducible]

instance Localization.instLinearOrderOfIsOrderedCancelMonoid {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LinearOrder (Localization s)

Equations

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

@[instance_reducible]

instance AddLocalization.instLinearAddOrderOfIsOrderedAddCancelMonoid {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : LinearOrder (AddLocalization s)

Equations

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