Mathlib.Algebra.Order.Nonneg.Ring

Module docstring

{"# Bundled ordered algebra instance on the type of nonnegative elements

This file defines instances and prove some properties about the nonnegative elements {x : α // 0 ≤ x} of an arbitrary type α.

Currently we only state instances and states some simp/norm_cast lemmas.

When α is ℝ, this will give us some properties about ℝ≥0.

Main declarations

{x : α // 0 ≤ x} is a CanonicallyLinearOrderedAddCommMonoid if α is a LinearOrderedRing.

Implementation Notes

Instead of {x : α // 0 ≤ x} we could also use Set.Ici (0 : α), which is definitionally equal. However, using the explicit subtype has a big advantage: when writing an element explicitly with a proof of nonnegativity as ⟨x, hx⟩, the hx is expected to have type 0 ≤ x. If we would use Ici 0, then the type is expected to be x ∈ Ici 0. Although these types are definitionally equal, this often confuses the elaborator. Similar problems arise when doing cases on an element.

The disadvantage is that we have to duplicate some instances about Set.Ici to this subtype. "}

Nonneg.isOrderedAddMonoid instance

[AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid { x : α // 0 ≤ x }

Full source

instance isOrderedAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
    IsOrderedAddMonoid { x : α // 0 ≤ x } :=
  Subtype.coe_injective.isOrderedAddMonoid _ Nonneg.coe_zero (fun _ _ => rfl) fun _ _ => rfl

Ordered Additive Monoid Structure on Nonnegative Elements

Informal description

For any additive commutative monoid $\alpha$ with a partial order that makes it an ordered additive monoid, the subtype $\{x \in \alpha \mid 0 \leq x\}$ inherits an ordered additive monoid structure from $\alpha$.

Nonneg.isOrderedCancelAddMonoid instance

[AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] : IsOrderedCancelAddMonoid { x : α // 0 ≤ x }

Full source

instance isOrderedCancelAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
    IsOrderedCancelAddMonoid { x : α // 0 ≤ x } :=
  Subtype.coe_injective.isOrderedCancelAddMonoid _ Nonneg.coe_zero (fun _ _ => rfl) fun _ _ => rfl

Ordered Cancellative Additive Monoid Structure on Nonnegative Elements

Informal description

For any additive commutative monoid $\alpha$ with a partial order that makes it an ordered cancellative additive monoid, the subtype $\{x \in \alpha \mid 0 \leq x\}$ inherits an ordered cancellative additive monoid structure from $\alpha$.

Nonneg.isOrderedRing instance

[Semiring α] [PartialOrder α] [IsOrderedRing α] : IsOrderedRing { x : α // 0 ≤ x }

Full source

instance isOrderedRing [Semiring α] [PartialOrder α] [IsOrderedRing α] :
    IsOrderedRing { x : α // 0 ≤ x } :=
  Subtype.coe_injective.isOrderedRing _ Nonneg.coe_zero Nonneg.coe_one
    (fun _ _ => rfl) (fun _ _=> rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ => rfl

Ordered Semiring Structure on Nonnegative Elements

Informal description

For any ordered semiring $\alpha$, the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements inherits an ordered semiring structure from $\alpha$.

Nonneg.isStrictOrderedRing instance

[Semiring α] [PartialOrder α] [IsStrictOrderedRing α] : IsStrictOrderedRing { x : α // 0 ≤ x }

Full source

instance isStrictOrderedRing [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
    IsStrictOrderedRing { x : α // 0 ≤ x } :=
  Subtype.coe_injective.isStrictOrderedRing _ Nonneg.coe_zero Nonneg.coe_one
    (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl

Strict Ordered Ring Structure on Nonnegative Elements

Informal description

For any semiring $\alpha$ with a partial order and a strict ordered ring structure, the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements inherits a strict ordered ring structure from $\alpha$.

Nonneg.existsAddOfLE instance

[Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] : ExistsAddOfLE { x : α // 0 ≤ x }

Full source

instance existsAddOfLE [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] :
    ExistsAddOfLE { x : α // 0 ≤ x } :=
  ⟨fun {a b} h ↦ by
    rw [← Subtype.coe_le_coe] at h
    obtain ⟨c, hc⟩ := exists_add_of_le h
    refine ⟨⟨c, ?_⟩, by simp [Subtype.ext_iff, hc]⟩
    rw [← add_zero a.val, hc] at h
    exact le_of_add_le_add_left h⟩

Existence of Addition for Nonnegative Elements in Strict Ordered Semirings

Informal description

For any semiring $\alpha$ with a partial order and a strict ordered ring structure, if $\alpha$ has the property that for any elements $a \leq b$ there exists $c$ such that $a + c = b$, then the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements also has this property.

Nonneg.nontrivial instance

[Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : Nontrivial { x : α // 0 ≤ x }

Full source

instance nontrivial [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] :
    Nontrivial { x : α // 0 ≤ x } :=
  ⟨⟨0, 1, fun h => zero_ne_one (congr_arg Subtype.val h)⟩⟩

Nontriviality of Nonnegative Elements in Strict Ordered Semirings

Informal description

For any semiring $\alpha$ with a linear order and a strict ordered ring structure, the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements is nontrivial (contains at least two distinct elements).

Nonneg.linearOrderedCommMonoidWithZero instance

[CommSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : LinearOrderedCommMonoidWithZero { x : α // 0 ≤ x }

Full source

instance linearOrderedCommMonoidWithZero [CommSemiring α] [LinearOrder α] [IsStrictOrderedRing α] :
    LinearOrderedCommMonoidWithZero { x : α // 0 ≤ x } :=
  { Nonneg.commSemiring, Nonneg.isOrderedRing with
    mul_le_mul_left := fun _ _ h c ↦ mul_le_mul_of_nonneg_left h c.prop }

Nonnegative Elements Form a Linearly Ordered Commutative Monoid with Zero

Informal description

For any commutative semiring $\alpha$ with a linear order and strict ordered ring structure, the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements forms a linearly ordered commutative monoid with zero. This means it has a commutative monoid structure with a zero element, a linear order compatible with the monoid operation, and zero as the least element.

Nonneg.canonicallyOrderedAdd instance

[Ring α] [PartialOrder α] [IsOrderedRing α] : CanonicallyOrderedAdd { x : α // 0 ≤ x }

Full source

instance canonicallyOrderedAdd [Ring α] [PartialOrder α] [IsOrderedRing α] :
    CanonicallyOrderedAdd { x : α // 0 ≤ x } :=
  { le_self_add := fun _ b => le_add_of_nonneg_right b.2
    exists_add_of_le := fun {a b} h =>
      ⟨⟨b - a, sub_nonneg_of_le h⟩, Subtype.ext (add_sub_cancel _ _).symm⟩ }

Nonnegative Elements Form a Canonically Ordered Additive Monoid

Informal description

For any ring $\alpha$ with a partial order that makes it an ordered ring, the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements forms a canonically ordered additive monoid. This means that the order relation on the nonnegative elements coincides with the subtractibility relation: for any two nonnegative elements $a$ and $b$, $a \leq b$ if and only if there exists a nonnegative element $c$ such that $b = a + c$.

Nonneg.noZeroDivisors instance

[Semiring α] [PartialOrder α] [IsOrderedRing α] [NoZeroDivisors α] : NoZeroDivisors { x : α // 0 ≤ x }

Full source

instance noZeroDivisors [Semiring α] [PartialOrder α] [IsOrderedRing α] [NoZeroDivisors α] :
    NoZeroDivisors { x : α // 0 ≤ x } :=
  { eq_zero_or_eq_zero_of_mul_eq_zero := by
      rintro ⟨a, ha⟩ ⟨b, hb⟩
      simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self]}

Nonnegative Elements of an Ordered Semiring Have No Zero Divisors

Informal description

For any semiring $\alpha$ with a partial order that forms an ordered semiring and has no zero divisors, the subtype $\{x : \alpha \mid 0 \leq x\}$ also has no zero divisors.

Nonneg.orderedSub instance

[Ring α] [LinearOrder α] [IsStrictOrderedRing α] : OrderedSub { x : α // 0 ≤ x }

Full source

instance orderedSub [Ring α] [LinearOrder α] [IsStrictOrderedRing α] :
    OrderedSub { x : α // 0 ≤ x } :=
  ⟨by
    rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩
    simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le,
      Subtype.coe_mk]⟩

Ordered Subtraction Structure on Nonnegative Elements of a Strict Ordered Ring

Informal description

For any linearly ordered ring $\alpha$ that is a strict ordered ring, the subtype $\{x \in \alpha \mid 0 \leq x\}$ of nonnegative elements forms an ordered subtraction structure. This means that for any nonnegative elements $a, b, c$, the inequality $a - b \leq c$ holds if and only if $a \leq c + b$.