Ordered structures on localizations of commutative monoids #

source

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₂

source

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₁) ⋯ }

source

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₁) ⋯ }

source

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₂

source

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₁) ⋯ }

source

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₁) ⋯ }

source

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₁

source

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₁

source

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₁

source

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₁

source

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

PartialOrder (AddLocalization s)

Equations

AddLocalization.partialOrder = PartialOrder.mk ⋯

source

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

a < b ↔ a ≤ b ∧ ¬b ≤ a

source

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

a ≤ b → b ≤ a → a = b

source

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

a ≤ a

source

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

source

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

PartialOrder (Localization s)

Equations

Localization.partialOrder = PartialOrder.mk ⋯

source

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

source

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

OrderedCancelAddCommMonoid (AddLocalization s)

Equations

AddLocalization.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

source

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

source

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

OrderedCancelCommMonoid (Localization s)

Equations

Localization.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

source

instance AddLocalization.decidableLE {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} [DecidableRel fun (x x_1 : α) => x ≤ x_1] :

DecidableRel fun (x x_1 : AddLocalization s) => x ≤ x_1

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) ⋯

source

theorem AddLocalization.decidableLE.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : ↥s) (d : ↥s) :

Subsingleton (Decidable ((fun (x x_1 : AddLocalization s) => x ≤ x_1) (AddLocalization.mk a b) (AddLocalization.mk c d)))

source

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

DecidableRel fun (x x_1 : Localization s) => x ≤ x_1

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) ⋯

source

theorem AddLocalization.decidableLT.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : ↥s) (d : ↥s) :

Subsingleton (Decidable ((fun (x x_1 : AddLocalization s) => x < x_1) (AddLocalization.mk a b) (AddLocalization.mk c d)))

source

instance AddLocalization.decidableLT {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} [DecidableRel fun (x x_1 : α) => x < x_1] :

DecidableRel fun (x x_1 : AddLocalization s) => x < x_1

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) ⋯

source

instance Localization.decidableLT {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} [DecidableRel fun (x x_1 : α) => x < x_1] :

DecidableRel fun (x x_1 : Localization s) => x < x_1

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) ⋯

source

theorem AddLocalization.mkOrderEmbedding.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : ↥s) :

Function.Injective fun (a : α) => AddLocalization.mk a b

source

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

source

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

source

@[simp]

theorem Localization.mkOrderEmbedding_apply {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} (b : ↥s) (a : α) :

(Localization.mkOrderEmbedding b) a = (Localization.monoidOf s).mk' a b

source

@[simp]

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

(AddLocalization.mkOrderEmbedding b) a = (AddLocalization.addMonoidOf s).mk' a b

source

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

source

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_3 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} :

∀ (a b : AddLocalization s), max a b = max a b

source

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_4 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} :

∀ (a b : AddLocalization s), compare a b = compare a b

source

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} :

∀ (a b : AddLocalization s), min a b = min a b

source

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

LinearOrderedCancelAddCommMonoid (AddLocalization s)

Equations

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

source

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

a ≤ b ∨ b ≤ a

source

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

LinearOrderedCancelCommMonoid (Localization s)

Equations

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

Documentation

Mathlib.GroupTheory.MonoidLocalization.Order

Ordered structures on localizations of commutative monoids #