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.
@[implicit_reducible]
instance
Nonneg.instSMul
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[PartialOrder R]
[SMul R S]
:
SMul { c : R // 0 ≤ c } S
@[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
@[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 { c : R // 0 ≤ c } S M
@[implicit_reducible]
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
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
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
@[implicit_reducible]
instance
Nonneg.instModule
{R : Type u_1}
{M : Type u_3}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[AddCommMonoid M]
[Module R M]
:
A module over an ordered semiring is also a module over just the non-negative scalars.