Ordered scalar multiplication and vector addition

This file defines ordered scalar multiplication and vector addition, and proves some properties. In the additive case, a motivating example is given by the additive action of ℤ on subsets of reals that are closed under integer translation. The order compatibility allows for a treatment of the R((z))-module structure on (z ^ s) V((z)) for an R-module V, using the formalism of Hahn series. In the multiplicative case, a standard example is the action of non-negative rationals on an ordered field.

Implementation notes

• Because these classes mix the algebra and order hierarchies, we write them as Prop-valued mixins.
• Despite the file name, Ordered AddTorsors are not defined as a separate class. To implement them, combine [AddTorsor G P] with [IsOrderedCancelVAdd G P]

Definitions

• IsOrderedSMul : inequalities are preserved by scalar multiplication.
• IsOrderedVAdd : inequalities are preserved by translation.
• IsCancelSMul : the scalar multiplication version of cancellative multiplication
• IsCancelVAdd : the vector addition version of cancellative addition
• IsOrderedCancelSMul : inequalities are preserved and reflected by scalar multiplication.
• IsOrderedCancelVAdd : inequalities are preserved and reflected by translation.

Instances

• OrderedCommMonoid.toIsOrderedSMul
• OrderedAddCommMonoid.toIsOrderedVAdd
• IsOrderedSMul.toCovariantClassLeft
• IsOrderedVAdd.toCovariantClassLeft
• IsOrderedCancelSMul.toCancelSMul
• IsOrderedCancelVAdd.toCancelVAdd
• OrderedCancelCommMonoid.toIsOrderedCancelSMul
• OrderedCancelAddCommMonoid.toIsOrderedCancelVAdd
• IsOrderedCancelSMul.toContravariantClassLeft
• IsOrderedCancelVAdd.toContravariantClassLeft

TODO

• (lex) prod instances
• Pi instances
• WithTop (in a different file?)

class IsOrderedVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] : Prop

An ordered vector addition is a bi-monotone vector addition.

• vadd_le_vadd_left : ∀ (a b : P), a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b
• vadd_le_vadd_right : ∀ (c d : G), c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a

theorem IsOrderedVAdd.vadd_le_vadd_left {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : IsOrderedVAdd G P] (a : P) (b : P) : a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b

theorem IsOrderedVAdd.vadd_le_vadd_right {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : IsOrderedVAdd G P] (c : G) (d : G) : c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a

@[deprecated IsOrderedVAdd]

def OrderedVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] : Prop

Alias of IsOrderedVAdd.

---

An ordered vector addition is a bi-monotone vector addition.

Equations

• OrderedVAdd = IsOrderedVAdd

class IsOrderedSMul (G : Type u_3) (P : Type u_4) [LE G] [LE P] [SMul G P] : Prop

An ordered scalar multiplication is a bi-monotone scalar multiplication. Note that this is different from OrderedSMul, which uses strict inequality, requires G to be a semiring, and the defining conditions are restricted to positive elements of G.

• smul_le_smul_left : ∀ (a b : P), a ≤ b → ∀ (c : G), c • a ≤ c • b
• smul_le_smul_right : ∀ (c d : G), c ≤ d → ∀ (a : P), c • a ≤ d • a

theorem IsOrderedSMul.smul_le_smul_left {G : Type u_3} {P : Type u_4} [LE G] [LE P] [SMul G P] [self : IsOrderedSMul G P] (a : P) (b : P) : a ≤ b → ∀ (c : G), c • a ≤ c • b

theorem IsOrderedSMul.smul_le_smul_right {G : Type u_3} {P : Type u_4} [LE G] [LE P] [SMul G P] [self : IsOrderedSMul G P] (c : G) (d : G) : c ≤ d → ∀ (a : P), c • a ≤ d • a

instance instCovariantClassHVAddLeOfIsOrderedVAdd {G : Type u_1} {P : Type u_2} [LE G] [LE P] [VAdd G P] [IsOrderedVAdd G P] : CovariantClass G P (fun (x : G) (x_1 : P) => x +ᵥ x_1) fun (x x_1 : P) => x ≤ x_1

Equations

• ⋯ = ⋯

instance instCovariantClassHSMulLeOfIsOrderedSMul {G : Type u_1} {P : Type u_2} [LE G] [LE P] [SMul G P] [IsOrderedSMul G P] : CovariantClass G P (fun (x : G) (x_1 : P) => x • x_1) fun (x x_1 : P) => x ≤ x_1

Equations

• ⋯ = ⋯

instance instIsOrderedVAdd {G : Type u_1} [OrderedAddCommMonoid G] : IsOrderedVAdd G G

Equations

• ⋯ = ⋯

instance instIsOrderedSMul {G : Type u_1} [OrderedCommMonoid G] : IsOrderedSMul G G

Equations

• ⋯ = ⋯

theorem IsOrderedVAdd.vadd_le_vadd {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [VAdd G P] [IsOrderedVAdd G P] {a : G} {b : G} {c : P} {d : P} (hab : a ≤ b) (hcd : c ≤ d) : a +ᵥ c ≤ b +ᵥ d

theorem IsOrderedSMul.smul_le_smul {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [SMul G P] [IsOrderedSMul G P] {a : G} {b : G} {c : P} {d : P} (hab : a ≤ b) (hcd : c ≤ d) : a • c ≤ b • d

theorem Monotone.vadd {G : Type u_1} {P : Type u_2} {γ : Type u_3} [Preorder G] [Preorder P] [Preorder γ] [VAdd G P] [IsOrderedVAdd G P] {f : γ → G} {g : γ → P} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : γ) => f x +ᵥ g x

theorem Monotone.smul {G : Type u_1} {P : Type u_2} {γ : Type u_3} [Preorder G] [Preorder P] [Preorder γ] [SMul G P] [IsOrderedSMul G P] {f : γ → G} {g : γ → P} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : γ) => f x • g x

class IsCancelVAdd (G : Type u_3) (P : Type u_4) [VAdd G P] : Prop

A vector addition is cancellative if it is pointwise injective on the left and right.

• left_cancel : ∀ (a : G) (b c : P), a +ᵥ b = a +ᵥ c → b = c
• right_cancel : ∀ (a b : G) (c : P), a +ᵥ c = b +ᵥ c → a = b

theorem IsCancelVAdd.left_cancel {G : Type u_3} {P : Type u_4} [VAdd G P] [self : IsCancelVAdd G P] (a : G) (b : P) (c : P) : a +ᵥ b = a +ᵥ c → b = c

theorem IsCancelVAdd.right_cancel {G : Type u_3} {P : Type u_4} [VAdd G P] [self : IsCancelVAdd G P] (a : G) (b : G) (c : P) : a +ᵥ c = b +ᵥ c → a = b

@[deprecated IsCancelVAdd]

def CancelVAdd (G : Type u_3) (P : Type u_4) [VAdd G P] : Prop

Alias of IsCancelVAdd.

---

A vector addition is cancellative if it is pointwise injective on the left and right.

Equations

• CancelVAdd = IsCancelVAdd

class IsCancelSMul (G : Type u_3) (P : Type u_4) [SMul G P] : Prop

A scalar multiplication is cancellative if it is pointwise injective on the left and right.

• left_cancel : ∀ (a : G) (b c : P), a • b = a • c → b = c
• right_cancel : ∀ (a b : G) (c : P), a • c = b • c → a = b

theorem IsCancelSMul.left_cancel {G : Type u_3} {P : Type u_4} [SMul G P] [self : IsCancelSMul G P] (a : G) (b : P) (c : P) : a • b = a • c → b = c

theorem IsCancelSMul.right_cancel {G : Type u_3} {P : Type u_4} [SMul G P] [self : IsCancelSMul G P] (a : G) (b : G) (c : P) : a • c = b • c → a = b

class IsOrderedCancelVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] extends IsOrderedVAdd : Prop

An ordered cancellative vector addition is an ordered vector addition that is cancellative.

• vadd_le_vadd_left : ∀ (a b : P), a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b
• vadd_le_vadd_right : ∀ (c d : G), c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a
• le_of_vadd_le_vadd_left : ∀ (a : G) (b c : P), a +ᵥ b ≤ a +ᵥ c → b ≤ c
• le_of_vadd_le_vadd_right : ∀ (a b : G) (c : P), a +ᵥ c ≤ b +ᵥ c → a ≤ b

theorem IsOrderedCancelVAdd.le_of_vadd_le_vadd_left {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : IsOrderedCancelVAdd G P] (a : G) (b : P) (c : P) : a +ᵥ b ≤ a +ᵥ c → b ≤ c

theorem IsOrderedCancelVAdd.le_of_vadd_le_vadd_right {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : IsOrderedCancelVAdd G P] (a : G) (b : G) (c : P) : a +ᵥ c ≤ b +ᵥ c → a ≤ b

@[deprecated IsOrderedCancelVAdd]

def OrderedCancelVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] : Prop

Alias of IsOrderedCancelVAdd.

---

An ordered cancellative vector addition is an ordered vector addition that is cancellative.

Equations

• OrderedCancelVAdd = IsOrderedCancelVAdd

class IsOrderedCancelSMul (G : Type u_3) (P : Type u_4) [LE G] [LE P] [SMul G P] extends IsOrderedSMul : Prop

An ordered cancellative scalar multiplication is an ordered scalar multiplication that is cancellative.

• smul_le_smul_left : ∀ (a b : P), a ≤ b → ∀ (c : G), c • a ≤ c • b
• smul_le_smul_right : ∀ (c d : G), c ≤ d → ∀ (a : P), c • a ≤ d • a
• le_of_smul_le_smul_left : ∀ (a : G) (b c : P), a • b ≤ a • c → b ≤ c
• le_of_smul_le_smul_right : ∀ (a b : G) (c : P), a • c ≤ b • c → a ≤ b

theorem IsOrderedCancelSMul.le_of_smul_le_smul_left {G : Type u_3} {P : Type u_4} [LE G] [LE P] [SMul G P] [self : IsOrderedCancelSMul G P] (a : G) (b : P) (c : P) : a • b ≤ a • c → b ≤ c

theorem IsOrderedCancelSMul.le_of_smul_le_smul_right {G : Type u_3} {P : Type u_4} [LE G] [LE P] [SMul G P] [self : IsOrderedCancelSMul G P] (a : G) (b : G) (c : P) : a • c ≤ b • c → a ≤ b

instance instIsCancelVAddOfIsOrderedCancelVAdd {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] : IsCancelVAdd G P

Equations

• ⋯ = ⋯

instance instIsCancelSMulOfIsOrderedCancelSMul {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] : IsCancelSMul G P

Equations

• ⋯ = ⋯

instance instIsOrderedCancelVAdd {G : Type u_1} [OrderedCancelAddCommMonoid G] : IsOrderedCancelVAdd G G

Equations

• ⋯ = ⋯

instance instIsOrderedCancelSMul {G : Type u_1} [OrderedCancelCommMonoid G] : IsOrderedCancelSMul G G

Equations

• ⋯ = ⋯

@[instance 200]

instance instContravariantClassHVAddLeOfIsOrderedCancelVAdd {G : Type u_1} {P : Type u_2} [LE G] [LE P] [VAdd G P] [IsOrderedCancelVAdd G P] : ContravariantClass G P (fun (x : G) (x_1 : P) => x +ᵥ x_1) fun (x x_1 : P) => x ≤ x_1

Equations

• ⋯ = ⋯

@[instance 200]

instance instContravariantClassHSMulLeOfIsOrderedCancelSMul {G : Type u_1} {P : Type u_2} [LE G] [LE P] [SMul G P] [IsOrderedCancelSMul G P] : ContravariantClass G P (fun (x : G) (x_1 : P) => x • x_1) fun (x x_1 : P) => x ≤ x_1

Equations

• ⋯ = ⋯

theorem VAdd.vadd_lt_vadd_of_le_of_lt {G : Type u_1} {P : Type u_2} [LE G] [Preorder P] [VAdd G P] [IsOrderedCancelVAdd G P] {a : G} {b : G} {c : P} {d : P} (h₁ : a ≤ b) (h₂ : c < d) : a +ᵥ c < b +ᵥ d

theorem SMul.smul_lt_smul_of_le_of_lt {G : Type u_1} {P : Type u_2} [LE G] [Preorder P] [SMul G P] [IsOrderedCancelSMul G P] {a : G} {b : G} {c : P} {d : P} (h₁ : a ≤ b) (h₂ : c < d) : a • c < b • d

theorem VAdd.vadd_lt_vadd_of_lt_of_le {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [VAdd G P] [IsOrderedCancelVAdd G P] {a : G} {b : G} {c : P} {d : P} (h₁ : a < b) (h₂ : c ≤ d) : a +ᵥ c < b +ᵥ d

theorem SMul.smul_lt_smul_of_lt_of_le {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [SMul G P] [IsOrderedCancelSMul G P] {a : G} {b : G} {c : P} {d : P} (h₁ : a < b) (h₂ : c ≤ d) : a • c < b • d