Ordered algebras #
An ordered algebra is an ordered semiring, which is an algebra over an ordered commutative semiring, for which scalar multiplication is "compatible" with the two orders.
The prototypical example is 2x2 matrices over the reals or complexes (or indeed any C^* algebra)
where the ordering the one determined by the positive cone of positive operators,
i.e. A ≤ B iff B - A = star R * R for some R.
(We don't yet have this example in mathlib.)
Implementation #
Because the axioms for an ordered algebra are exactly the same as those for the underlying
module being ordered, we don't actually introduce a new class, but just use the OrderedSMul
mixin.
Tags #
ordered algebra
theorem
algebraMap_monotone
{R : Type u_1}
{A : Type u_2}
[OrderedCommRing R]
[OrderedRing A]
[Algebra R A]
[OrderedSMul R A]
:
Monotone ⇑(algebraMap R A)