Documentation

Mathlib.Algebra.Order.AddTorsor

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] :

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

Instances

@[deprecated IsOrderedVAdd]

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

Alias of IsOrderedVAdd.

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

Equations

OrderedVAdd = IsOrderedVAdd

Instances For

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

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

Instances

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

Equations

⋯ = ⋯

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

Equations

⋯ = ⋯

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

IsOrderedSMul G G

Equations

⋯ = ⋯

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

IsOrderedVAdd G G

Equations

⋯ = ⋯

theorem IsOrderedSMul.smul_le_smul {G : Type u_1} {P : Type u_2} [Preorder 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} [Preorder 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] :

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

Instances

@[deprecated IsCancelVAdd]

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

Alias of IsCancelVAdd.

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

Equations

CancelVAdd = IsCancelVAdd

Instances For

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

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

Instances

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

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

Instances

@[deprecated IsOrderedCancelVAdd]

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

Alias of IsOrderedCancelVAdd.

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

Equations

OrderedCancelVAdd = IsOrderedCancelVAdd

Instances For

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

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

Instances

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 instIsCancelVAddOfIsOrderedCancelVAdd {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] :

IsCancelVAdd G P

Equations

⋯ = ⋯

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

IsOrderedCancelSMul G G

Equations

⋯ = ⋯

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

IsOrderedCancelVAdd G G

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

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

Equations

⋯ = ⋯

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