Ordered structures on localizations of commutative monoids

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₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) ⋯ }

theorem AddLocalization.le.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : { x : α // x ∈ s }} {b₂ : { x : α // x ∈ s }} {c₁ : α} {d₁ : α} {c₂ : { x : α // x ∈ s }} {d₂ : { x : α // x ∈ s }} (hab : (AddLocalization.r s) (a₁, a₂) (b₁, b₂)) (hcd : (AddLocalization.r s) (c₁, c₂) (d₁, d₂)) : (fun (a₁ : α) (a₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) a₁ a₂ c₁ c₂ = (fun (a₁ : α) (a₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) b₁ b₂ d₁ d₂

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₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ * a₁ ≤ ↑a₂ * b₁) ⋯ }

theorem AddLocalization.lt.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : { x : α // x ∈ s }} {b₂ : { x : α // x ∈ s }} {c₁ : α} {d₁ : α} {c₂ : { x : α // x ∈ s }} {d₂ : { x : α // x ∈ s }} (hab : (AddLocalization.r s) (a₁, a₂) (b₁, b₂)) (hcd : (AddLocalization.r s) (c₁, c₂) (d₁, d₂)) : (fun (a₁ : α) (a₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ + a₁ < ↑a₂ + b₁) a₁ a₂ c₁ c₂ = (fun (a₁ : α) (a₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ + a₁ < ↑a₂ + b₁) b₁ b₂ d₁ d₂

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₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ 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₂ : { x : α // x ∈ s }) (b₁ : α) (b₂ : { x : α // x ∈ s }) => ↑b₂ * a₁ < ↑a₂ * b₁) ⋯ }

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

theorem Localization.mk_le_mk {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} {a₁ : α} {b₁ : α} {a₂ : { x : α // x ∈ s }} {b₂ : { x : α // x ∈ 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₂ : { x : α // x ∈ s }} {b₂ : { x : α // x ∈ 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₂ : { x : α // x ∈ s }} {b₂ : { x : α // x ∈ s }} : Localization.mk a₁ a₂ < Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁

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

Equations

• AddLocalization.partialOrder = PartialOrder.mk ⋯

theorem AddLocalization.partialOrder.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) (c : AddLocalization s) : a ≤ b → b ≤ c → a ≤ c

theorem AddLocalization.partialOrder.proof_4 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a ≤ b → b ≤ a → a = b

theorem AddLocalization.partialOrder.proof_3 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem AddLocalization.partialOrder.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) : a ≤ a

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

Equations

• Localization.partialOrder = PartialOrder.mk ⋯

theorem AddLocalization.orderedAddCancelCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a ≤ b → ∀ (c : AddLocalization s), c + a ≤ c + b

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

Equations

• AddLocalization.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

theorem AddLocalization.orderedAddCancelCommMonoid.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) (c : AddLocalization s) : a + b ≤ a + c → b ≤ c

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

Equations

• Localization.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

theorem AddLocalization.decidableLE.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : { x : α // x ∈ s }) (d : { x : α // x ∈ s }) : Subsingleton (Decidable ((fun (x1 x2 : AddLocalization s) => x1 ≤ x2) (AddLocalization.mk a b) (AddLocalization.mk c d)))

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 : { x : α // x ∈ s }) => decidable_of_iff' (↑x_3 + x ≤ ↑x_2 + x_1) ⋯

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 : { x : α // x ∈ s }) => decidable_of_iff' (↑x_3 * x ≤ ↑x_2 * x_1) ⋯

theorem AddLocalization.decidableLT.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : { x : α // x ∈ s }) (d : { x : α // x ∈ s }) : Subsingleton (Decidable ((fun (x1 x2 : AddLocalization s) => x1 < x2) (AddLocalization.mk a b) (AddLocalization.mk c d)))

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 : { x : α // x ∈ 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 : { x : α // x ∈ s }) => decidable_of_iff' (↑x_3 * x < ↑x_2 * x_1) ⋯

def AddLocalization.mkOrderEmbedding {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : { x : α // x ∈ 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' := ⋯ }

theorem AddLocalization.mkOrderEmbedding.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : { x : α // x ∈ s }) : Function.Injective fun (a : α) => AddLocalization.mk a b

theorem AddLocalization.mkOrderEmbedding.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : { x : α // x ∈ s }) {a : α} {b : α} : AddLocalization.mk a b✝ ≤ AddLocalization.mk b b✝ ↔ a ≤ b

@[simp]

theorem Localization.mkOrderEmbedding_apply {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} (b : { x : α // x ∈ s }) (a : α) : (Localization.mkOrderEmbedding b) a = (Localization.monoidOf s).mk' a b

@[simp]

theorem AddLocalization.mkOrderEmbedding_apply {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : { x : α // x ∈ s }) (a : α) : (AddLocalization.mkOrderEmbedding b) a = (AddLocalization.addMonoidOf s).mk' a b

def Localization.mkOrderEmbedding {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} (b : { x : α // x ∈ 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' := ⋯ }

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

Equations

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

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a ≤ b ∨ b ≤ a

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_4 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : ∀ (a b : AddLocalization s), compare a b = compare a b

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : ∀ (a b : AddLocalization s), min a b = min a b

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_3 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : ∀ (a b : AddLocalization s), max a b = max 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 ⋯ ⋯ ⋯