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₂ : ↥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₂))
:
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₁) ⋯ }
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₂))
:
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₁) ⋯ }
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₁) ⋯ }
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₁
instance
AddLocalization.partialOrder
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
:
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)
:
theorem
AddLocalization.partialOrder.proof_4
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(a : AddLocalization s)
(b : AddLocalization s)
:
theorem
AddLocalization.partialOrder.proof_3
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(a : AddLocalization s)
(b : AddLocalization s)
:
theorem
AddLocalization.partialOrder.proof_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(a : AddLocalization s)
:
a ≤ a
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 α}
:
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)
:
instance
Localization.orderedCancelCommMonoid
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Submonoid α}
:
Equations
- Localization.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯
theorem
AddLocalization.decidableLE.proof_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(a : α)
(c : α)
(b : ↥s)
(d : ↥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 : ↥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)
:
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 : ↥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) ⋯
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' := ⋯ }
Instances For
theorem
AddLocalization.mkOrderEmbedding.proof_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(b : ↥s)
:
Function.Injective fun (a : α) => AddLocalization.mk a b
theorem
AddLocalization.mkOrderEmbedding.proof_2
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(b : ↥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 : ↥s)
(a : α)
:
(Localization.mkOrderEmbedding b) a = (Localization.monoidOf s).mk' a b
@[simp]
theorem
AddLocalization.mkOrderEmbedding_apply
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
(b : ↥s)
(a : α)
:
(AddLocalization.mkOrderEmbedding b) a = (AddLocalization.addMonoidOf s).mk' a b
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' := ⋯ }
Instances For
instance
AddLocalization.instLinearOrderedAddCancelCommMonoid
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
{s : AddSubmonoid α}
:
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)
:
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 α}
:
Equations
- Localization.instLinearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ Localization.decidableLE Localization.decidableEq Localization.decidableLT ⋯ ⋯ ⋯