Modules over nonnegative elements

For an ordered ring R, this file proves that any (ordered) R-module M is also an (ordered) R≥0-module.

Among other things, these instances are useful for working with ConvexCone.

@[instance_reducible]

instance Nonneg.instSMul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] : SMul (Nonneg R) S

Equations

• Nonneg.instSMul = { smul := fun (c : Nonneg R) (x : S) => ↑c • x }

@[simp]

theorem Nonneg.coe_smul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] (a : Nonneg R) (x : S) : ↑a • x = a • x

@[simp]

theorem Nonneg.mk_smul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] (a : R) (ha : 0 ≤ a) (x : S) : ⟨a, ha⟩ • x = a • x

instance Nonneg.instIsScalarTower {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [SMul R S] [SMul R M] [SMul S M] [IsScalarTower R S M] : IsScalarTower (Nonneg R) S M

@[instance_reducible]

instance Nonneg.instSMulWithZero {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [Zero S] [SMulWithZero R S] : SMulWithZero (Nonneg R) S

Equations

• Nonneg.instSMulWithZero = { toSMul := Nonneg.instSMul, smul_zero := ⋯, zero_smul := ⋯ }

instance Nonneg.instIsOrderedModule {R : Type u_1} {M : Type u_3} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] [hM : IsOrderedModule R M] : IsOrderedModule (Nonneg R) M

instance Nonneg.instIsStrictOrderedModule {R : Type u_1} {M : Type u_3} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] [hM : IsStrictOrderedModule R M] : IsStrictOrderedModule (Nonneg R) M

@[instance_reducible]

instance Nonneg.instModule {R : Type u_1} {M : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid M] [Module R M] : Module (Nonneg R) M

A module over an ordered semiring is also a module over just the non-negative scalars.

Equations

• Nonneg.instModule = { toSMul := Nonneg.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }