strict weak order in nLab
Context
Relations
Rel, bicategory of relations, allegory
Types of Binary relation
-
left and right euclidean;
-
extensional, well-founded relations.
In higher category theory
(0,1)(0,1)-Category theory
Contents
Idea
A strict total order which is not a connected relation.
Definition
A strict weak order is a strict preorder which is also a cotransitive relation.
These are sometimes called strict partial orders in the literature, but the term “strict partial order” is also used for other order relations in mathematics.
Strict weak orders are used in models of the real numbers which have infinitesimals, such as in the smooth real numbers in synthetic differential geometry, and thus where not every real number not greater than or less than zero is equal to zero.
Properties
Proof
Transitivity of <\lt says that for all x∈Sx \in S and y∈Sy \in S, x<yx \lt y and y<xy \lt x implies x<xx \lt x. However, irreflexivity says that for all xx, x≤xx \leq x is always false. This implies that for all xx and yy, x<yx \lt y and y<xy \lt x is always false, which is precisely the condition of asymmetry.
Preorder of a strict weak order
An important part of a strict weak order is that it is a preorder.
Theorem
The negation of a strict weak order is transitive.
Proof
The contrapositive of cotransitivity says that
for all xx, yy, and zz, if x<yx \lt y or y<zy \lt z is false, then x<zx \lt z is false.
By one of de Morgan's laws, that x<yx \lt y or y<zy \lt z is false is logically to equivalent to that ¬(x<y)\neg(x \lt y) and ¬(y<z)\neg(y \lt z), and substituting this into the original statement results in
if ¬(x<y)\neg(x \lt y) and ¬(y<z)\neg(y \lt z), then ¬(x<z)\neg(x \lt z)
which is precisely transitivity for the negation of the strict weak order.
Theorem
The negation of a strict weak order is reflexive.
Proof
Irreflexivity states that ¬(x<x)\neg (x \lt x) is true, which is precisely reflexivity for the negation of the strict weak order.
Theorem
The negation of a strict weak order is a preorder.
Corollary
The incomparability relation of a strict weak order, ¬(x<y)∧¬(y<x)\neg (x \lt y) \wedge \neg (y \lt x), is an equivalence relation
Proof
For every preorder, (x≤y)∧(y≤x)(x \leq y) \wedge (y \leq x) is an equivalence relation. Since ¬(x<y)\neg (x \lt y) is a preorder, ¬(x<y)∧¬(y<x)\neg (x \lt y) \wedge \neg (y \lt x) is an equivalence relation.
See also
References
- Wikipedia, Weak order
Strict weak orders are called strict partial orders in section 4.1 of:
- Auke Booij, Analysis in univalent type theory (2020) [[etheses:10411, pdf]]
Strict weak orders are used in defining the smooth real numbers in:
- David Jaz Myers, Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory (arXiv:2205.15887)
Last revised on July 10, 2024 at 15:55:25. See the history of this page for a list of all contributions to it.