Mathlib.Algebra.Order.Monoid.Basic

Module docstring

{"# Ordered monoids

This file develops some additional material on ordered monoids. "}

Function.Injective.isOrderedMonoid theorem

 [IsOrderedMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1)
  (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
  let _ : CommMonoid β := hf.commMonoid f one mul npow
  let _ : PartialOrder β := PartialOrder.lift f hf
  IsOrderedMonoid β

Full source

/-- Pullback an `IsOrderedMonoid` under an injective map. -/
@[to_additive "Pullback an `IsOrderedAddMonoid` under an injective map."]
lemma Function.Injective.isOrderedMonoid [IsOrderedMonoid α] [One β] [Mul β]
    [Pow β ℕ] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    let _ : CommMonoid β := hf.commMonoid f one mul npow
    let _ : PartialOrder β := PartialOrder.lift f hf
    IsOrderedMonoid β :=
  let _ : CommMonoid β := hf.commMonoid f one mul npow
  let _ : PartialOrder β := PartialOrder.lift f hf
  { mul_le_mul_left a b ab c := show f (c * a) ≤ f (c * b) by
      rw [mul, mul]; apply mul_le_mul_left'; exact ab }

Pullback of Ordered Monoid Structure via Injective Homomorphism

Informal description

Let $\alpha$ be an ordered monoid and $\beta$ be a type equipped with operations for one, multiplication, and exponentiation by natural numbers. Given an injective function $f \colon \beta \to \alpha$ such that: - $f(1) = 1$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in \beta$, - $f(x^n) = f(x)^n$ for all $x \in \beta$ and $n \in \mathbb{N}$, then $\beta$ can be endowed with the structure of an ordered monoid, where the partial order on $\beta$ is defined by lifting the order from $\alpha$ via $f$.

Function.Injective.isOrderedCancelMonoid theorem

 [IsOrderedCancelMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1)
  (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
  let _ : CommMonoid β := hf.commMonoid f one mul npow
  let _ : PartialOrder β := PartialOrder.lift f hf
  IsOrderedCancelMonoid β

Full source

/-- Pullback an `IsOrderedCancelMonoid` under an injective map. -/
@[to_additive Function.Injective.isOrderedCancelAddMonoid
    "Pullback an `IsOrderedCancelAddMonoid` under an injective map."]
lemma Function.Injective.isOrderedCancelMonoid [IsOrderedCancelMonoid α] [One β] [Mul β]
    [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    let _ : CommMonoid β := hf.commMonoid f one mul npow
    let _ : PartialOrder β := PartialOrder.lift f hf
    IsOrderedCancelMonoid β :=
  let _ : CommMonoid β := hf.commMonoid f one mul npow
  let _ : PartialOrder β := PartialOrder.lift f hf
  { __ := hf.isOrderedMonoid f one mul npow
    le_of_mul_le_mul_left a b c (bc : f (a * b) ≤ f (a * c)) :=
      (mul_le_mul_iff_left (f a)).1 (by rwa [← mul, ← mul]) }

Pullback of Ordered Cancellative Monoid Structure via Injective Homomorphism

Informal description

Let $\alpha$ be an ordered cancellative monoid and $\beta$ be a type equipped with operations for one, multiplication, and exponentiation by natural numbers. Given an injective function $f \colon \beta \to \alpha$ such that: - $f(1) = 1$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in \beta$, - $f(x^n) = f(x)^n$ for all $x \in \beta$ and $n \in \mathbb{N}$, then $\beta$ can be endowed with the structure of an ordered cancellative monoid, where the partial order on $\beta$ is defined by lifting the order from $\alpha$ via $f$.

OrderEmbedding.mulLeft definition

{α : Type*} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m : α) : α ↪o α

Full source

/-- The order embedding sending `b` to `a * b`, for some fixed `a`.
See also `OrderIso.mulLeft` when working in an ordered group. -/
@[to_additive (attr := simps!)
      "The order embedding sending `b` to `a + b`, for some fixed `a`.
       See also `OrderIso.addLeft` when working in an additive ordered group."]
def OrderEmbedding.mulLeft {α : Type*} [Mul α] [LinearOrder α]
    [MulLeftStrictMono α] (m : α) : α ↪o α :=
  OrderEmbedding.ofStrictMono (fun n => m * n) fun _ _ w => mul_lt_mul_left' w m

Left multiplication order embedding

Informal description

For a fixed element $a$ in a linearly ordered monoid $\alpha$ where left multiplication by $a$ is strictly monotone, the function $x \mapsto a \cdot x$ defines an order embedding from $\alpha$ to itself. This means the function is injective and preserves the order relation: for any $x, y \in \alpha$, $x \leq y$ if and only if $a \cdot x \leq a \cdot y$.

OrderEmbedding.mulRight definition

{α : Type*} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m : α) : α ↪o α

Full source

/-- The order embedding sending `b` to `b * a`, for some fixed `a`.
See also `OrderIso.mulRight` when working in an ordered group. -/
@[to_additive (attr := simps!)
      "The order embedding sending `b` to `b + a`, for some fixed `a`.
       See also `OrderIso.addRight` when working in an additive ordered group."]
def OrderEmbedding.mulRight {α : Type*} [Mul α] [LinearOrder α]
    [MulRightStrictMono α] (m : α) : α ↪o α :=
  OrderEmbedding.ofStrictMono (fun n => n * m) fun _ _ w => mul_lt_mul_right' w m

Order embedding induced by right multiplication

Informal description

For a fixed element $m$ in a linearly ordered multiplicative monoid $\alpha$ where right multiplication by $m$ is strictly monotone, the function $x \mapsto x \cdot m$ defines an order embedding from $\alpha$ to itself. This means the function is injective and preserves the order relation: for any $x, y \in \alpha$, $x \leq y$ if and only if $x \cdot m \leq y \cdot m$.