CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> partial order in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> partial order </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/9525/#Item_7" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="category_theory"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(0,1)</annotation></semantics></math>-Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category+theory">(0,1)-category theory</a></strong>: <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, <a class="existingWikiWord" href="/nlab/show/order+theory">order theory</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">relation between preorders and (0,1)-categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proset">proset</a>, <a class="existingWikiWord" href="/nlab/show/partially+ordered+set">partially ordered set</a> (<a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a>, <a class="existingWikiWord" href="/nlab/show/total+order">total order</a>, <a class="existingWikiWord" href="/nlab/show/linear+order">linear order</a>)</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/top">top</a>, <a class="existingWikiWord" href="/nlab/show/true">true</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bottom">bottom</a>, <a class="existingWikiWord" href="/nlab/show/false">false</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monotone+function">monotone function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/implication">implication</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/filter">filter</a>, <a class="existingWikiWord" href="/nlab/show/interval">interval</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lattice">lattice</a>, <a class="existingWikiWord" href="/nlab/show/semilattice">semilattice</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/meet">meet</a>, <a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a>, <a class="existingWikiWord" href="/nlab/show/and">and</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/join">join</a>, <a class="existingWikiWord" href="/nlab/show/logical+disjunction">logical disjunction</a>, <a class="existingWikiWord" href="/nlab/show/or">or</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+element">compact element</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lattice+of+subobjects">lattice of subobjects</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/complete+lattice">complete lattice</a>, <a class="existingWikiWord" href="/nlab/show/algebraic+lattice">algebraic lattice</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/distributive+lattice">distributive lattice</a>, <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive lattice</a>, <a class="existingWikiWord" href="/nlab/show/canonical+extension">canonical extension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperdoctrine">hyperdoctrine</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+hyperdoctrine">first-order</a>, <a class="existingWikiWord" href="/nlab/show/Boolean+hyperdoctrine">Boolean</a>, <a class="existingWikiWord" href="/nlab/show/coherent+hyperdoctrine">coherent</a>, <a class="existingWikiWord" href="/nlab/show/tripos">tripos</a></li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/regular+element">regular element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/frame">frame</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> </ul> <h2 id="theorems">Theorems</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/Stone+duality">Stone duality</a></li> </ul> </div></div> <h4 id="category_theory_2">Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></p> <h2 id="sidebar_concepts">Concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> </li> </ul> <h2 id="sidebar_universal_constructions">Universal constructions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit">limit</a>/<a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weighted+limit">weighted limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/end">end</a>/<a class="existingWikiWord" href="/nlab/show/coend">coend</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kan+extension">Kan extension</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Isbell+duality">Isbell duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monadicity+theorem">monadicity theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+lifting+theorem">adjoint lifting theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tannaka+duality">Tannaka duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gabriel-Ulmer+duality">Gabriel-Ulmer duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/small+object+argument">small object argument</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freyd-Mitchell+embedding+theorem">Freyd-Mitchell embedding theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></p> </li> </ul> <h2 id="sidebar_extensions">Extensions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf+and+topos+theory">sheaf and topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+category+theory">enriched category theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> </li> </ul> <h2 id="sidebar_applications">Applications</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/applications+of+%28higher%29+category+theory">applications of (higher) category theory</a></li> </ul> <div> <p> <a href="/nlab/edit/category+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definitions'>Definitions</a></li> <ul> <li><a href='#as_a_set_with_extra_structure'>As a set with extra structure</a></li> <li><a href='#as_a_preorder_with_antisymmetry'>As a preorder with antisymmetry</a></li> <ul> <li><a href='#in_dependent_type_theory'>In dependent type theory</a></li> </ul> <li><a href='#AsACategoryWithExtraProperties'>As a category with extra properties</a></li> <li><a href='#monotone_functions'>Monotone functions</a></li> <li><a href='#intervals'>Intervals</a></li> <li><a href='#kinds_of_posets'>Kinds of posets</a></li> <li><a href='#in_higher_category_theory'>In higher category theory</a></li> </ul> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#ExtensionToLinearOrder'>Extension to linear order</a></li> <li><a href='#LocalesFromPosets'>Locales from posets – Alexandroff topology</a></li> <li><a href='#cauchy_completion'>Cauchy completion</a></li> <li><a href='#in_univalent_universes'>In univalent universes</a></li> </ul> <li><a href='#examples'>Examples</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <em>partial order</em> on a set is a way of ordering its elements to say that some elements precede others, but allowing for the possibility that two elements may be incomparable without being the same. This is the fundamental notion in <a class="existingWikiWord" href="/nlab/show/order+theory">order theory</a>.</p> <p>By regarding the ordering <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> as the existence of a unique <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a>, preorders may be regarded as certain <a class="existingWikiWord" href="/nlab/show/categories">categories</a> (namely, <a class="existingWikiWord" href="/nlab/show/thin+categories">thin categories</a>). This category is sometimes called the <em>order category</em> associated to a partial order; see <a href="#AsACategoryWithExtraProperties">below</a> for details.</p> <h2 id="definitions">Definitions</h2> <h3 id="as_a_set_with_extra_structure">As a set with extra structure</h3> <p>A poset may be understood as a <a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/extra+structure">extra structure</a>.</p> <p>Given a <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, a <strong>partial order</strong> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a (binary) <a class="existingWikiWord" href="/nlab/show/relation">relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> with the following properties:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/reflexive+relation">reflexivity</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x \leq x</annotation></semantics></math> always;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/transitive+relation">transitivity</a>: if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mo>≤</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \leq y \leq z</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \leq z</annotation></semantics></math>;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/antisymmetric+relation">antisymmetry</a>: if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x \leq y \leq x</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math>.</p> </li> </ul> <p>A <strong>poset</strong> is a set equipped with a partial order.</p> <h3 id="as_a_preorder_with_antisymmetry">As a preorder with antisymmetry</h3> <p>A poset is precisely a <a class="existingWikiWord" href="/nlab/show/proset">proset</a> satisfying the extra condition that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x \leq y \leq x</annotation></semantics></math> implies that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math>.</p> <h4 id="in_dependent_type_theory">In dependent type theory</h4> <p>In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, the identity type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math> representing equality is not necessarily valued in <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>. As a result, a naive translation of the set theoretic definition of a partial order from a preorder above doesn’t work. Instead, one has to postulate an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> between the identity type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math> and the condition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x \leq y \leq x</annotation></semantics></math>:</p> <p>A <strong>partial order</strong> is a preorder <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> with an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">antisym</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">(</mo><mi>x</mi><msub><mo>=</mo> <mi>X</mi></msub><mi>y</mi><mo stretchy="false">)</mo><mo>≃</mo><mo stretchy="false">(</mo><mi>x</mi><mo><</mo><mi>y</mi><mo stretchy="false">)</mo><mo>×</mo><mo stretchy="false">(</mo><mi>y</mi><mo><</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{antisym}(x, y):(x =_X y) \simeq (x \lt y) \times (y \lt x)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">x:X</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">y:X</annotation></semantics></math>.</p> <p>Equivalently, one could <a class="existingWikiWord" href="/nlab/show/inductively+define">inductively define</a> a function</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>X</mi><mo>⊢</mo><mi mathvariant="normal">idToOrd</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">(</mo><mi>x</mi><msub><mo>=</mo> <mi>X</mi></msub><mi>y</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>x</mi><mo><</mo><mi>y</mi><mo stretchy="false">)</mo><mo>×</mo><mo stretchy="false">(</mo><mi>y</mi><mo><</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:X, y:X \vdash \mathrm{idToOrd}(x, y):(x =_X y) \to (x \lt y) \times (y \lt x)</annotation></semantics></math></div> <p>on reflexivity of the <a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> by reflexivity of the preorder</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">idToSymCon</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi mathvariant="normal">id</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≔</mo><msub><mi mathvariant="normal">refl</mi> <mo>≤</mo></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{idToSymCon}(x, x)(\mathrm{id}_X(x)) \coloneqq \mathrm{refl}_{\leq}(x)</annotation></semantics></math></div> <p>Then, a partial order is a preorder such that the defined function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">idToOrd</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{idToOrd}(x, y)</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">x:X</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">y:X</annotation></semantics></math>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">antisym</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>y</mi><mo>:</mo><mi>X</mi></mrow></munder><mi mathvariant="normal">isEquiv</mi><mo stretchy="false">(</mo><mi mathvariant="normal">idToOrd</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{antisym}:\prod_{x:X} \prod_{y:X} \mathrm{isEquiv}(\mathrm{idToOrd}(x, y))</annotation></semantics></math></div> <p>In either case, since the preorder is valued in propositions, the antisymmetry axiom ensures that the partial order is an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>.</p> <h3 id="AsACategoryWithExtraProperties">As a category with extra properties</h3> <p>A poset <a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">may be understood</a> as a <a class="existingWikiWord" href="/nlab/show/category">category</a> with <a class="existingWikiWord" href="/nlab/show/extra+property">extra property</a>, sometimes called its <em>order category</em>.</p> <p>A <strong>poset</strong> <a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">is</a> a <a class="existingWikiWord" href="/nlab/show/category">category</a> such that:</p> <ul> <li> <p>for any <a class="existingWikiWord" href="/nlab/show/pair">pair</a> of <a class="existingWikiWord" href="/nlab/show/objects">objects</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x, y</annotation></semantics></math>, there is at most one morphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math></p> </li> <li> <p>if there is a morphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> and a morphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> (which by the above implies that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/isomorphic">isomorphic</a>), then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math>.</p> </li> </ul> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">Equivalently</a>, this says that a poset is a <a class="existingWikiWord" href="/nlab/show/skeletal+category">skeletal</a> <a class="existingWikiWord" href="/nlab/show/thin+category">thin</a> category, or equivalently a skeletal <a class="existingWikiWord" href="/nlab/show/category+enriched">category enriched</a> over the <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a> or equivalently a skeletal <a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a>. (See also at <em><a class="existingWikiWord" href="/nlab/show/enriched+poset">enriched poset</a></em>).</p> <p>When we do this, we are soon <a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">led to contemplate</a> a slight generalization of partial orders: namely <a class="existingWikiWord" href="/nlab/show/preorder">preorders</a>. The reason is that the antisymmetry law, saying that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \le y</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \le x</annotation></semantics></math> imply <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math>, violates the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> in a certain sense. (On the other hand, it does not violate it if taken as a <em>definition</em> of <a class="existingWikiWord" href="/nlab/show/equality">equality</a>.)</p> <h3 id="monotone_functions">Monotone functions</h3> <p>The morphisms of partially ordered sets are <a class="existingWikiWord" href="/nlab/show/monotone+functions">monotone functions</a>; a <strong>monotone function</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> from a poset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> to a poset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/function">function</a> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> (seen as <a class="existingWikiWord" href="/nlab/show/structured+sets">structured sets</a>) that preserves <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mspace width="thickmathspace"></mspace><mo>⇒</mo><mspace width="thickmathspace"></mspace><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>f</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex"> x \leq y \;\Rightarrow\; f(x) \leq f(y) .</annotation></semantics></math></div> <p>Equivalently, it is a <a class="existingWikiWord" href="/nlab/show/functor">functor</a> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> (seen as certain categories).</p> <p>In this way, posets form a <a class="existingWikiWord" href="/nlab/show/category">category</a> <a class="existingWikiWord" href="/nlab/show/Pos">Pos</a>.</p> <h3 id="intervals">Intervals</h3> <p>A (closed bounded) <strong><a class="existingWikiWord" href="/nlab/show/interval">interval</a></strong> in a poset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a set of the form</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">]</mo><mo>=</mo><mo stretchy="false">{</mo><mi>r</mi><mo>∈</mo><mi>C</mi><mo stretchy="false">|</mo><mi>x</mi><mo>≤</mo><mi>r</mi><mo>≤</mo><mi>y</mi><mo stretchy="false">}</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">[x,y] = \{r\in C|x\le r\le y\}.</annotation></semantics></math></div> <p>A poset is <strong><a class="existingWikiWord" href="/nlab/show/locally+finite+poset">locally finite</a></strong> if every closed bounded interval is finite.</p> <h3 id="kinds_of_posets">Kinds of posets</h3> <p>A poset with a <a class="existingWikiWord" href="/nlab/show/top+element">top element</a> and <a class="existingWikiWord" href="/nlab/show/bottom+element">bottom element</a> is called <strong>bounded</strong>. (But note that a <em><a class="existingWikiWord" href="/nlab/show/subset">subset</a></em> of a poset may be bounded without being a bounded as a poset in its own right.) More generally, it is <strong>bounded above</strong> if it is has a top element and <strong>bounded below</strong> if it has a bottom element.</p> <p>A poset with all finite <a class="existingWikiWord" href="/nlab/show/meets">meets</a> and <a class="existingWikiWord" href="/nlab/show/joins">joins</a> is called a <strong><a class="existingWikiWord" href="/nlab/show/lattice">lattice</a></strong>; if it has only one or the other, it is still a <strong><a class="existingWikiWord" href="/nlab/show/semilattice">semilattice</a></strong>.</p> <p>A poset in which every finite set has an upper bound (but perhaps not a <em>least</em> upper bound, that is a join) is a <strong><a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a></strong>.</p> <p>As remarked above, a poset in which each interval <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[x,y]</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a> is called <strong>locally finite</strong> or a <strong><a class="existingWikiWord" href="/nlab/show/causet">causet</a></strong>.</p> <p>A poset with a bounding <a class="existingWikiWord" href="/nlab/show/countable+set">countable subset</a> is called <strong><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>σ</mi></mrow><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-bounded</strong>. That is, the poset is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>σ</mi></mrow><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-bounded above if there exists a sequence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>x</mi> <mi>n</mi></msub><msubsup><mo stretchy="false">)</mo> <mrow><mi>n</mi><mo>=</mo><mn>1</mn></mrow> <mi>N</mi></msubsup></mrow><annotation encoding="application/x-tex">(x_n)_{n=1}^{N}</annotation></semantics></math> (where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math> is a natural number or infinity) such that for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> in the poset there is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>m</mi></msub></mrow><annotation encoding="application/x-tex">x_m</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><msub><mi>x</mi> <mi>m</mi></msub></mrow><annotation encoding="application/x-tex">y \leq x_m</annotation></semantics></math>. (The poset is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>σ</mi></mrow><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-bounded below if we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>m</mi></msub><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x_m \leq y</annotation></semantics></math> instead.) Note that every bounded poset is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>σ</mi></mrow><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-bounded, but not conversely. Note that some authorities require <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi><mo>=</mo><mn>∞</mn></mrow><annotation encoding="application/x-tex">N = \infty</annotation></semantics></math>; this makes a difference only for the empty poset (we say it is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>σ</mi></mrow><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-bounded, they say it is not).</p> <h3 id="in_higher_category_theory">In higher category theory</h3> <p>A poset can be understood as a <a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a>. This suggests an obvious <a class="existingWikiWord" href="/nlab/show/vertical+categorification">vertical categorification</a> of the notion of poset to that of <a class="existingWikiWord" href="/nlab/show/n-poset">n-poset</a>.</p> <h2 id="properties">Properties</h2> <h3 id="ExtensionToLinearOrder">Extension to linear order</h3> <div class="num_prop" id="LinearExtension"> <h6 id="proposition">Proposition</h6> <p>On a <a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a>, every <a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a> may be <a class="existingWikiWord" href="/nlab/show/linear+extension+of+a+partial+order">extended</a> to a <a class="existingWikiWord" href="/nlab/show/linear+order">linear order</a>.</p> <p>For non-finite sets this still holds with the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>.</p> </div> <p>See at <em><a class="existingWikiWord" href="/nlab/show/linear+extension+of+a+partial+order">linear extension of a partial order</a></em> <a href="linear+extension+of+a+partial+order#LinearExtensionOfAPartialOrder">this Prop.</a>.</p> <h3 id="LocalesFromPosets">Locales from posets – Alexandroff topology</h3> <div class="num_defn"> <h6 id="definition">Definition</h6> <p>For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> a poset, write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Up</mi><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Up(P)</annotation></semantics></math> for the <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> whose underlying <a class="existingWikiWord" href="/nlab/show/set">set</a> is the underlying set of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> and whose <a class="existingWikiWord" href="/nlab/show/open+subset">open subset</a>s are the <em>upward closed subsets</em> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>: those subsets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>⊂</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">U \subset P</annotation></semantics></math> with the property that</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∈</mo><mi>U</mi><mo stretchy="false">)</mo><mi>and</mi><mo stretchy="false">(</mo><mi>x</mi><mo>≤</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⇒</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∈</mo><mi>U</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> ((x \in U) and (x \leq y)) \Rightarrow (y \in U) \,. </annotation></semantics></math></div> <p>This is called the <strong><a class="existingWikiWord" href="/nlab/show/Alexandroff+topology">Alexandroff topology</a></strong> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>.</p> </div> <div class="num_prop" id="UpIfFFAndPreservesLimits"> <h6 id="proposition_2">Proposition</h6> <p>This construction naturally extends to a <a class="existingWikiWord" href="/nlab/show/full+and+faithful+functor">full and faithful functor</a>.</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Up</mi><mo>:</mo></mrow><annotation encoding="application/x-tex">Up : </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Poset">Poset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Top">Top</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a>.</p> </div> <div class="num_prop"> <h6 id="proposition_3">Proposition</h6> <p>For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> a poset, there is a <a class="existingWikiWord" href="/nlab/show/natural+equivalence">natural equivalence</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>Up</mi><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><mo stretchy="false">[</mo><mi>P</mi><mo>,</mo><mi>Set</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex"> Sh(Up(P)) \simeq [P,Set] </annotation></semantics></math></div> <p>between the <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a> on the <a class="existingWikiWord" href="/nlab/show/locale">locale</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Up</mi><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Up(P)</annotation></semantics></math> and the category of <a class="existingWikiWord" href="/nlab/show/copresheaves">copresheaves</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>.</p> </div> <p>For more see <a class="existingWikiWord" href="/nlab/show/Alexandroff+topology">Alexandroff topology</a>.</p> <h3 id="cauchy_completion">Cauchy completion</h3> <p>Every poset is a <a class="existingWikiWord" href="/nlab/show/Cauchy+complete+category">Cauchy complete category</a>. Posets are the Cauchy completions of <a class="existingWikiWord" href="/nlab/show/prosets">prosets</a>. (<a href="#Rosolini">Rosolini</a>)</p> <h3 id="in_univalent_universes">In univalent universes</h3> <p>In <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, every <a class="existingWikiWord" href="/nlab/show/type">type</a> with a partial order in a <a class="existingWikiWord" href="/nlab/show/univalent+universe">univalent universe</a> is a poset. (<a href="#Tosun">Tosun</a>, <a href="#ANST">Ahrens, North, Shulman, Tsementzis</a>)</p> <h2 id="examples">Examples</h2> <ul> <li> <p>The <a class="existingWikiWord" href="/nlab/show/function+algebra">function algebra</a> of <a class="existingWikiWord" href="/nlab/show/rational+number">rational</a>-valued <a class="existingWikiWord" href="/nlab/show/functions">functions</a> on any <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a partial order.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/function+algebra">function algebra</a> of <a class="existingWikiWord" href="/nlab/show/Cauchy+real+number">Cauchy real</a>-valued functions on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a partial order. In fact, it is the <a class="existingWikiWord" href="/nlab/show/Cauchy+completion">Cauchy completion</a> of the function algebra of <a class="existingWikiWord" href="/nlab/show/rational+number">rational</a>-valued <a class="existingWikiWord" href="/nlab/show/functions">functions</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>.</p> </li> <li> <p>More generally, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/vector+space">vector space</a> on the <a class="existingWikiWord" href="/nlab/show/rational+numbers">rational numbers</a> with a <a class="existingWikiWord" href="/nlab/show/quadratic+form">quadratic form</a>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a partial order, and its Cauchy completion is a vector space of same dimension on the <a class="existingWikiWord" href="/nlab/show/Cauchy+real+numbers">Cauchy real numbers</a> with a quadratic form. In particular, the Cauchy <a class="existingWikiWord" href="/nlab/show/complex+numbers">complex numbers</a> and the <a class="existingWikiWord" href="/nlab/show/Gaussian+rationals">Gaussian rationals</a> are partial orders.</p> </li> <li> <p>In a logic with implications, the set of propositions is partially ordered with respect to the implication as a relation.</p> </li> </ul> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">relation between preorders and (0,1)-categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/preorder">preorder</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/continuous+poset">continuous poset</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Noetherian+poset">Noetherian poset</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+poset">enriched poset</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/specialization+topology">specialization topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/prefix+order">prefix order</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/partially+ordered+object">partially ordered object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Thomason+model+structure">Thomason model structure</a></p> </li> </ul> <h2 id="references">References</h2> <ul> <li>Richard P. Stanley, Enumerative <a class="existingWikiWord" href="/nlab/show/combinatorics">combinatorics</a>, vol I <a href="http://www-math.mit.edu/~rstan/ec/ec1.pdf">pdf</a></li> </ul> <p><a class="existingWikiWord" href="/nlab/show/Cauchy+completion">Cauchy completion</a> of prosets and posets is discussed in</p> <ul id="Rosolini"> <li>G. Rosolini, <em>A note on Cauchy completeness for preorders</em> (<a href="http://rivista.math.unipr.it/fulltext/1999-2s/06.pdf">pdf</a>)</li> </ul> <p>Here are some references on <a class="existingWikiWord" href="/nlab/show/directed+homotopy+theory">directed homotopy theory</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Marco+Grandis">Marco Grandis</a>, <em>Directed homotopy theory, I. The fundamental category</em> (<a href="http://arxiv.org/abs/math.AT/0111048">arXiv</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tim+Porter">Tim Porter</a>, <em>Enriched categories and models for spaces of evolving states</em>, Theoretical Computer Science, 405, (2008), pp. 88–100.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tim+Porter">Tim Porter</a>, <em>Enriched categories and models for spaces of dipaths. A discussion document and overview of some techniques</em> (<a href="http://drops.dagstuhl.de/opus/volltexte/2007/898/pdf/06341.PorterTimothy.Paper.898.pdf">pdf</a>)</p> </li> </ul> <p>Posets in <a class="existingWikiWord" href="/nlab/show/univalent+universes">univalent universes</a> in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> are discussed in</p> <ul> <li id="Tosun"> <p>Ayberk Tosun, Formal Topology in Univalent Foundations <a href="https://odr.chalmers.se/handle/20.500.12380/301098">pdf</a></p> </li> <li id="ANST"> <p>Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle (<a href="https://arxiv.org/abs/2102.06275">abs:2102.06275</a>)</p> </li> </ul> <p>On posets that are <a class="existingWikiWord" href="/nlab/show/cofibrant+objects">cofibrant objects</a> in the Thomason model structure:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Roman+Bruckner">Roman Bruckner</a>, <a class="existingWikiWord" href="/nlab/show/Christoph+Pegel">Christoph Pegel</a>, <em>Cofibrant objects in the Thomason Model Structure</em>, [<a href="http://arxiv.org/abs/1603.05448">arXiv:0808.4108</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Roman+Bruckner">Roman Bruckner</a>, <em>Abstract Homotopy Theory and the Thomason Model Structure</em>, PhD thesis, Bremen 2016 [<a href="http://nbn-resolving.de/urn:nbn:de:gbv:46-00105527-15">gbv:46-00105527-15</a>, <a href="https://media.suub.uni-bremen.de/bitstream/elib/1120/1/00105527-1.pdf">pdf</a>]</p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on August 31, 2024 at 21:03:23. See the <a href="/nlab/history/partial+order" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/partial+order" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/9525/#Item_7">Discuss</a><span class="backintime"><a href="/nlab/revision/partial+order/64" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/partial+order" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/partial+order" accesskey="S" class="navlink" id="history" rel="nofollow">History (64 revisions)</a> <a href="/nlab/show/partial+order/cite" style="color: black">Cite</a> <a href="/nlab/print/partial+order" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/partial+order" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>