Ordered structures on localizations of commutative monoids

instance Localization.le {α : Type u_1} [OrderedCancelCommMonoid α] {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 AddLocalization.le {α : Type u_1} [OrderedCancelAddCommMonoid α] {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 Localization.lt {α : Type u_1} [OrderedCancelCommMonoid α] {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 AddLocalization.lt {α : Type u_1} [OrderedCancelAddCommMonoid α] {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} [OrderedCancelCommMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : Localization.mk a₁ a₂ ≤ Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁

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

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

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

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

Equations

• Localization.partialOrder = PartialOrder.mk ⋯

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

Equations

• AddLocalization.partialOrder = PartialOrder.mk ⋯

instance Localization.orderedCancelCommMonoid {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} : OrderedCancelCommMonoid (Localization s)

Equations

• Localization.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

instance AddLocalization.orderedAddCancelCommMonoid {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : OrderedCancelAddCommMonoid (AddLocalization s)

Equations

• AddLocalization.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Localization.decidableLE {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : DecidableRel fun (x1 x2 : Localization s) => x1 ≤ x2

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 AddLocalization.decidableLE {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : DecidableRel fun (x1 x2 : AddLocalization s) => x1 ≤ x2

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 Localization.decidableLT {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} [DecidableRel fun (x1 x2 : α) => x1 < x2] : DecidableRel fun (x1 x2 : Localization s) => x1 < x2

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 AddLocalization.decidableLT {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} [DecidableRel fun (x1 x2 : α) => x1 < x2] : DecidableRel fun (x1 x2 : AddLocalization s) => x1 < x2

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} [OrderedCancelCommMonoid α] {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} [OrderedCancelAddCommMonoid α] {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 Localization.mkOrderEmbedding_apply {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} (b : ↥s) (a : α) : (Localization.mkOrderEmbedding b) a = Localization.mk a b

@[simp]

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

instance Localization.instLinearOrderedCancelCommMonoid {α : Type u_1} [LinearOrderedCancelCommMonoid α] {s : Submonoid α} : LinearOrderedCancelCommMonoid (Localization s)

Equations

• Localization.instLinearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ Localization.decidableLE Localization.decidableEq Localization.decidableLT ⋯ ⋯ ⋯

instance AddLocalization.instLinearOrderedAddCancelCommMonoid {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : LinearOrderedCancelAddCommMonoid (AddLocalization s)

Equations

• AddLocalization.instLinearOrderedAddCancelCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ AddLocalization.decidableLE AddLocalization.decidableEq AddLocalization.decidableLT ⋯ ⋯ ⋯