Ordered monoids #
This file develops some additional material on ordered monoids.
theorem
Function.Injective.isOrderedMonoid
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Pullback an IsOrderedMonoid under an injective map.
theorem
Function.Injective.isOrderedAddMonoid
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Pullback an IsOrderedAddMonoid under an injective map.
theorem
Function.Injective.isOrderedCancelMonoid
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedCancelMonoid β
Pullback an IsOrderedCancelMonoid under an injective map.
theorem
Function.Injective.isOrderedCancelAddMonoid
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedCancelAddMonoid β
Pullback an IsOrderedCancelAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedCommMonoid
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Alias of Function.Injective.isOrderedMonoid.
Pullback an IsOrderedMonoid under an injective map.
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedAddCommMonoid
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Alias of Function.Injective.isOrderedAddMonoid.
Pullback an IsOrderedAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedCancelMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedCancelCommMonoid
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedCancelMonoid β
Alias of Function.Injective.isOrderedCancelMonoid.
Pullback an IsOrderedCancelMonoid under an injective map.
@[deprecated Function.Injective.isOrderedCancelAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedCancelAddCommMonoid
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedCancelAddMonoid β
Alias of Function.Injective.isOrderedCancelAddMonoid.
Pullback an IsOrderedCancelAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedCommMonoid
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Alias of Function.Injective.isOrderedMonoid.
Pullback an IsOrderedMonoid under an injective map.
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedAddCommMonoid
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Alias of Function.Injective.isOrderedAddMonoid.
Pullback an IsOrderedAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedCancelMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedCancelCommMonoid
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedCancelMonoid β
Alias of Function.Injective.isOrderedCancelMonoid.
Pullback an IsOrderedCancelMonoid under an injective map.
@[deprecated Function.Injective.isOrderedCancelAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedCancelAddCommMonoid
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedCancelAddMonoid β
Alias of Function.Injective.isOrderedCancelAddMonoid.
Pullback an IsOrderedCancelAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedCommGroup
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Alias of Function.Injective.isOrderedMonoid.
Pullback an IsOrderedMonoid under an injective map.
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.orderedAddCommGroup
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Alias of Function.Injective.isOrderedAddMonoid.
Pullback an IsOrderedAddMonoid under an injective map.
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedCommGroup
{α : Type u}
{β : Type u_1}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[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 x := Injective.commMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedMonoid β
Alias of Function.Injective.isOrderedMonoid.
Pullback an IsOrderedMonoid under an injective map.
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem
Function.Injective.linearOrderedAddCommGroup
{α : Type u}
{β : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Zero β]
[Add β]
[SMul ℕ β]
(f : β → α)
(hf : Injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
:
let x := Injective.addCommMonoid f hf one mul npow;
let x_1 := PartialOrder.lift f hf;
IsOrderedAddMonoid β
Alias of Function.Injective.isOrderedAddMonoid.
Pullback an IsOrderedAddMonoid under an injective map.
The order embedding sending b to a * b, for some fixed a.
See also OrderIso.mulLeft when working in an ordered group.
Equations
- OrderEmbedding.mulLeft m = OrderEmbedding.ofStrictMono (fun (n : α) => m * n) ⋯
Instances For
The order embedding sending b to a + b, for some fixed a.
See also OrderIso.addLeft when working in an additive ordered group.
Equations
- OrderEmbedding.addLeft m = OrderEmbedding.ofStrictMono (fun (n : α) => m + n) ⋯
Instances For
@[simp]
theorem
OrderEmbedding.mulLeft_apply
{α : Type u_2}
[Mul α]
[LinearOrder α]
[MulLeftStrictMono α]
(m n : α)
:
@[simp]
theorem
OrderEmbedding.addLeft_apply
{α : Type u_2}
[Add α]
[LinearOrder α]
[AddLeftStrictMono α]
(m n : α)
:
The order embedding sending b to b * a, for some fixed a.
See also OrderIso.mulRight when working in an ordered group.
Equations
- OrderEmbedding.mulRight m = OrderEmbedding.ofStrictMono (fun (n : α) => n * m) ⋯
Instances For
The order embedding sending b to b + a, for some fixed a.
See also OrderIso.addRight when working in an additive ordered group.
Equations
- OrderEmbedding.addRight m = OrderEmbedding.ofStrictMono (fun (n : α) => n + m) ⋯
Instances For
@[simp]
theorem
OrderEmbedding.mulRight_apply
{α : Type u_2}
[Mul α]
[LinearOrder α]
[MulRightStrictMono α]
(m n : α)
:
@[simp]
theorem
OrderEmbedding.addRight_apply
{α : Type u_2}
[Add α]
[LinearOrder α]
[AddRightStrictMono α]
(m n : α)
: