Documentation

Mathlib.GroupTheory.MonoidLocalization.Order

Ordered structures on localizations of commutative monoids #

Equations
  • AddLocalization.le = { le := fun (a b : AddLocalization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ + a₁ a₂ + b₁) }
theorem AddLocalization.le.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : s} {b₂ : s} {c₁ : α} {d₁ : α} {c₂ : s} {d₂ : s} (hab : (AddLocalization.r s) (a₁, a₂) (b₁, b₂)) (hcd : (AddLocalization.r s) (c₁, c₂) (d₁, d₂)) :
(fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ + a₁ a₂ + b₁) a₁ a₂ c₁ c₂ = (fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ + a₁ a₂ + b₁) b₁ b₂ d₁ d₂
instance Localization.le {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} :
Equations
  • Localization.le = { le := fun (a b : Localization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ * a₁ a₂ * b₁) }
theorem AddLocalization.lt.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : s} {b₂ : s} {c₁ : α} {d₁ : α} {c₂ : s} {d₂ : s} (hab : (AddLocalization.r s) (a₁, a₂) (b₁, b₂)) (hcd : (AddLocalization.r s) (c₁, c₂) (d₁, d₂)) :
(fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ + a₁ < a₂ + b₁) a₁ a₂ c₁ c₂ = (fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ + a₁ < a₂ + b₁) b₁ b₂ d₁ d₂
Equations
  • AddLocalization.lt = { lt := 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 α} :
Equations
  • Localization.lt = { lt := fun (a b : Localization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : s) (b₁ : α) (b₂ : s) => b₂ * a₁ < a₂ * b₁) }
theorem AddLocalization.mk_le_mk {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : s} {b₂ : 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₂ : s} {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₂ : s} {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₂ : s} {b₂ : s} :
Localization.mk a₁ a₂ < Localization.mk b₁ b₂ b₂ * a₁ < a₂ * b₁
Equations
Equations
Equations
theorem AddLocalization.decidableLE.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : s) (d : s) :
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.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)
theorem AddLocalization.decidableLT.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : s) (d : s) :
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)
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)

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

Equations
Instances For
    theorem AddLocalization.mkOrderEmbedding.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : s) {a : α} {b : α} :
    @[simp]

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

    Equations
    Instances For
      Equations
      • AddLocalization.instLinearOrderedAddCancelCommMonoid = LinearOrderedCancelAddCommMonoid.mk AddLocalization.decidableLE AddLocalization.decidableEq AddLocalization.decidableLT
      Equations
      • Localization.instLinearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk Localization.decidableLE Localization.decidableEq Localization.decidableLT