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] :
Type (max u_1 u_2)
  • to_semimodule : semimodule R M
  • smul_lt_smul_of_pos : ∀ {a b : M} {c_1 : R}, a < b0 < c_1c_1 a < c_1 b
  • lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c_1 : R}, c_1 a < c_1 b0 < c_1a < 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] [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] [ordered_semimodule R M] {a b : M} {c : R} :
a b0 cc 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] [ordered_semimodule R M] {a b : M} {c : R} :
c a = c b0 < ca ba = 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] [ordered_semimodule R M] {a b : M} {c : R} :
c a < c b0 ca < b

theorem smul_lt_smul_iff_of_pos {R : Type u_1} {M : Type u_2} [ordered_semiring R] [ordered_add_comm_monoid M] [ordered_semimodule R M] {a b : M} {c : R} :
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] [ordered_semimodule R M] {a : M} {c : R} :
0 < c(0 < c a 0 < a)

def ordered_semimodule.mk'' {R : Type u_1} {M : Type u_2} [linear_ordered_semiring R] [ordered_add_comm_monoid M] [semimodule R M] :
(∀ {c : R}, c 0is_unit c)(∀ ⦃a b : M⦄ ⦃c : R⦄, a < b0 < cc a c b)ordered_semimodule R M

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.

Equations
def ordered_semimodule.mk' {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_monoid M] [semimodule k M] :
(∀ ⦃a b : M⦄ ⦃c : k⦄, a < b0 < cc a c b)ordered_semimodule k M

If R is a linear ordered field, then it suffices to verify only the first axiom of ordered_semimodule.

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

@[instance]

Equations