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

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

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

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

instance instIsOrderedSMulOfIsOrderedMonoid {G : Type u_1} [CommMonoid G] [PartialOrder G] [IsOrderedMonoid G] : IsOrderedSMul G G

instance instIsOrderedVAddOfIsOrderedAddMonoid {G : Type u_1} [AddCommMonoid G] [PartialOrder G] [IsOrderedAddMonoid G] : IsOrderedVAdd G G

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

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

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

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

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

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

class IsOrderedCancelVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] extends IsOrderedVAdd G P : 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

class IsOrderedCancelSMul (G : Type u_3) (P : Type u_4) [LE G] [LE P] [SMul G P] extends IsOrderedSMul G P : 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

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

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

instance instIsOrderedCancelSMulOfIsOrderedCancelMonoid {G : Type u_1} [CommMonoid G] [PartialOrder G] [IsOrderedCancelMonoid G] : IsOrderedCancelSMul G G

instance instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid {G : Type u_1} [AddCommMonoid G] [PartialOrder G] [IsOrderedCancelAddMonoid G] : IsOrderedCancelVAdd G G

@[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 (x1 : G) (x2 : P) => x1 • x2) fun (x1 x2 : P) => x1 ≤ x2

@[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 (x1 : G) (x2 : P) => x1 +ᵥ x2) fun (x1 x2 : P) => x1 ≤ x2

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 b : G} {c d : P} (h₁ : a ≤ b) (h₂ : c < d) : a • c < b • d

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 b : G} {c 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 b : G} {c 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 b : G} {c d : P} (h₁ : a < b) (h₂ : c ≤ d) : a +ᵥ c < b +ᵥ d