mathlib documentation

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

source

@[class]

structure ordered_semimodule (R : Type u_1) (β : Type u_2) [ordered_semiring R] [ordered_add_comm_monoid β] :

Type (max u_1 u_2)

to_semimodule : semimodule R β
smul_lt_smul_of_pos : ∀ {a b : β} {c_1 : R}, a < b → 0 < c_1 → c_1 • a < c_1 • b
lt_of_smul_lt_smul_of_nonneg : ∀ {a b : β} {c_1 : R}, c_1 • a < c_1 • b → 0 ≤ c_1 → a < 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

source

theorem smul_lt_smul_of_pos {R : Type u_1} {β : Type u_2} [ordered_semiring R] [ordered_add_comm_monoid β] [ordered_semimodule R β] {a b : β} {c : R} (a_1 : a < b) (a_2 : 0 < c) :

c • a < c • b

source

theorem smul_le_smul_of_nonneg {R : Type u_1} {β : Type u_2} [ordered_semiring R] [ordered_add_comm_monoid β] [ordered_semimodule R β] {a b : β} {c : R} (h₁ : a ≤ b) (h₂ : 0 ≤ c) :

c • a ≤ c • b

source

@[instance]

def linear_ordered_ring.to_ordered_semimodule {R : Type u_1} [linear_ordered_ring R] :

ordered_semimodule R R

Equations

linear_ordered_ring.to_ordered_semimodule = {to_semimodule := semiring.to_semimodule (ordered_semiring.to_semiring R), smul_lt_smul_of_pos := _, lt_of_smul_lt_smul_of_nonneg := _}

source

@[instance]

def order_dual.has_scalar {R : Type u_1} {β : Type u_2} [semiring R] [ordered_add_comm_monoid β] [semimodule R β] :

has_scalar R (order_dual β)

Equations

order_dual.has_scalar = {smul := has_scalar.smul mul_action.to_has_scalar}

source

@[instance]

def order_dual.mul_action {R : Type u_1} {β : Type u_2} [semiring R] [ordered_add_comm_monoid β] [semimodule R β] :

mul_action R (order_dual β)

Equations

order_dual.mul_action = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, one_smul := _, mul_smul := _}

source

@[instance]

def order_dual.distrib_mul_action {R : Type u_1} {β : Type u_2} [semiring R] [ordered_add_comm_monoid β] [semimodule R β] :

distrib_mul_action R (order_dual β)

Equations

order_dual.distrib_mul_action = {to_mul_action := order_dual.mul_action _inst_3, smul_add := _, smul_zero := _}

source

@[instance]

def order_dual.semimodule {R : Type u_1} {β : Type u_2} [semiring R] [ordered_add_comm_monoid β] [semimodule R β] :

semimodule R (order_dual β)

Equations

order_dual.semimodule = {to_distrib_mul_action := order_dual.distrib_mul_action _inst_3, add_smul := _, zero_smul := _}

source

@[instance]

def order_dual.ordered_semimodule {R : Type u_1} {β : Type u_2} [ordered_semiring R] [ordered_add_comm_monoid β] [ordered_semimodule R β] :

ordered_semimodule R (order_dual β)

Equations

order_dual.ordered_semimodule = {to_semimodule := order_dual.semimodule ordered_semimodule.to_semimodule, smul_lt_smul_of_pos := _, lt_of_smul_lt_smul_of_nonneg := _}