Ordered semimodules
In this file we define
ordered_semimodule R M: an ordered additive commutative monoidMis anordered_semimoduleover anordered_semiringRif the scalar product respects the order relation on the monoid and on the ring.
Implementation notes
- We choose to define
ordered_semimoduleso that it extendssemimoduleonly, as is done for semimodules itself. - To get ordered modules and ordered vector spaces, it suffices to the replace the
order_add_comm_monoidand theordered_semiringas desired.
TODO
- Connect this with convex cones: show that a convex cone defines an order on the vector space and vice-versa.
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)
(β : 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.
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} :
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} :
@[instance]
@[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
@[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
@[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 := _}
@[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 := _}
@[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 β)