Physlib

PhyslibAlpha.Mathematics.Order.StrongUnit

Strong units

i. Overview

A strong unit of an ordered abelian group is an element `u` such that every element lies below some natural multiple of `u`; an order unit is a nonnegative strong unit. A group with a nonnegative strong unit is directed: any two elements lie below a common multiple of `u`. In a nontrivial group a strong unit is nonzero.

ii. Key results

  • `IsStrongUnit` : every element lies below a natural multiple of `u`.
  • `IsStrongUnit.exists_two_sided` : every element lies between opposite multiples of `u`.
  • `IsStrongUnit.isDirectedOrder` : a nonnegative strong unit makes the order directed.
  • `IsStrongUnit.ne_zero` : a strong unit of a nontrivial group is nonzero.
  • `IsOrderUnit` : a nonnegative strong unit.

iii. Table of contents

  • A. Strong units
  • B. Order units

A. Strong units

B. Order units

8 declarations

definition

Strong unit uu (x≤n⋅ux \le n \cdot u)

In an ordered abelian group GG, an element u∈Gu \in G is defined to be a **strong unit** if for every element x∈Gx \in G, there exists a natural number n∈Nn \in \mathbb{N} such that x≤n⋅ux \le n \cdot u, where n⋅un \cdot u denotes the nn-fold sum of uu with itself.

theorem

Every element lies between opposite multiples of a non-negative strong unit uu (−n⋅u≤x≤n⋅u-n \cdot u \leq x \leq n \cdot u)

Let GG be an ordered abelian group. If u∈Gu \in G is a non-negative strong unit (that is, u≥0u \ge 0 and for every a∈Ga \in G there exists k∈Nk \in \mathbb{N} such that a≤k⋅ua \le k \cdot u), then for any element x∈Gx \in G, there exists a natural number n∈Nn \in \mathbb{N} such that −n⋅u≤x≤n⋅u-n \cdot u \leq x \leq n \cdot u, where n⋅un \cdot u denotes the nn-fold sum of uu with itself.

theorem

A Nonnegative Strong Unit implies a Directed Order

Let GG be an ordered abelian group. If u∈Gu \in G is a strong unit (meaning for every x∈Gx \in G, there exists a natural number n∈Nn \in \mathbb{N} such that x≤n⋅ux \le n \cdot u) and uu is non-negative (0≤u0 \le u), then the order on GG is a directed order, meaning that for any two elements in GG, there exists a common upper bound.

theorem

A Strong Unit of a Nontrivial Group is Nonzero

Let GG be a nontrivial ordered abelian group. If u∈Gu \in G is a strong unit, meaning that for every element x∈Gx \in G there exists a natural number n∈Nn \in \mathbb{N} such that x≤n⋅ux \le n \cdot u, then u≠0u \neq 0.

theorem

Every element lies between two opposite multiples of an order unit

Let GG be an ordered abelian group and let u∈Gu \in G be an order unit. For any element x∈Gx \in G, there exists a natural number n∈Nn \in \mathbb{N} such that −(n⋅u)≤x-(n \cdot u) \le x and x≤n⋅ux \le n \cdot u.

theorem

An order unit implies the group is a directed order

Let GG be an ordered abelian group. If GG has an order unit uu (a nonnegative element such that for every x∈Gx \in G, there exists a natural number nn such that x≤n⋅ux \leq n \cdot u), then GG is a directed order. That is, for any two elements x,y∈Gx, y \in G, there exists an element z∈Gz \in G such that x≤zx \leq z and y≤zy \leq z.

theorem

Finitely many elements are bounded above by a non-negative multiple of an order unit

Let GG be an ordered abelian group and uu be an order unit of GG. For any finite collection of elements {xi}i∈I\{x_i\}_{i \in I} in GG, there exists a non-negative real number μ≥0\mu \geq 0 such that xi≤μ⋅ux_i \leq \mu \cdot u for all i∈Ii \in I.

theorem

For an order unit uu in a nontrivial space, 0≤c⋅u  ⟹  0≤c0 \le c \cdot u \implies 0 \le c

Let GG be a nontrivial ordered abelian group and let uu be an order unit of GG. For any real number cc, if the scalar multiple c⋅uc \cdot u is non-negative (i.e., 0≤c⋅u0 \le c \cdot u), then the factor cc must also be non-negative (i.e., 0≤c0 \le c).