# 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`.

source
instance Nonneg.instSMul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] :
SMul { c : R // 0 ≤ c } S
Equations

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

source
@[simp]
theorem Nonneg.coe_smul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] (a : { c : R // 0 ≤ c }) (x : S) :
↑a • x = a • x
source
@[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
source
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 { c : R // 0 ≤ c } S M
source
instance Nonneg.instSMulWithZero {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [Zero S] [SMulWithZero R S] :
SMulWithZero { c : R // 0 ≤ c } S
Equations

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

source
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 { c : R // 0 ≤ c } M
source
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 { c : R // 0 ≤ c } M
source
instance Nonneg.instModule {R : Type u_1} {M : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid M] [Module R M] :
Module { c : R // 0 ≤ c } M

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

Equations

- Nonneg.instModule = Module.compHom M Nonneg.coeRingHom