Ordered scalar product

In this file we define

• OrderedSMul R M : an ordered additive commutative monoid M is an OrderedSMul over an OrderedSemiring R if 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 in Mathlib/Analysis/Convex/Cone.lean.

Implementation notes

• We choose to define OrderedSMul as a Prop-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 OrderedAddCommMonoid and the OrderedSemiring as desired.

TODO

This file is now mostly useless. We should try deleting OrderedSMul

References

• https://en.wikipedia.org/wiki/Ordered_vector_space

Tags

ordered module, ordered scalar, ordered smul, ordered action, ordered vector space

class OrderedSMul (R : Type u_1) (M : Type u_2) [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] : Prop

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. Note that this is different from IsOrderedSMul, which uses ≤, has no semiring assumption, and has no positivity constraint on the defining conditions.

• smul_lt_smul_of_pos {a b : M} {c : R} : a < b → 0 < c → c • a < c • b

  Scalar multiplication by positive elements preserves the order.

• lt_of_smul_lt_smul_of_pos {a b : M} {c : R} : c • a < c • b → 0 < c → a < b

  If c • a < c • b for some positive c, then a < b.

instance OrderedSMul.toPosSMulStrictMono {R : Type u_3} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] [OrderedSMul R M] : PosSMulStrictMono R M

instance OrderedSMul.toPosSMulReflectLT {R : Type u_3} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] [OrderedSMul R M] : PosSMulReflectLT R M

instance OrderDual.instOrderedSMul {R : Type u_3} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] [OrderedSMul R M] : OrderedSMul R Mᵒᵈ

theorem OrderedSMul.mk'' {𝕜 : Type u_2} {M : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid M] [LinearOrder M] [SMulWithZero 𝕜 M] (h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun (a : M) => c • a) : OrderedSMul 𝕜 M

To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first axiom of OrderedSMul.

instance Nat.orderedSMul {M : Type u_4} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : OrderedSMul ℕ M

instance Int.orderedSMul {M : Type u_4} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : OrderedSMul ℤ M

instance LinearOrderedSemiring.toOrderedSMul {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] : OrderedSMul R R

theorem OrderedSMul.mk' {𝕜 : Type u_2} {M : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommMonoid M] [PartialOrder M] [MulActionWithZero 𝕜 M] (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) : OrderedSMul 𝕜 M

To prove that a vector space over a linear ordered field is ordered, it suffices to verify only the first axiom of OrderedSMul.

instance instOrderedSMulProd {𝕜 : Type u_2} {M : Type u_4} {N : Type u_5} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommMonoid M] [PartialOrder M] [AddCommMonoid N] [PartialOrder N] [MulActionWithZero 𝕜 M] [MulActionWithZero 𝕜 N] [OrderedSMul 𝕜 M] [OrderedSMul 𝕜 N] : OrderedSMul 𝕜 (M × N)

instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {M : ι → Type u_6} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → PartialOrder (M i)] [(i : ι) → MulActionWithZero 𝕜 (M i)] [∀ (i : ι), OrderedSMul 𝕜 (M i)] : OrderedSMul 𝕜 ((i : ι) → M i)

theorem inf_eq_half_smul_add_sub_abs_sub (α : Type u_6) {β : Type u_7} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [Module α β] [AddLeftMono β] (x y : β) : x ⊓ y = ⅟2 • (x + y - |y - x|)

theorem sup_eq_half_smul_add_add_abs_sub (α : Type u_6) {β : Type u_7} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [Module α β] [AddLeftMono β] (x y : β) : x ⊔ y = ⅟2 • (x + y + |y - x|)

theorem inf_eq_half_smul_add_sub_abs_sub' (α : Type u_6) {β : Type u_7} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [Module α β] [AddLeftMono β] (x y : β) : x ⊓ y = 2⁻¹ • (x + y - |y - x|)

theorem sup_eq_half_smul_add_add_abs_sub' (α : Type u_6) {β : Type u_7} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [Module α β] [AddLeftMono β] (x y : β) : x ⊔ y = 2⁻¹ • (x + y + |y - x|)