# mathlibdocumentation

algebra.module.ordered

# Ordered semimodules

In this file we define

• ordered_semimodule R M : an ordered additive commutative monoid M is an ordered_semimodule over an ordered_semiring R if the scalar product respects the order relation on the monoid and on the ring. There is a correspondence between this structure and convex cones, which is proven in analysis/convex/cone.lean.

## Implementation notes

• We choose to define ordered_semimodule so that it extends semimodule only, as is done for semimodules itself.
• To get ordered modules and ordered vector spaces, it suffices to the replace the order_add_comm_monoid and the ordered_semiring as desired.

## References

• https://en.wikipedia.org/wiki/Ordered_vector_space

## Tags

ordered semimodule, ordered module, ordered vector space

@[class]
structure ordered_semimodule (R : Type u_1) (M : Type u_2)  :
Type (max u_1 u_2)
• to_semimodule : M
• smul_lt_smul_of_pos : ∀ {a b : M} {c_1 : R}, a < b0 < c_1c_1 a < c_1 b
• lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c_1 : R}, c_1 a < c_1 b0 < c_1a < b

An ordered semimodule is an ordered additive commutative monoid with a partial order in which the scalar multiplication is compatible with the order.

Instances
theorem smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} [ M] {a b : M} {c : R} :
a < b0 < cc a < c b

theorem smul_le_smul_of_nonneg {R : Type u_1} {M : Type u_2} [ M] {a b : M} {c : R} :
a b0 cc a c b

theorem eq_of_smul_eq_smul_of_pos_of_le {R : Type u_1} {M : Type u_2} [ M] {a b : M} {c : R} :
c a = c b0 < ca ba = b

theorem lt_of_smul_lt_smul_of_nonneg {R : Type u_1} {M : Type u_2} [ M] {a b : M} {c : R} :
c a < c b0 ca < b

theorem smul_lt_smul_iff_of_pos {R : Type u_1} {M : Type u_2} [ M] {a b : M} {c : R} :
0 < c(c a < c b a < b)

theorem smul_pos_iff_of_pos {R : Type u_1} {M : Type u_2} [ M] {a : M} {c : R} :
0 < c(0 < c a 0 < a)

def ordered_semimodule.mk'' {R : Type u_1} {M : Type u_2} [ M] :
(∀ {c : R}, c 0is_unit c)(∀ ⦃a b : M⦄ ⦃c : R⦄, a < b0 < cc a c b)

If R is a linear ordered semifield, then it suffices to verify only the first axiom of ordered_semimodule. Moreover, it suffices to verify that a < b and 0 < c imply c • a ≤ c • b. We have no semifields in mathlib, so we use the assumption ∀ c ≠ 0, is_unit c instead.

Equations
def ordered_semimodule.mk' {k : Type u_1} {M : Type u_2} [ M] :
(∀ ⦃a b : M⦄ ⦃c : k⦄, a < b0 < cc a c b)

If R is a linear ordered field, then it suffices to verify only the first axiom of ordered_semimodule.

Equations
@[instance]

Equations
theorem smul_le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] {a b : M} {c : k} :
0 < c(c a c b a b)

theorem smul_le_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [ M] {a b : M} {c : k} :
c < 0(c a c b b a)

theorem smul_lt_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] {a b : M} {c : k} :
0 < c(c a < b a < c⁻¹ b)

theorem smul_le_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] {a b : M} {c : k} :
0 < c(c a b a c⁻¹ b)

theorem le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] {a b : M} {c : k} :
0 < c(a c b c⁻¹ a b)

@[instance]
def prod.ordered_semimodule {k : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] :
(M × N)

Equations
@[instance]
def order_dual.has_scalar {R : Type u_1} {M : Type u_2} [semiring R] [ M] :

Equations
@[instance]
def order_dual.mul_action {R : Type u_1} {M : Type u_2} [semiring R] [ M] :

Equations
@[instance]
def order_dual.distrib_mul_action {R : Type u_1} {M : Type u_2} [semiring R] [ M] :

Equations
@[instance]
def order_dual.semimodule {R : Type u_1} {M : Type u_2} [semiring R] [ M] :

Equations
@[instance]
def order_dual.ordered_semimodule {R : Type u_1} {M : Type u_2} [ M] :

Equations