mathlib documentation

algebra.module.ordered

Ordered semimodules

In this file we define

Implementation notes

References

Tags

ordered semimodule, ordered module, ordered vector space

@[class]
structure ordered_semimodule (R : Type u_1) (M : Type u_2) [ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R 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 semimodule 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} [ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R M] [ordered_semimodule R 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} [ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R M] [ordered_semimodule R 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} [ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R M] [ordered_semimodule 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] [semimodule R M] [ordered_semimodule 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] [semimodule R M] [ordered_semimodule R 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} [ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R M] [ordered_semimodule R M] {a : M} {c : R} (hc : 0 < c) :
0 < c a 0 < a

theorem ordered_semimodule.mk'' {R : Type u_1} {M : Type u_2} [linear_ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R M] (hR : ∀ {c : R}, c 0is_unit c) (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_semimodule. 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_semimodule.mk' {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_monoid M] [semimodule k 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_semimodule.

theorem smul_le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [semimodule k M] [ordered_semimodule k 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} [linear_ordered_field k] [ordered_add_comm_group M] [semimodule k M] [ordered_semimodule k 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} [linear_ordered_field k] [ordered_add_comm_group M] [semimodule k M] [ordered_semimodule k 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} [linear_ordered_field k] [ordered_add_comm_group M] [semimodule k M] [ordered_semimodule k 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} [linear_ordered_field k] [ordered_add_comm_group M] [semimodule k M] [ordered_semimodule k M] {a b : M} {c : k} (hc : 0 < c) :
a c b c⁻¹ a b

@[instance]

@[instance]
def pi.ordered_semimodule {k : Type u_1} [linear_ordered_field k] {ι : Type u_2} {M : ι → Type u_3} [Π (i : ι), ordered_add_comm_group (M i)] [Π (i : ι), semimodule k (M i)] [∀ (i : ι), ordered_semimodule k (M i)] :
ordered_semimodule k (Π (i : ι), M i)

@[instance]
def pi.ordered_semimodule' {k : Type u_1} [linear_ordered_field k] {ι : Type u_2} {M : Type u_3} [ordered_add_comm_group M] [semimodule k M] [ordered_semimodule k M] :
ordered_semimodule k (ι → M)