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> distributive lattice 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> distributive lattice </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/11069/#Item_8" 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> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#definition'>Definition</a></li> <li><a href='#alternative_characterizations'>Alternative characterizations</a></li> <li><a href='#examples'>Examples</a></li> <li><a href='#infinitely_distributive_property'>Infinitely distributive property</a></li> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#OppositeCategory'>Finite distributive lattices</a></li> <li><a href='#the_free_distributive_lattice'>The free distributive lattice</a></li> <li><a href='#categorification'>Categorification</a></li> <li><a href='#completion'>Completion</a></li> </ul> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="definition">Definition</h2> <div class="num_defn"> <h6 id="definition_2">Definition</h6> <p>A <strong>distributive lattice</strong> is a <a class="existingWikiWord" href="/nlab/show/lattice">lattice</a> in which <a class="existingWikiWord" href="/nlab/show/join">join</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">\vee</annotation></semantics></math> and <a class="existingWikiWord" href="/nlab/show/meet">meet</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">\wedge</annotation></semantics></math> <em>distribute</em> over each other, in that for all <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,y,z</annotation></semantics></math> in the lattice, the <em>distributivity laws</em> are satisfied:</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</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>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \vee (y \wedge z) = (x \vee y) \wedge (x \vee z)</annotation></semantics></math>,</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</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>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \wedge (y \vee z) = (x \wedge y) \vee (x \wedge z)</annotation></semantics></math>.</li> </ul> </div> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>The nullary forms of distributivity hold in any lattice:</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∨</mo><mo>⊤</mo><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x \vee \top = \top</annotation></semantics></math>,</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∧</mo><mo>⊥</mo><mo>=</mo><mo>⊥</mo></mrow><annotation encoding="application/x-tex">x \wedge \bot = \bot</annotation></semantics></math>.</li> </ul> <p>Distributive lattices and <a class="existingWikiWord" href="/nlab/show/lattice">lattice</a> <a class="existingWikiWord" href="/nlab/show/homomorphisms">homomorphisms</a> form a <a class="existingWikiWord" href="/nlab/show/concrete+category">concrete category</a> <a class="existingWikiWord" href="/nlab/show/DistLat">DistLat</a>.</p> </div> <div class="num_remark"> <h6 id="remark_2">Remark</h6> <p>Any lattice that satisfies one of the two binary distributivity laws must also satisfy the other; isn't that nice? (This may safely be left as an <a class="existingWikiWord" href="/nlab/show/exercise">exercise</a>.) This also means that a distributive lattice is precisely a lattice (or indeed a <a class="existingWikiWord" href="/nlab/show/poset">poset</a>) which is a <a class="existingWikiWord" href="/nlab/show/distributive+category">distributive category</a> (when viewed as a <a class="existingWikiWord" href="/nlab/show/thin+category">thin category</a>.)</p> <p>This convenience does <em>not</em> extend to infinitary distributivity, however.</p> </div> <div class="num_remark"> <h6 id="remark_3">Remark</h6> <p>Each distributivity law holds in one direction in any lattice (the proofs of which may be left as an exercise):</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</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>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \vee (y \wedge z) \leq (x \vee y) \wedge (x \vee z)</annotation></semantics></math></li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</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>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \wedge (y \vee z) \geq (x \wedge y) \vee (x \wedge z)</annotation></semantics></math></li> </ul> <p>As a result, the real content of the definition consists of the converse directions (and as remarked above, either one suffices):</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</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>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \vee (y \wedge z) \geq (x \vee y) \wedge (x \vee z)</annotation></semantics></math></li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</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>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \wedge (y \vee z) \leq (x \wedge y) \vee (x \wedge z)</annotation></semantics></math></li> </ul> </div> <h2 id="alternative_characterizations">Alternative characterizations</h2> <p>As mentioned above, the theory of distributive lattices is self-dual, something that is proved in almost any account (or left as an exercise), but which is not manifestly obvious from the standard definition which chooses one of the two distributivity laws and goes from there. In this section we provide some other characterizations or axiomatizations which <em>are</em> manifestly self-dual.</p> <p>Here is one such characterization:</p> <div class="num_prop" id="sd1"> <h6 id="proposition">Proposition</h6> <p>A lattice is distributive if and only if the identity</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>a</mi><mo>∧</mo><mi>b</mi><mo stretchy="false">)</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∧</mo><mi>c</mi><mo stretchy="false">)</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>b</mi><mo>∧</mo><mi>c</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∨</mo><mi>b</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∨</mo><mi>c</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>b</mi><mo>∨</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(a \wedge b) \vee (a \wedge c) \vee (b \wedge c) = (a \vee b) \wedge (a \vee c) \wedge (b \vee c)</annotation></semantics></math></div> <p>is satisfied.</p> </div> <p>Again this may be left as a (somewhat mechanical) exercise.</p> <p>Perhaps more useful in practice is the characterization in terms of “forbidden sublattices” due to Birkhoff. Namely, introduce the “pentagon” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math> as the 5-element lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⊥</mo><mo>≤</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo>≤</mo><mo>⊤</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\bot \leq a, b, c \leq \top\}</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>≤</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">b \leq c</annotation></semantics></math> and <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 incomparable to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>,</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">b, c</annotation></semantics></math>, so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo><mo>=</mo><mi>a</mi><mo>∧</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">\bot = a \wedge c</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∨</mo><mi>b</mi><mo>=</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">a \vee b = \top</annotation></semantics></math>. Introduce the “thick diamond” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math> as the 5-element lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⊥</mo><mo>≤</mo><mi>a</mi><mo>′</mo><mo>,</mo><mi>b</mi><mo>′</mo><mo>,</mo><mi>c</mi><mo>′</mo><mo>≤</mo><mo>⊤</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\bot \leq a', b', c' \leq \top\}</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>′</mo><mo>,</mo><mi>b</mi><mo>′</mo><mo>,</mo><mi>c</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">a', b', c'</annotation></semantics></math> pairwise incomparable. Both <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math> are self-dual. Birkhoff’s characterization is the following (manifestly self-dual) criterion.</p> <div class="num_theorem"> <h6 id="theorem">Theorem</h6> <p>A lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is distributive if and only if there is no <a class="existingWikiWord" href="/nlab/show/injective+function">embedding</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math> into <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> that preserves binary meets and binary joins.</p> </div> <p>This can be useful for determining distributivity or its failure, especially in cases where one can visualize a lattice via its <a class="existingWikiWord" href="/nlab/show/Hasse+diagram">Hasse diagram</a>.</p> <p>The necessity of the forbidden sublattice condition is clear in view of the fact that the cancellation law stated in the next result fails in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math>. This result gives another self-dual axiomatization of distributive lattices.</p> <div class="num_prop" id="sd2"> <h6 id="proposition_2">Proposition</h6> <p>A lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is distributive if and only if the cancellation law holds: for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>,</mo><mi>z</mi><mo>∈</mo><mi>L</mi></mrow><annotation encoding="application/x-tex">y, z \in L</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>=</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y = z</annotation></semantics></math> whenever <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><mo>∧</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \wedge y = x \wedge z</annotation></semantics></math> and <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><mo>∨</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \vee y = x \vee z</annotation></semantics></math> (for some <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> </div> <div class="proof"> <h6 id="proof">Proof</h6> <p>“Only if”: 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><mo>∧</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \wedge y = x \wedge z</annotation></semantics></math> and <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><mo>∨</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \vee y = x \vee z</annotation></semantics></math>, then</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>=</mo><mi>y</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</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><mi>z</mi></mrow><annotation encoding="application/x-tex">y = y \vee (x \wedge y) = y \vee (x \wedge z) = (y \vee x) \wedge (y \vee z) = (x \vee z) \wedge (y \vee z) = (x \wedge y) \vee z</annotation></semantics></math></div> <p>which implies <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">z \leq y</annotation></semantics></math>, and similarly we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y \leq z</annotation></semantics></math>.</p> <p>“If”: this is harder. Assuming the cancellation law for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math>, we first show <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is modular. Recall from <a class="existingWikiWord" href="/nlab/show/modular+lattice">modular lattice</a> that for any lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>∈</mo><mi>L</mi></mrow><annotation encoding="application/x-tex">a, b \in L</annotation></semantics></math>, there is a covariant <a class="existingWikiWord" href="/nlab/show/Galois+connection">Galois connection</a></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>a</mi><mo>∧</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">]</mo><mo>→</mo><mo stretchy="false">[</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo>∨</mo><mi>b</mi><mo stretchy="false">]</mo><mo>:</mo><mi>x</mi><mo>↦</mo><mi>a</mi><mo>∨</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>⊣</mo><mspace width="thickmathspace"></mspace><mo stretchy="false">(</mo><mo stretchy="false">[</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo>∨</mo><mi>b</mi><mo stretchy="false">]</mo><mo>→</mo><mo stretchy="false">[</mo><mi>a</mi><mo>∧</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">]</mo><mo>:</mo><mi>y</mi><mo>↦</mo><mi>b</mi><mo>∧</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">([a \wedge b, b] \to [a, a \vee b]: x \mapsto a \vee x) \; \dashv \; ([a, a \vee b] \to [a \wedge b, b]: y \mapsto b \wedge y)</annotation></semantics></math></div> <p>and that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is <em>modular</em> if this Galois connection is a <a class="existingWikiWord" href="/nlab/show/Galois+correspondence">Galois correspondence</a> (or <a class="existingWikiWord" href="/nlab/show/adjoint+equivalence">adjoint equivalence</a>) for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a, b</annotation></semantics></math>. Now, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mo stretchy="false">[</mo><mi>a</mi><mo>∧</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">x \in [a \wedge b, b]</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∨</mo><mi>x</mi><mo>=</mo><mi>a</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>b</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∨</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a \vee x = a \vee (b \wedge (a \vee x))</annotation></semantics></math> because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>=</mo><mi>f</mi><mi>g</mi><mi>f</mi></mrow><annotation encoding="application/x-tex">f = f g f</annotation></semantics></math> for any Galois connection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>⊣</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f \dashv g</annotation></semantics></math>. From <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∧</mo><mi>b</mi><mo>≤</mo><mi>x</mi><mo>≤</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a \wedge b \leq x \leq b</annotation></semantics></math> we also have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∧</mo><mi>x</mi><mo>=</mo><mi>a</mi><mo>∧</mo><mi>b</mi><mo>∧</mo><mi>x</mi><mo>=</mo><mi>a</mi><mo>∧</mo><mi>b</mi><mo>=</mo><mi>a</mi><mo>∧</mo><mi>b</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∨</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a \wedge x = a \wedge b \wedge x = a \wedge b = a \wedge b \wedge (a \vee x)</annotation></semantics></math></div> <p>and so by cancellation of the <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>'s, we conclude <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>b</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∨</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x = b \wedge (a \vee x)</annotation></semantics></math>. Similarly (dually), for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mo stretchy="false">[</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo>∨</mo><mi>b</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">y \in [a, a \vee b]</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>=</mo><mi>a</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>b</mi><mo>∧</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">y = a \vee (b \wedge y)</annotation></semantics></math>. Hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is modular.</p> <p>Now we show <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is distributive. Let <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><mo>∈</mo><mi>L</mi></mrow><annotation encoding="application/x-tex">x, y, z \in L</annotation></semantics></math> and consider the three elements</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>u</mi></mtd> <mtd><mo>≔</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>=</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>x</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>v</mi></mtd> <mtd><mo>≔</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>y</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>=</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>y</mi><mo>∨</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>w</mi></mtd> <mtd><mo>≔</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>z</mi><mo>∧</mo><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>x</mi><mo>∧</mo><mi>y</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>=</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>z</mi><mo>∨</mo><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>x</mi><mo>∨</mo><mi>y</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ u & \coloneqq & [x \wedge (y \vee z)] \vee (y \wedge z) & = & [x \vee (y \wedge z)] \wedge (y \vee z) \\ v & \coloneqq & [y \wedge (x \vee z)] \vee (x \wedge z) & = & [y \vee (x \wedge z)] \wedge (x \vee z) \\ w & \coloneqq & [z \wedge (x \vee y)] \vee (x \wedge y) & = & [z \vee (x \wedge y)] \wedge (x \vee y) } </annotation></semantics></math></div> <p>where the non-definitional equalities follow from modularity. Using the first expressions, we compute</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>u</mi><mo>∨</mo><mi>v</mi></mtd> <mtd><mo>=</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∨</mo><mo stretchy="false">[</mo><mi>y</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>=</mo></mtd> <mtd><mo stretchy="false">[</mo><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>∨</mo><mo stretchy="false">[</mo><mi>y</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>=</mo></mtd> <mtd><mo stretchy="false">[</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∨</mo><mi>y</mi><mo stretchy="false">]</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>=</mo></mtd> <mtd><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><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ u \vee v & = & [x \wedge (y \vee z)] \vee (y \wedge z) \vee [y \wedge (x \vee z)] \vee (x \wedge z) \\ & = & [x \wedge (y \vee z)] \vee [y \wedge (x \vee z)] \\ & = & [(x \wedge (y \vee z)) \vee y] \wedge (x \vee z) \\ & = & (x \vee y) \wedge (x \vee z) \wedge (y \vee z) } </annotation></semantics></math></div> <p>where the third and fourth lines use modularity. By symmetry in the letters <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, y, z</annotation></semantics></math>, we also have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>∨</mo><mi>w</mi><mo>=</mo><mi>v</mi><mo>∨</mo><mi>w</mi><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>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">u \vee w = v \vee w = (x \vee y) \wedge (x \vee z) \wedge (y \vee z)</annotation></semantics></math>. Now the second expressions are dual to the first, so by duality we compute</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>∧</mo><mi>v</mi><mo>=</mo><mi>u</mi><mo>∧</mo><mi>w</mi><mo>=</mo><mi>v</mi><mo>∧</mo><mi>w</mi><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>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">u \wedge v = u \wedge w = v \wedge w = (x \wedge y) \vee (x \wedge z) \vee (y \wedge z).</annotation></semantics></math></div> <p>Now by cancellation of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi></mrow><annotation encoding="application/x-tex">u</annotation></semantics></math>'s, we may conclude <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>v</mi><mo>=</mo><mi>w</mi></mrow><annotation encoding="application/x-tex">v = w</annotation></semantics></math>, but in that case we obtain</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>x</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>v</mi><mo>∨</mo><mi>w</mi><mo>=</mo><mi>v</mi><mo>∧</mo><mi>w</mi><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>x</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo><mo>∨</mo><mo stretchy="false">(</mo><mi>y</mi><mo>∧</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x \vee y) \wedge (x \vee z) \wedge (y \vee z) = v \vee w = v \wedge w = (x \wedge y) \vee (x \wedge z) \vee (y \wedge z)</annotation></semantics></math></div> <p>so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is distributive by Proposition <a class="maruku-ref" href="#sd1"></a>.</p> </div> <div class="num_remark"> <h6 id="remark_4">Remark</h6> <p>While the expressions for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>,</mo><mi>v</mi><mo>,</mo><mi>w</mi></mrow><annotation encoding="application/x-tex">u, v, w</annotation></semantics></math> in the preceding proof may look as though they come out of thin air, the underlying idea is that the sublattice of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> generated by <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, y, z</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/image">image</a> of a lattice map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mn>3</mn><mo stretchy="false">)</mo><mo>→</mo><mi>L</mi></mrow><annotation encoding="application/x-tex">F(3) \to L</annotation></semantics></math> out of the free modular lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mn>3</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F(3)</annotation></semantics></math> on three elements. The only obstruction to distributivity in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mn>3</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F(3)</annotation></semantics></math> is the presence of an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math>-sublattice appearing in the center of its <a href="https://golem.ph.utexas.edu/category/2015/09/the_free_modular_lattice_on_3.html#c049685">Hasse diagram</a>. The middle elements of that sublattice correspond to the formal expressions for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>,</mo><mi>v</mi><mo>,</mo><mi>w</mi></mrow><annotation encoding="application/x-tex">u, v, w</annotation></semantics></math> given above, and the proof shows that under the cancellation law, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>=</mo><mi>v</mi><mo>=</mo><mi>w</mi></mrow><annotation encoding="application/x-tex">u = v = w</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math>, making the thick diamond collapse to a point in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> and removing the obstruction to distributivity.</p> </div> <p>From Proposition <a class="maruku-ref" href="#sd2"></a>, it is not very hard to deduce Birkhoff’s theorem. The presence of a copy of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math> in a non-distributive lattice <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> is deduced from a failure of the cancellation law where we have three elements <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, y, z</annotation></semantics></math> with <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><mo>∧</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \wedge y = x \wedge z</annotation></semantics></math>, <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><mo>∨</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \vee y = x \vee z</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>z</mi></mrow><annotation encoding="application/x-tex">y \neq z</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>,</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y, z</annotation></semantics></math> are comparable, say <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y \leq z</annotation></semantics></math>, then the set <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>,</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo>,</mo><mi>x</mi><mo>∨</mo><mi>y</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x \wedge y, x, y, z, x \vee y\}</annotation></semantics></math> forms an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>,</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y, z</annotation></semantics></math> are incomparable, then we have either <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∨</mo><mi>z</mi><mo><</mo><mi>x</mi><mo>∨</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">y \vee z \lt x \vee y</annotation></semantics></math>, or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∧</mo><mi>z</mi><mo>></mo><mi>x</mi><mo>∧</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">y \wedge z \gt x \wedge y</annotation></semantics></math>, or both <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∨</mo><mi>z</mi><mo>=</mo><mi>x</mi><mo>∨</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">y \vee z = x \vee 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>z</mi><mo>=</mo><mi>x</mi><mo>∧</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">y \wedge z = x \wedge y</annotation></semantics></math>; in the first two cases we get an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mn>5</mn></msub></mrow><annotation encoding="application/x-tex">N_5</annotation></semantics></math> (e.g., <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>,</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>y</mi><mo>∨</mo><mi>z</mi><mo>,</mo><mi>x</mi><mo>∨</mo><mi>y</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x \wedge y, x, y, y \vee z, x \vee y\}</annotation></semantics></math> for the first case), and in the third case the set <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>,</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo>,</mo><mi>x</mi><mo>∨</mo><mi>y</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x \wedge y, x, y, z, x \vee y\}</annotation></semantics></math> forms an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mn>3</mn></msub></mrow><annotation encoding="application/x-tex">M_3</annotation></semantics></math>.</p> <h2 id="examples">Examples</h2> <p>Any <a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a>, and even any <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>, is a distributive lattice.</p> <p>Every <a class="existingWikiWord" href="/nlab/show/frame">frame</a> and every <a class="existingWikiWord" href="/nlab/show/sigma-frame"><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>-frame</a> is a distributive lattice.</p> <p>Any <a class="existingWikiWord" href="/nlab/show/bounded+total+order">bounded total order</a> is a distributive lattice.</p> <p>Any <a class="existingWikiWord" href="/nlab/show/linear+order">linear order</a> is a distributive lattice.</p> <p>An <a class="existingWikiWord" href="/nlab/show/integral+domain">integral domain</a> is a <span class="newWikiWord">Prüfer domain<a href="/nlab/new/Pr%C3%BCfer+domain">?</a></span> iff its lattice of <a class="existingWikiWord" href="/nlab/show/ideals">ideals</a> is distributive. The classical example 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">\mathbb{Z}</annotation></semantics></math>; equivalently, the (opposite of the) multiplicative monoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> ordered by divisibility, with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> at the bottom and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> at the top.</p> <p>The lattice of <a class="existingWikiWord" href="/nlab/show/Young+diagrams">Young diagrams</a> ordered by inclusion is distributive.</p> <h2 id="infinitely_distributive_property">Infinitely distributive property</h2> <p>A distributive lattice that is complete (not necessarily <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive</a>) may be <strong>infinitely distributive</strong> or said to satisfiy the <strong>infinite distributive law</strong> :</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><mo stretchy="false">(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>i</mi></munder><msub><mi>y</mi> <mi>i</mi></msub><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>i</mi></munder><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><msub><mi>y</mi> <mi>i</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> x \wedge (\bigvee_i y_i) = \bigvee_i (x\wedge y_i) </annotation></semantics></math></div> <p>This property is sufficient to give the lattice <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a> stucture where the implication <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>⇒</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a\Rightarrow b</annotation></semantics></math> (or <a class="existingWikiWord" href="/nlab/show/exponential+object">exponential object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>b</mi> <mi>a</mi></msup></mrow><annotation encoding="application/x-tex">b^a</annotation></semantics></math>) is:</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>u</mi><mo>⇒</mo><mi>v</mi><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>x</mi><mo>∧</mo><mi>u</mi><mo>≤</mo><mi>v</mi></mrow></munder><mi>x</mi></mrow><annotation encoding="application/x-tex">(u \Rightarrow v) = \bigvee_{x \wedge u \leq v} x</annotation></semantics></math></div> <p>Note that this property does not imply the dual <strong>co-infinitely distributive</strong> property:</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><mo stretchy="false">(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋀</mo> <mi>i</mi></munder><msub><mi>y</mi> <mi>i</mi></msub><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋀</mo> <mi>i</mi></munder><mo stretchy="false">(</mo><mi>x</mi><mo>∨</mo><msub><mi>y</mi> <mi>i</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> x \vee (\bigwedge_i y_i) = \bigwedge_i (x\vee y_i) </annotation></semantics></math></div> <p>Instead this dual gives the lattice <a class="existingWikiWord" href="/nlab/show/co-Heyting+algebra">co-Heyting</a> structure where the co-implication or “subtraction” (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>\</mo></mrow><annotation encoding="application/x-tex">\backslash</annotation></semantics></math>) is</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>u</mi><mo>\</mo><mi>v</mi><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋀</mo> <mrow><mi>u</mi><mo>≤</mo><mi>v</mi><mo>∨</mo><mi>x</mi></mrow></munder><mi>x</mi></mrow><annotation encoding="application/x-tex">(u \backslash v) = \bigwedge_{u \leq v \vee x} x</annotation></semantics></math></div> <p>If a lattice has both properties, as in a <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive lattice</a>, then it has <a class="existingWikiWord" href="/nlab/show/bi-Heyting+algebra">bi-Heyting</a> structure (both Heyting and co-Heyting), but the two exponentials are not necessarily equal.</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>u</mi><mo>⇒</mo><mi>v</mi><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>x</mi><mo>∧</mo><mi>u</mi><mo>≤</mo><mi>v</mi></mrow></munder><mi>x</mi></mrow><annotation encoding="application/x-tex">(u \Rightarrow v) = \bigvee_{x \wedge u \leq v} x</annotation></semantics></math></div> <p>and</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>u</mi><mo>\</mo><mi>v</mi><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋀</mo> <mrow><mi>u</mi><mo>≤</mo><mi>v</mi><mo>∨</mo><mi>x</mi></mrow></munder><mi>x</mi></mrow><annotation encoding="application/x-tex">(u \backslash v) = \bigwedge_{u \leq v \vee x} x</annotation></semantics></math></div> <blockquote> <p>Does it make sense to define “infinitely distributive property” for non-complete lattices? (Something like: “Whenever the join exists, it satisfies the infinite distributive law.”)</p> </blockquote> <h2 id="properties">Properties</h2> <h3 id="OppositeCategory">Finite distributive lattices</h3> <p>Since a finite distributive lattice is <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive</a> it is a bi-Heyting lattice, as shown above.</p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinDistLat</mi></mrow><annotation encoding="application/x-tex">FinDistLat</annotation></semantics></math> be the category of finite distributive lattices and lattice homomorphisms, and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinPoset</mi></mrow><annotation encoding="application/x-tex">FinPoset</annotation></semantics></math> be the category of finite <a class="existingWikiWord" href="/nlab/show/posets">posets</a> and order-preserving functions. These are contravariantly equivalent, thanks to the presence of an <a class="existingWikiWord" href="/nlab/show/ambimorphic+object">ambimorphic object</a>:</p> <p><strong>Proposition.</strong> The <a class="existingWikiWord" href="/nlab/show/opposite+category">opposite category</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinDistLat</mi></mrow><annotation encoding="application/x-tex">FinDistLat</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinPoset</mi></mrow><annotation encoding="application/x-tex">FinPoset</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>FinDistLat</mi> <mi>op</mi></msup><mo>≃</mo><mi>FinPoset</mi><mo>.</mo></mrow><annotation encoding="application/x-tex"> FinDistLat^{op} \simeq FinPoset. </annotation></semantics></math></div> <p>One direction of this equivalence is given by the hom-functor</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 lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mn>2</mn><mo stretchy="false">]</mo><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><msup><mi>FinDistLat</mi> <mi>op</mi></msup><mover><mo>→</mo><mo>≃</mo></mover><mi>FinPoset</mi></mrow><annotation encoding="application/x-tex"> [-,2] \;\colon\; FinDistLat^{op} \stackrel{\simeq}{\to} FinPoset </annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math> is the 2-element distributive lattice and for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>∈</mo><mi>FinDistLat</mi></mrow><annotation encoding="application/x-tex">X \in FinDistLat</annotation></semantics></math>, <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><mn>2</mn><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[X,2]</annotation></semantics></math> is the poset of distributive lattice morphisms 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><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>. The other direction is given by</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 lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mn>2</mn><mo stretchy="false">]</mo><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><msup><mi>FinPoset</mi> <mi>op</mi></msup><mover><mo>→</mo><mo>≃</mo></mover><mi>FinDistLat</mi></mrow><annotation encoding="application/x-tex"> [-,2] \;\colon\; FinPoset^{op} \stackrel{\simeq}{\to} FinDistLat </annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mo>=</mo><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">2 = \{0,1\}</annotation></semantics></math> is the 2-element poset with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo><</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">0 \lt 1</annotation></semantics></math> and for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo>∈</mo><mo lspace="0em" rspace="thinmathspace">FinPoset</mo></mrow><annotation encoding="application/x-tex">Y \in \FinPoset</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Y</mi><mo>,</mo><mn>2</mn><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[Y,2]</annotation></semantics></math> is the distributive lattice of poset morphisms 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><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>.</p> <p>This <strong>Birkhoff duality</strong> is (in one form or another) mentioned in many places; the formulation in terms of hom-functors may be found in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Gavin+C.+Wraith">Gavin C. Wraith</a>, <em>Using the generic interval</em>, Cah. Top. Géom. Diff. Cat. <strong>XXXIV</strong> 4 (1993) pp.259-266. (<a href="http://archive.numdam.org/ARCHIVE/CTGDC/CTGDC_1993__34_4/CTGDC_1993__34_4_259_0/CTGDC_1993__34_4_259_0.pdf">pdf</a>)</li> </ul> <p>The functorial nature of the correspondence means that morphisms of finite posets (i.e. order-preserving maps) naturally correspond to morphisms of finite distributive lattices (i.e. order-preserving maps that also respect meet and join).</p> <p>It follows from Birkhoff’s representation theorem that every finite distributive lattice can be seen as a lattice of sets (i.e. sets with join and meet given by union and intersection) – in particular, sets whose elements are the join-irreducible elements of the lattice. Furthermore, a good intuition for why this duality holds is that either an element is generated as the join of existing elements, or it is join-irreducible. Hence given any existing poset, we can simply add all missing joins, and also a bottom (i.e. the nullary join). By general results (the adjoint functor theorem for posets) this suffices to ensure that all meets exist as well. This is analogous to the free colimit completion of a category, and indeed Birkhoff representation can be seen as a very special case of the Yoneda lemma as applied to (0,1)-category theory (i.e., order theory), since (0,1)-presheaves are functors into Bool rather than Set and hence correspond to <a class="existingWikiWord" href="/nlab/show/lower+set">lower set</a>s.</p> <p>Birkhoff duality does not hold for infinite distributive lattices. However, in the general case of not-necessarily-finite distributive lattices there is a correspondence not to posets, but instead to a class of spaces known as Priestley spaces. This is an instance of a general phenomena known as Stone-type duality.</p> <h3 id="the_free_distributive_lattice">The free distributive lattice</h3> <p>Posets also give rise to a “free” distributive lattice, which is not the same as their Birkhoff dual. Instead, it is formed by the following procedure: First, take the poset of upsets with the reverse ordering (this is the free finite meet completion). Then form the distributive lattice of finitely generated downsets in that.</p> <p>In the case that one begins with a discrete poset (i.e., a set) then the number of elements in the resultant free distributive lattice is known as a Dedekind number, which also counts the number of monotone Boolean functions in <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> variables. Dedekind numbers increase extremely rapidly, and there is no good known closed-form summation to compute them. The first ten (and only known) Dedekind numbers are (starting at <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>=</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n = 0</annotation></semantics></math>): 2, 3, 6, 20, 168, 7581, 7828354, 2414682040998, 56130437228687557907788, and 286386577668298411128469151667598498812366; see <a href="#A000372">OEIS A000372</a>.</p> <h3 id="categorification">Categorification</h3> <p>Every distributive lattice, regarded as a <a class="existingWikiWord" href="/nlab/show/category">category</a> (a <a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a>), is a <em><a class="existingWikiWord" href="/nlab/show/coherent+category">coherent category</a></em>. Conversely, the notion of coherent category may be understood as a <a class="existingWikiWord" href="/nlab/show/categorification">categorification</a> of the notion of distributive lattice. A different categorification is the notion of <a class="existingWikiWord" href="/nlab/show/distributive+category">distributive category</a>.</p> <h3 id="completion">Completion</h3> <p>The <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive</a> <a class="existingWikiWord" href="/nlab/show/algebraic+lattices">algebraic lattices</a> (the <a class="existingWikiWord" href="/nlab/show/frames+of+opens">frames of opens</a> of <a class="existingWikiWord" href="/nlab/show/Alexandroff+locales">Alexandroff locales</a>) form a <a class="existingWikiWord" href="/nlab/show/reflective+subcategory">reflective subcategory</a> of that of all distributive lattices. The reflector is called <em><a class="existingWikiWord" href="/nlab/show/canonical+extension">canonical extension</a></em>.</p> <h2 id="references">References</h2> <ul> <li id="A000372">OEIS sequence <a href="https://oeis.org/A000372">A000372</a></li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on December 29, 2024 at 15:29:55. See the <a href="/nlab/history/distributive+lattice" 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/distributive+lattice" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/11069/#Item_8">Discuss</a><span class="backintime"><a href="/nlab/revision/distributive+lattice/28" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/distributive+lattice" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/distributive+lattice" accesskey="S" class="navlink" id="history" rel="nofollow">History (28 revisions)</a> <a href="/nlab/show/distributive+lattice/cite" style="color: black">Cite</a> <a href="/nlab/print/distributive+lattice" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/distributive+lattice" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>