Monotonicity of scalar multiplication by positive elements #

This file defines typeclasses to reason about monotonicity of the operations

b ↦ a • b, "left scalar multiplication"
a ↦ a • b, "right scalar multiplication"

We use eight typeclasses to encode the various properties we care about for those two operations. These typeclasses are meant to be mostly internal to this file, to set up each lemma in the appropriate generality.

Less granular typeclasses like IsOrderedAddMonoid and IsOrderedModule should be enough for most purposes, and the system is set up so that they imply the correct granular typeclasses here. If those are enough for you, you may stop reading here! Else, beware that what follows is a bit technical.

Definitions #

In all that follows, α and β are orders which have a 0 and such that α acts on β by scalar multiplication. Note however that we do not use lawfulness of this action in most of the file. Hence • should be considered here as a mostly arbitrary function α → β → β.

We use the following four typeclasses to reason about left scalar multiplication (b ↦ a • b):

PosSMulMono: If a ≥ 0, then b₁ ≤ b₂ implies a • b₁ ≤ a • b₂.
PosSMulStrictMono: If a > 0, then b₁ < b₂ implies a • b₁ < a • b₂.
PosSMulReflectLT: If a ≥ 0, then a • b₁ < a • b₂ implies b₁ < b₂.
PosSMulReflectLE: If a > 0, then a • b₁ ≤ a • b₂ implies b₁ ≤ b₂.

We use the following four typeclasses to reason about right scalar multiplication (a ↦ a • b):

SMulPosMono: If b ≥ 0, then a₁ ≤ a₂ implies a₁ • b ≤ a₂ • b.
SMulPosStrictMono: If b > 0, then a₁ < a₂ implies a₁ • b < a₂ • b.
SMulPosReflectLT: If b ≥ 0, then a₁ • b < a₂ • b implies a₁ < a₂.
SMulPosReflectLE: If b > 0, then a₁ • b ≤ a₂ • b implies a₁ ≤ a₂.

Furthermore, in a module, i.e. a group acted on by a ring, PosSMulMono and SMulPosMono are equivalent (they are both the same as ∀ r ≥ 0, ∀ m ≥ 0, 0 ≤ r • m), and similarly for PosSMulStrictMono and SMulPosStrictMono. To avoid dangerous instances going both, we have the extra two typeclasses:

IsOrderedModule: Conjunction of PosSMulMono and SMulPosMono
IsStrictOrderedModule: Conjunction of PosSMulStrictMono and SMulPosStrictMono.

Constructors #

The four typeclasses about nonnegativity can usually be checked only on positive inputs due to their condition becoming trivial when a = 0 or b = 0. We therefore make the following constructors available: PosSMulMono.of_pos, PosSMulReflectLT.of_pos, SMulPosMono.of_pos, SMulPosReflectLT.of_pos

Implications #

As α and β get more and more structure, those typeclasses end up being equivalent. The commonly used implications are:

When α, β are partial orders:
- PosSMulStrictMono → PosSMulMono
- SMulPosStrictMono → SMulPosMono
- PosSMulReflectLE → PosSMulReflectLT
- SMulPosReflectLE → SMulPosReflectLT
When β is a linear order:
- PosSMulStrictMono → PosSMulReflectLE
- PosSMulReflectLT → PosSMulMono (not registered as instance)
- SMulPosReflectLT → SMulPosMono (not registered as instance)
- PosSMulReflectLE → PosSMulStrictMono (not registered as instance)
- SMulPosReflectLE → SMulPosStrictMono (not registered as instance)
When α is a linear order:
- SMulPosStrictMono → SMulPosReflectLE
When α is an ordered ring, β an ordered group and also an α-module:
- PosSMulMono → SMulPosMono
- PosSMulStrictMono → SMulPosStrictMono
When α is an linear ordered semifield, β is an α-module:
- PosSMulStrictMono → PosSMulReflectLT
- PosSMulMono → PosSMulReflectLE
When α is a semiring, β is an α-module with NoZeroSMulDivisors:
- PosSMulMono → PosSMulStrictMono (not registered as instance)
When α is a ring, β is an α-module with NoZeroSMulDivisors:
- SMulPosMono → SMulPosStrictMono (not registered as instance)

Further, the bundled non-granular typeclasses imply the granular ones like so:

IsOrderedModule → PosSMulMono
IsOrderedModule → SMulPosMono
IsStrictOrderedModule → PosSMulStrictMono
IsStrictOrderedModule → SMulPosStrictMono

Unless otherwise stated, all these implications are registered as instances, which means that in practice you should not worry about these implications. However, if you encounter a case where you think a statement is true but not covered by the current implications, please bring it up on Zulip!

Implementation notes #

This file uses custom typeclasses instead of abbreviations of CovariantClass/ContravariantClass because:

They get displayed as classes in the docs. In particular, one can see their list of instances, instead of their instances being invariably dumped to the CovariantClass/ContravariantClass list.
They don't pollute other typeclass searches. Having many abbreviations of the same typeclass for different purposes always felt like a performance issue (more instances with the same key, for no added benefit), and indeed making the classes here abbreviation previous creates timeouts due to the higher number of CovariantClass/ContravariantClass instances.
SMulPosReflectLT/SMulPosReflectLE do not fit in the framework since they relate ≤ on two different types. So we would have to generalise CovariantClass/ContravariantClass to three types and two relations.
Very minor, but the constructors let you work with a : α, h : 0 ≤ a instead of a : {a : α // 0 ≤ a}. This actually makes some instances surprisingly cleaner to prove.
The CovariantClass/ContravariantClass framework is only useful to automate very simple logic anyway. It is easily copied over.

In the future, it would be good to make the corresponding typeclasses in Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean custom typeclasses too.