Documentation

Mathlib.Algebra.Order.Module.OrderedSMul

Ordered scalar product #

In this file we define

Implementation notes #

TODO #

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

References #

Tags #

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

class OrderedSMul (R : Type u_1) (M : Type u_2) [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] :

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 < b0 < cc 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 b0 < ca < b

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

Instances
    theorem OrderedSMul.smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} :
    ∀ {inst : OrderedSemiring R} {inst_1 : OrderedAddCommMonoid M} {inst_2 : SMulWithZero R M} [self : OrderedSMul R M] {a b : M} {c : R}, a < b0 < cc a < c b

    Scalar multiplication by positive elements preserves the order.

    theorem OrderedSMul.lt_of_smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} :
    ∀ {inst : OrderedSemiring R} {inst_1 : OrderedAddCommMonoid M} {inst_2 : SMulWithZero R M} [self : OrderedSMul R M] {a b : M} {c : R}, c a < c b0 < ca < b

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

    Equations
    • =
    theorem OrderedSMul.mk'' {𝕜 : Type u_5} {M : Type u_7} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid M] [SMulWithZero 𝕜 M] (h : ∀ ⦃c : 𝕜⦄, 0 < cStrictMono fun (a : M) => c a) :

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

    Equations
    • =
    theorem OrderedSMul.mk' {𝕜 : Type u_5} {M : Type u_7} [LinearOrderedSemifield 𝕜] [OrderedAddCommMonoid M] [MulActionWithZero 𝕜 M] (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b0 < cc a c b) :

    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_5} {M : Type u_7} {N : Type u_8} [LinearOrderedSemifield 𝕜] [OrderedAddCommMonoid M] [OrderedAddCommMonoid N] [MulActionWithZero 𝕜 M] [MulActionWithZero 𝕜 N] [OrderedSMul 𝕜 M] [OrderedSMul 𝕜 N] :
    OrderedSMul 𝕜 (M × N)
    Equations
    • =
    instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_5} [LinearOrderedSemifield 𝕜] {M : ιType u_9} [(i : ι) → OrderedAddCommMonoid (M i)] [(i : ι) → MulActionWithZero 𝕜 (M i)] [∀ (i : ι), OrderedSMul 𝕜 (M i)] :
    OrderedSMul 𝕜 ((i : ι) → M i)
    Equations
    • =
    theorem inf_eq_half_smul_add_sub_abs_sub (α : Type u_9) {β : Type u_10} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] (x : β) (y : β) :
    x y = 2 (x + y - |y - x|)
    theorem sup_eq_half_smul_add_add_abs_sub (α : Type u_9) {β : Type u_10} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] (x : β) (y : β) :
    x y = 2 (x + y + |y - x|)
    theorem inf_eq_half_smul_add_sub_abs_sub' (α : Type u_9) {β : Type u_10} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] (x : β) (y : β) :
    x y = 2⁻¹ (x + y - |y - x|)
    theorem sup_eq_half_smul_add_add_abs_sub' (α : Type u_9) {β : Type u_10} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] (x : β) (y : β) :
    x y = 2⁻¹ (x + y + |y - x|)