Modules over nonnegative elements #

This file defines instances and prove some properties about modules over nonnegative elements {c : 𝕜 // 0 ≤ c} of an arbitrary OrderedSemiring 𝕜.

These instances are useful for working with ConvexCone.

instance Nonneg.instSMul {𝕜 : Type u_1} {𝕜' : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [SMul 𝕜 𝕜'] :

SMul { c : 𝕜 // 0 ≤ c } 𝕜'

Equations

@[simp]

theorem Nonneg.coe_smul {𝕜 : Type u_1} {𝕜' : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [SMul 𝕜 𝕜'] (a : { c : 𝕜 // 0 ≤ c }) (x : 𝕜') :

↑a • x = a • x

@[simp]

theorem Nonneg.mk_smul {𝕜 : Type u_1} {𝕜' : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [SMul 𝕜 𝕜'] (a : 𝕜) (ha : 0 ≤ a) (x : 𝕜') :

⟨a, ha⟩ • x = a • x

instance Nonneg.instIsScalarTower {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [SMul 𝕜 𝕜'] [SMul 𝕜 E] [SMul 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower { c : 𝕜 // 0 ≤ c } 𝕜' E

instance Nonneg.instSMulWithZero {𝕜 : Type u_1} {𝕜' : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [Zero 𝕜'] [SMulWithZero 𝕜 𝕜'] :

SMulWithZero { c : 𝕜 // 0 ≤ c } 𝕜'

Equations

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

instance Nonneg.instModule {𝕜 : Type u_1} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] :

Module { c : 𝕜 // 0 ≤ c } E

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

Equations

instance Nonneg.instModuleFinite {𝕜 : Type u_1} {E : Type u_3} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [Module.Finite 𝕜 E] :

If a module is finite over a linearly ordered ring, then it is also finite over the non-negative scalars.

Documentation