Ordered scalar product #
In this file we define
ordered_smul R M: an ordered additive commutative monoidMis anordered_smulover 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_smulas aProp-valued mixin, so that it can be used for actions, 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 scalar, ordered smul, ordered action, ordered vector space
@[class]
structure
ordered_smul
(R : Type u_1)
(M : Type u_2)
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero 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
The ordered scalar product property is when an ordered additive commutative monoid with a partial order has a scalar multiplication which is compatible with the order.
@[protected, instance]
def
order_dual.has_scalar
{R : Type u_1}
{M : Type u_2}
[has_scalar R M] :
has_scalar R (order_dual M)
Equations
- order_dual.has_scalar = {smul := λ (k : R) (x : order_dual M), order_dual.rec (λ (x' : M), k • x') x}
@[protected, instance]
def
order_dual.smul_with_zero
{R : Type u_1}
{M : Type u_2}
[has_zero R]
[add_zero_class M]
[h : smul_with_zero R M] :
smul_with_zero R (order_dual M)
Equations
- order_dual.smul_with_zero = {to_has_scalar := {smul := has_scalar.smul order_dual.has_scalar}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
order_dual.mul_action
{R : Type u_1}
{M : Type u_2}
[monoid R]
[mul_action R M] :
mul_action R (order_dual M)
Equations
- order_dual.mul_action = {to_has_scalar := {smul := has_scalar.smul order_dual.has_scalar}, one_smul := _, mul_smul := _}
@[protected, instance]
def
order_dual.mul_action_with_zero
{R : Type u_1}
{M : Type u_2}
[monoid_with_zero R]
[add_monoid M]
[mul_action_with_zero R M] :
Equations
- order_dual.mul_action_with_zero = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar order_dual.mul_action, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
order_dual.distrib_mul_action
{R : Type u_1}
{M : Type u_2}
[monoid_with_zero R]
[add_monoid M]
[distrib_mul_action R M] :
distrib_mul_action R (order_dual M)
Equations
@[protected, instance]
def
order_dual.ordered_smul
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M] :
ordered_smul R (order_dual M)
@[simp]
theorem
order_dual.to_dual_smul
{R : Type u_1}
{M : Type u_2}
[has_scalar R M]
{c : R}
{a : M} :
⇑order_dual.to_dual (c • a) = c • ⇑order_dual.to_dual a
@[simp]
theorem
order_dual.of_dual_smul
{R : Type u_1}
{M : Type u_2}
[has_scalar R M]
{c : R}
{a : order_dual M} :
⇑order_dual.of_dual (c • a) = c • ⇑order_dual.of_dual a
theorem
smul_lt_smul_of_pos
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul 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]
[smul_with_zero R M]
[ordered_smul R M]
{a b : M}
{c : R}
(h₁ : a ≤ b)
(h₂ : 0 ≤ c) :
theorem
smul_nonneg
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 ≤ c)
(ha : 0 ≤ a) :
theorem
smul_nonpos_of_nonneg_of_nonpos
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 ≤ c)
(ha : a ≤ 0) :
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]
[smul_with_zero R M]
[ordered_smul 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]
[smul_with_zero R M]
[ordered_smul 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]
[smul_with_zero R M]
[ordered_smul 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]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 < c) :
theorem
smul_pos
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 < c) :
Alias of smul_pos_iff_of_pos.
theorem
monotone_smul_left
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{c : R}
(hc : 0 ≤ c) :
theorem
strict_mono_smul_left
{R : Type u_1}
{M : Type u_2}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{c : R}
(hc : 0 < c) :
theorem
ordered_smul.mk''
{R : Type u_1}
{M : Type u_2}
[linear_ordered_semiring R]
[ordered_add_comm_monoid M]
[mul_action_with_zero 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_smul R M
If R is a linear ordered semifield, then it suffices to verify only the first axiom of
ordered_smul. 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_smul.mk'
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_monoid M]
[mul_action_with_zero k M]
(hlt : ∀ ⦃a b : M⦄ ⦃c : k⦄, a < b → 0 < c → c • a ≤ c • b) :
ordered_smul k M
If R is a linear ordered field, then it suffices to verify only the first axiom of
ordered_smul.
@[protected, instance]
def
linear_ordered_semiring.to_ordered_smul
{R : Type u_1}
[linear_ordered_semiring R] :
ordered_smul 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]
[mul_action_with_zero k M]
[ordered_smul k M]
{a b : M}
{c : k}
(hc : 0 < c) :
theorem
smul_lt_iff_of_pos
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[mul_action_with_zero k M]
[ordered_smul k M]
{a b : M}
{c : k}
(hc : 0 < c) :
theorem
lt_smul_iff_of_pos
{k : Type u_1}
{M : Type u_2}
[linear_ordered_field k]
[ordered_add_comm_group M]
[mul_action_with_zero k M]
[ordered_smul 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]
[mul_action_with_zero k M]
[ordered_smul 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]
[mul_action_with_zero k M]
[ordered_smul k M]
{a b : M}
{c : k}
(hc : 0 < c) :
@[simp]
theorem
order_iso.smul_left_apply
{k : Type u_1}
(M : Type u_2)
[linear_ordered_field k]
[ordered_add_comm_group M]
[mul_action_with_zero k M]
[ordered_smul k M]
{c : k}
(hc : 0 < c)
(b : M) :
⇑(order_iso.smul_left M hc) b = c • b
def
order_iso.smul_left
{k : Type u_1}
(M : Type u_2)
[linear_ordered_field k]
[ordered_add_comm_group M]
[mul_action_with_zero k M]
[ordered_smul k M]
{c : k}
(hc : 0 < c) :
M ≃o M
Left scalar multiplication as an order isomorphism.
@[simp]
theorem
order_iso.smul_left_symm_apply
{k : Type u_1}
(M : Type u_2)
[linear_ordered_field k]
[ordered_add_comm_group M]
[mul_action_with_zero k M]
[ordered_smul k M]
{c : k}
(hc : 0 < c)
(b : M) :
⇑(rel_iso.symm (order_iso.smul_left M hc)) b = c⁻¹ • b