# mathlibdocumentation

algebra.module.ordered

# Ordered modules #

In this file we define

• ordered_module R M : an ordered additive commutative monoid M is an ordered_module 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_module as a Prop-valued mixin, so that it can be used for both modules and algebras (the axioms for an "ordered algebra" are exactly that the algebra is ordered as a module).
• To get ordered modules and ordered vector spaces, it suffices to replace the order_add_comm_monoid and the ordered_semiring as desired.

## Tags #

ordered module, ordered module, ordered vector space

@[class]
structure ordered_module (R : Type u_1) (M : Type u_2) [ M] :
Prop
• smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b0 < cc a < c b
• lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c a < c b0 < ca < b

An ordered module 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] [ 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] [ M] {a b : M} {c : R} (h₁ : a b) (h₂ : 0 c) :
c a c b
theorem eq_of_smul_eq_smul_of_pos_of_le {R : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : R} (h₁ : c a = c b) (hc : 0 < c) (hle : a b) :
a = b
theorem lt_of_smul_lt_smul_of_nonneg {R : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : R} (h : c a < c b) (hc : 0 c) :
a < b
theorem smul_lt_smul_iff_of_pos {R : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : R} (hc : 0 < c) :
c a < c b a < b
theorem smul_pos_iff_of_pos {R : Type u_1} {M : Type u_2} [ M] [ M] {a : M} {c : R} (hc : 0 < c) :
0 < c a 0 < a
theorem ordered_module.mk'' {R : Type u_1} {M : Type u_2} [ M] (hR : ∀ {c : R}, c 0) (hlt : ∀ ⦃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_module. 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.

theorem ordered_module.mk' {k : Type u_1} {M : Type u_2} [ M] (hlt : ∀ ⦃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_module.

@[protected, instance]
theorem smul_le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : k} (hc : 0 < c) :
c a c b a b
theorem smul_le_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : k} (hc : c < 0) :
c a c b b a
theorem smul_lt_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : k} (hc : 0 < c) :
c a < b a < c⁻¹ b
theorem smul_le_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : k} (hc : 0 < c) :
c a b a c⁻¹ b
theorem le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [ M] [ M] {a b : M} {c : k} (hc : 0 < c) :
a c b c⁻¹ a b
@[protected, instance]
def prod.ordered_module {k : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ M] [ N] [ N] :
(M × N)
@[protected, instance]
def pi.ordered_module {k : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Π (i : ι), ] [Π (i : ι), (M i)] [∀ (i : ι), (M i)] :
(Π (i : ι), M i)
@[protected, instance]
def pi.ordered_module' {k : Type u_1} {ι : Type u_2} {M : Type u_3} [ M] [ M] :
(ι → M)
@[protected, instance]
def order_dual.has_scalar {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected, instance]
def order_dual.mul_action {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected, instance]
def order_dual.distrib_mul_action {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected, instance]
def order_dual.module {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected, instance]
def order_dual.ordered_module {R : Type u_1} {M : Type u_2} [ M] [ M] :