Ordered modules #
In this file we define
ordered_module R M: an ordered additive commutative monoidMis anordered_moduleover anordered_semiringRif 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 inanalysis/convex/cone.lean.
Implementation notes #
- We choose to define
ordered_moduleas aProp-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_monoidand theordered_semiringas desired.
References #
Tags #
ordered module, ordered module, ordered vector space
@[class]
structure
ordered_module
(R : Type u_1)
(M : Type u_2)
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M] :
Prop
- smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b → 0 < c → c • a < c • b
- lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c • a < c • b → 0 < c → a < b
An ordered module 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}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R M]
{a b : M}
{c : R} :
theorem
smul_le_smul_of_nonneg
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R M]
{a b : M}
{c : R}
(h₁ : a ≤ b)
(h₂ : 0 ≤ c) :
theorem
eq_of_smul_eq_smul_of_pos_of_le
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R 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}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R 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}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R M]
{a b : M}
{c : R}
(hc : 0 < c) :
theorem
smul_pos_iff_of_pos
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R M]
{a : M}
{c : R}
(hc : 0 < c) :
theorem
ordered_module.mk''
{R : Type u_1}
{M : Type u_2}
[linear_ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
(hR : ∀ {c : R}, c ≠ 0 → is_unit c)
(hlt : ∀ ⦃a b : M⦄ ⦃c : R⦄, a < b → 0 < c → c • a ≤ c • b) :
ordered_module R M
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}
[linear_ordered_field k]
[ordered_add_comm_monoid M]
[module k M]
(hlt : ∀ ⦃a b : M⦄ ⦃c : k⦄, a < b → 0 < c → c • a ≤ c • b) :
ordered_module k M
If R is a linear ordered field, then it suffices to verify only the first axiom of
ordered_module.
@[protected, instance]
def
linear_ordered_semiring.to_ordered_module
{R : Type u_1}
[linear_ordered_semiring R] :
ordered_module R R
theorem
smul_le_smul_iff_of_pos
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[module k M]
[ordered_module k M]
{a b : M}
{c : k}
(hc : 0 < c) :
theorem
smul_le_smul_iff_of_neg
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[module k M]
[ordered_module k M]
{a b : M}
{c : k}
(hc : c < 0) :
theorem
smul_lt_iff_of_pos
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[module k M]
[ordered_module k M]
{a b : M}
{c : k}
(hc : 0 < c) :
theorem
smul_le_iff_of_pos
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[module k M]
[ordered_module k M]
{a b : M}
{c : k}
(hc : 0 < c) :
theorem
le_smul_iff_of_pos
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[module k M]
[ordered_module k M]
{a b : M}
{c : k}
(hc : 0 < c) :
@[protected, instance]
def
prod.ordered_module
{k : Type u_1}
{M : Type u_2}
{N : Type u_3}
[linear_ordered_field k]
[ordered_add_comm_group M]
[module k M]
[ordered_module k M]
[ordered_add_comm_group N]
[module k N]
[ordered_module k N] :
ordered_module k (M × N)
@[protected, instance]
def
pi.ordered_module
{k : Type u_1}
[linear_ordered_field k]
{ι : Type u_2}
{M : ι → Type u_3}
[Π (i : ι), ordered_add_comm_group (M i)]
[Π (i : ι), module k (M i)]
[∀ (i : ι), ordered_module k (M i)] :
ordered_module k (Π (i : ι), M i)
@[protected, instance]
def
pi.ordered_module'
{k : Type u_1}
[linear_ordered_field k]
{ι : Type u_2}
{M : Type u_3}
[ordered_add_comm_group M]
[module k M]
[ordered_module k M] :
ordered_module k (ι → M)
@[protected, instance]
def
order_dual.has_scalar
{R : Type u_1}
{M : Type u_2}
[semiring R]
[ordered_add_comm_monoid M]
[module R M] :
has_scalar R (order_dual M)
Equations
@[protected, instance]
def
order_dual.mul_action
{R : Type u_1}
{M : Type u_2}
[semiring R]
[ordered_add_comm_monoid M]
[module R M] :
mul_action R (order_dual M)
Equations
@[protected, instance]
def
order_dual.distrib_mul_action
{R : Type u_1}
{M : Type u_2}
[semiring R]
[ordered_add_comm_monoid M]
[module R M] :
distrib_mul_action R (order_dual M)
Equations
- order_dual.distrib_mul_action = {to_mul_action := order_dual.mul_action _inst_3, smul_add := _, smul_zero := _}
@[protected, instance]
def
order_dual.module
{R : Type u_1}
{M : Type u_2}
[semiring R]
[ordered_add_comm_monoid M]
[module R M] :
module R (order_dual M)
Equations
- order_dual.module = {to_distrib_mul_action := order_dual.distrib_mul_action _inst_3, add_smul := _, zero_smul := _}
@[protected, instance]
def
order_dual.ordered_module
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[module R M]
[ordered_module R M] :
ordered_module R (order_dual M)