Ordered algebras #
This file proves properties of algebras where both rings are ordered compatibly.
TODO #
positivity extension for algebraMap
theorem
algebraMap_mono
{α : Type u_1}
(β : Type u_2)
[OrderedCommSemiring α]
[OrderedSemiring β]
[Algebra α β]
[SMulPosMono α β]
:
Monotone ⇑(algebraMap α β)
theorem
GCongr.algebraMap_le_algebraMap
{α : Type u_1}
(β : Type u_2)
[OrderedCommSemiring α]
[OrderedSemiring β]
[Algebra α β]
[SMulPosMono α β]
{a₁ a₂ : α}
(ha : a₁ ≤ a₂)
:
(algebraMap α β) a₁ ≤ (algebraMap α β) a₂
A version of algebraMap_mono for use by gcongr since it currently does not preprocess
Monotone conclusions.
theorem
algebraMap_nonneg
{α : Type u_1}
(β : Type u_2)
[OrderedCommSemiring α]
[OrderedSemiring β]
[Algebra α β]
[SMulPosMono α β]
{a : α}
(ha : 0 ≤ a)
:
0 ≤ (algebraMap α β) a
@[simp]
theorem
algebraMap_le_algebraMap
{α : Type u_1}
{β : Type u_2}
[OrderedCommSemiring α]
[StrictOrderedSemiring β]
[Algebra α β]
[SMulPosMono α β]
[SMulPosReflectLE α β]
{a₁ a₂ : α}
:
(algebraMap α β) a₁ ≤ (algebraMap α β) a₂ ↔ a₁ ≤ a₂
theorem
algebraMap_strictMono
{α : Type u_1}
(β : Type u_2)
[OrderedCommSemiring α]
[StrictOrderedSemiring β]
[Algebra α β]
[SMulPosStrictMono α β]
:
StrictMono ⇑(algebraMap α β)
theorem
GCongr.algebraMap_lt_algebraMap
{α : Type u_1}
(β : Type u_2)
[OrderedCommSemiring α]
[StrictOrderedSemiring β]
[Algebra α β]
[SMulPosStrictMono α β]
{a₁ a₂ : α}
(ha : a₁ < a₂)
:
(algebraMap α β) a₁ < (algebraMap α β) a₂
A version of algebraMap_strictMono for use by gcongr since it currently does not preprocess
Monotone conclusions.
theorem
algebraMap_pos
{α : Type u_1}
(β : Type u_2)
[OrderedCommSemiring α]
[StrictOrderedSemiring β]
[Algebra α β]
[SMulPosStrictMono α β]
{a : α}
(ha : 0 < a)
:
0 < (algebraMap α β) a
@[simp]
theorem
algebraMap_lt_algebraMap
{α : Type u_1}
{β : Type u_2}
[OrderedCommSemiring α]
[StrictOrderedSemiring β]
[Algebra α β]
[SMulPosStrictMono α β]
{a₁ a₂ : α}
[SMulPosReflectLT α β]
:
(algebraMap α β) a₁ < (algebraMap α β) a₂ ↔ a₁ < a₂
Extension for algebraMap.