Mathlib.Algebra.Order.Module.Algebra

algebraMap_mono theorem

: Monotone (algebraMap α β)

Full source

@[mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
  fun a₁ a₂ ha ↦ by
    simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one

Monotonicity of the Algebra Map

Informal description

The algebra map $\text{algebraMap} : \alpha \to \beta$ is a monotone function, meaning that for any $a, b \in \alpha$ with $a \leq b$, we have $\text{algebraMap}(a) \leq \text{algebraMap}(b)$ in $\beta$.

GCongr.algebraMap_le_algebraMap theorem

{a₁ a₂ : α} (ha : a₁ ≤ a₂) : algebraMap α β a₁ ≤ algebraMap α β a₂

Full source

/-- A version of `algebraMap_mono` for use by `gcongr` since it currently does not preprocess
`Monotone` conclusions. -/
@[gcongr] protected lemma GCongr.algebraMap_le_algebraMap {a₁ a₂ : α} (ha : a₁ ≤ a₂) :
    algebraMap α β a₁ ≤ algebraMap α β a₂ := algebraMap_mono _ ha

Inequality Preservation by Algebra Map ($\text{algebraMap}(a_1) \leq \text{algebraMap}(a_2)$ when $a_1 \leq a_2$)

Informal description

For any elements $a_1, a_2$ in an ordered semiring $\alpha$ with $a_1 \leq a_2$, the algebra map $\text{algebraMap} : \alpha \to \beta$ preserves the inequality, i.e., $\text{algebraMap}(a_1) \leq \text{algebraMap}(a_2)$ in the ordered semiring $\beta$.

algebraMap_nonneg theorem

(ha : 0 ≤ a) : 0 ≤ algebraMap α β a

Full source

lemma algebraMap_nonneg (ha : 0 ≤ a) : 0 ≤ algebraMap α β a := by simpa using algebraMap_mono β ha

Nonnegativity Preservation by Algebra Map

Informal description

For any element $a$ in an ordered semiring $\alpha$ such that $0 \leq a$, the algebra map $\text{algebraMap} : \alpha \to \beta$ preserves nonnegativity, i.e., $0 \leq \text{algebraMap}(a)$ in the ordered semiring $\beta$.

algebraMap_le_algebraMap theorem

: algebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂

Full source

@[simp] lemma algebraMap_le_algebraMap : algebraMapalgebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂ := by
  simp [Algebra.algebraMap_eq_smul_one]

Order-Preserving Property of Algebra Map: $\text{algebraMap}(a_1) \leq \text{algebraMap}(a_2) \leftrightarrow a_1 \leq a_2$

Informal description

For any elements $a_1, a_2$ in an ordered semiring $\alpha$, the inequality $\text{algebraMap}(a_1) \leq \text{algebraMap}(a_2)$ holds in the ordered semiring $\beta$ if and only if $a_1 \leq a_2$ in $\alpha$.

algebraMap_strictMono theorem

: StrictMono (algebraMap α β)

Full source

@[mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
  fun a₁ a₂ ha ↦ by
    simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one

Strict Monotonicity of Algebra Homomorphism Between Ordered Semirings

Informal description

The algebra homomorphism $\text{algebraMap} : \alpha \to \beta$ between two ordered semirings is strictly monotone, meaning that for any $a_1, a_2 \in \alpha$, if $a_1 < a_2$, then $\text{algebraMap}(a_1) < \text{algebraMap}(a_2)$.

GCongr.algebraMap_lt_algebraMap theorem

{a₁ a₂ : α} (ha : a₁ < a₂) : algebraMap α β a₁ < algebraMap α β a₂

Full source

/-- A version of `algebraMap_strictMono` for use by `gcongr` since it currently does not preprocess
`Monotone` conclusions. -/
@[gcongr] protected lemma GCongr.algebraMap_lt_algebraMap {a₁ a₂ : α} (ha : a₁ < a₂) :
    algebraMap α β a₁ < algebraMap α β a₂ := algebraMap_strictMono _ ha

Strict Monotonicity of Algebra Map: $\text{algebraMap}(a_1) < \text{algebraMap}(a_2)$ when $a_1 < a_2$

Informal description

For any elements $a_1, a_2$ in an ordered semiring $\alpha$, if $a_1 < a_2$, then the algebra homomorphism $\text{algebraMap} : \alpha \to \beta$ satisfies $\text{algebraMap}(a_1) < \text{algebraMap}(a_2)$ in the ordered semiring $\beta$.

algebraMap_pos theorem

(ha : 0 < a) : 0 < algebraMap α β a

Full source

lemma algebraMap_pos (ha : 0 < a) : 0 < algebraMap α β a := by
  simpa using algebraMap_strictMono β ha

Positivity of Algebra Homomorphism on Positive Elements

Informal description

For any element $a$ in an ordered semiring $\alpha$ such that $0 < a$, the image of $a$ under the algebra homomorphism $\text{algebraMap} : \alpha \to \beta$ to another ordered semiring $\beta$ satisfies $0 < \text{algebraMap}(a)$.

algebraMap_lt_algebraMap theorem

: algebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂

Full source

@[simp] lemma algebraMap_lt_algebraMap : algebraMapalgebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂ := by
  simp [Algebra.algebraMap_eq_smul_one]

Order-Preserving Property of Algebra Maps: $\text{algebraMap}(a_1) < \text{algebraMap}(a_2) \leftrightarrow a_1 < a_2$

Informal description

Let $\alpha$ and $\beta$ be strict ordered semirings with $\beta$ having characteristic zero. For any elements $a_1, a_2 \in \alpha$, the inequality $\text{algebraMap}_{\alpha \to \beta}(a_1) < \text{algebraMap}_{\alpha \to \beta}(a_2)$ holds if and only if $a_1 < a_2$ in $\alpha$.

Mathlib.Meta.Positivity.evalAlgebraMap definition

: PositivityExt

Full source

/-- Extension for `algebraMap`. -/
@[positivity algebraMap _ _ _]
def evalAlgebraMap : PositivityExt where eval {u β} _zβ _pβ e := do
  let ~q(@algebraMap $α _ $instα $instβ $instαβ $a) := e | throwError "not `algebraMap`"
  let pα ← synthInstanceQ q(PartialOrder $α)
  match ← core q(inferInstance) pα a with
  | .positive pa =>
    let _instαSemiring ← synthInstanceQ q(Semiring $α)
    let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
    try
      let _instβSemiring ← synthInstanceQ q(Semiring $β)
      let _instβPartialOrder  ← synthInstanceQ q(PartialOrder $β)
      let _instβIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $β)
      let _instαβsmul ← synthInstanceQ q(SMulPosStrictMono $α $β)
      assertInstancesCommute
      return .positive q(algebraMap_pos $β $pa)
    catch _ =>
      let _instβSemiring ← synthInstanceQ q(Semiring $β)
      let _instβPartialOrder  ← synthInstanceQ q(PartialOrder $β)
      let _instβIsOrderedRing ← synthInstanceQ q(IsOrderedRing $β)
      let _instαβsmul ← synthInstanceQ q(SMulPosMono $α $β)
      assertInstancesCommute
      return .nonnegative q(algebraMap_nonneg $β <| le_of_lt $pa)
  | .nonnegative pa =>
    let _instαSemiring ← synthInstanceQ q(CommSemiring $α)
    let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
    let _instβSemiring ← synthInstanceQ q(Semiring $β)
    let _instβPartialOrder  ← synthInstanceQ q(PartialOrder $β)
    let _instβIsOrderedRing ← synthInstanceQ q(IsOrderedRing $β)
    let _instαβsmul ← synthInstanceQ q(SMulPosMono $α $β)
    assertInstancesCommute
    return .nonnegative q(algebraMap_nonneg $β $pa)
  | _ => pure .none

Positivity extension for algebra maps

Informal description

The `evalAlgebraMap` function is a positivity extension for the `algebraMap` operation, which determines the positivity properties of the image of an element under an algebra map. Given an expression of the form `algebraMap α β a`, where `α` and `β` are semirings with partial orders, the function analyzes the positivity of `a` in `α` and propagates this information to `algebraMap α β a` in `β`. The function proceeds as follows: 1. If `a` is positive in `α`, it checks if `β` is a strictly ordered ring and returns that `algebraMap α β a` is positive in `β`. 2. If `β` is not strictly ordered but is ordered, it returns that `algebraMap α β a` is non-negative. 3. If `a` is non-negative in `α`, it returns that `algebraMap α β a` is non-negative in `β`. 4. Otherwise, it returns no positivity information. This extension ensures that the `positivity` tactic can correctly infer positivity properties of algebra maps based on the properties of their arguments.

TODO