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> finite set (changes) in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="noindex,nofollow" /> <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> finite set (changes) </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/diff/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/12198/#Item_17" 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"> <p class="show_diff"> Showing changes from revision #66 to #67: <ins class="diffins">Added</ins> | <del class="diffdel">Removed</del> | <del class="diffmod">Chan</del><ins class="diffmod">ged</ins> </p> <p>\tableofcontents</p> <p>\section{Introduction}</p> <p>A <em>finite set</em> is, roughly speaking, a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> with only finitely many <a class='existingWikiWord' href='/nlab/show/diff/element'>elements</a>. There are a number of ways to make this precise.</p> <p>Classically, the finite sets are the <a class='existingWikiWord' href='/nlab/show/diff/compact+object'>finitely presentable objects</a> in <a class='existingWikiWord' href='/nlab/show/diff/Set'>Set</a>. Constructively, the same is true if <em>finitely presented</em> is properly interpreted, see there for details.</p> <p>The category <a class='existingWikiWord' href='/nlab/show/diff/FinSet'>FinSet</a> of finite sets and functions between them is a prime example of an <a class='existingWikiWord' href='/nlab/show/diff/topos'>elementary topos</a> which is not a <a class='existingWikiWord' href='/nlab/show/diff/Grothendieck+topos'>Grothendieck topos</a>. It is essentially the subject matter of <a class='existingWikiWord' href='/nlab/show/diff/combinatorics'>combinatorics</a>; it is fundamental in the subject of <a class='existingWikiWord' href='/nlab/show/diff/structure+type'>structure types</a>.</p> <p>\section{Definitions}</p> <p>\subsection{Standard definition}</p> <p>We can for example make the following definition.</p> <p>\begin{defn} A <strong>finite set</strong> is a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_1' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> for which there exists a <a class='existingWikiWord' href='/nlab/show/diff/bijection'>bijection</a> between <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_2' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> and the set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_3' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>n</mi><mo stretchy='false'>]</mo><mo>≔</mo><mo stretchy='false'>{</mo><mi>k</mi><mo>∈</mo><mi>ℕ</mi><mo stretchy='false'>|</mo><mi>k</mi><mo><</mo><mi>n</mi><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'>[n] \coloneqq \{k\in \mathbb{N} | k\lt n\}</annotation></semantics></math> for some <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_4' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi><mo>∈</mo><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>n\in \mathbb{N}</annotation></semantics></math>, where <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_5' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{N}</annotation></semantics></math> is the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a>. \end{defn}</p> <p id='Constructivist'>\subsection{Finiteness constructively and internally}</p> <p>\subsubsection{Variations}</p> <p>In <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>, and internally to a <a class='existingWikiWord' href='/nlab/show/diff/topos'>topos</a>, a number of classically equivalent notions of finiteness become distinguishable:</p> <ul> <li> <p>A set is <strong><a class='existingWikiWord' href='/nlab/show/diff/finite+object'>finite</a></strong> (for emphasis <strong>Bishop-finite</strong> or <strong><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_6' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math>-finite</strong>) if (as above) it admits a <a class='existingWikiWord' href='/nlab/show/diff/bijection'>bijection</a> with <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_7' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>n</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[n]</annotation></semantics></math> for some <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural number</a> <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_8' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi></mrow><annotation encoding='application/x-tex'>n</annotation></semantics></math>.</p> </li> <li> <p>A set is <strong><a class='existingWikiWord' href='/nlab/show/diff/finite+object'>subfinite</a></strong> (or <strong><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_9' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mover><mi>B</mi><mo stretchy='false'>˜</mo></mover></mrow><annotation encoding='application/x-tex'>\tilde{B}</annotation></semantics></math>-finite</strong>) if it admits an <a class='existingWikiWord' href='/nlab/show/diff/injection'>injection</a> into some finite set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_10' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>n</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[n]</annotation></semantics></math>; that is, it is a <a class='existingWikiWord' href='/nlab/show/diff/subset'>subset</a> of a finite set.</p> </li> <li> <p>A set is <strong>finitely indexed</strong> (or <strong><a class='existingWikiWord' href='/nlab/show/diff/finite+set'>Kuratowski-finite</a></strong>, <strong><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_11' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>K</mi></mrow><annotation encoding='application/x-tex'>K</annotation></semantics></math>-finite</strong>, or even sometimes, confusingly, <em>subfinite</em>) if it admits a <a class='existingWikiWord' href='/nlab/show/diff/surjection'>surjection</a> from some finite set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_12' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>n</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[n]</annotation></semantics></math>; that is, it is a <a class='existingWikiWord' href='/nlab/show/diff/quotient+set'>quotient set</a> of a finite set.</p> </li> <li> <p>A set is <strong>subfinitely indexed</strong> (or <strong><a class='existingWikiWord' href='/nlab/show/diff/finite+object'>Kuratowski-subfinite</a></strong> or <strong><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_13' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mover><mi>K</mi><mo stretchy='false'>˜</mo></mover></mrow><annotation encoding='application/x-tex'>\tilde{K}</annotation></semantics></math>-finite</strong>) if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set; that is, it is a <a class='existingWikiWord' href='/nlab/show/diff/subquotient'>subquotient set</a> of a finite set.</p> </li> <li> <p>A set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_14' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> is <strong><a class='existingWikiWord' href='/nlab/show/diff/finite+object'>Dedekind-finite</a></strong> if it satisfies one of the following:</p> <ul> <li>any <a class='existingWikiWord' href='/nlab/show/diff/injection'>injection</a> <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_15' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>↪</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>X\hookrightarrow X</annotation></semantics></math> must be a <a class='existingWikiWord' href='/nlab/show/diff/bijection'>bijection</a>.</li> <li>for any function <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_16' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mi>ℕ</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>f\colon \mathbb{N} \to X</annotation></semantics></math> from the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a>, there exist <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_17' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi><mo>,</mo><mi>m</mi></mrow><annotation encoding='application/x-tex'>n,m</annotation></semantics></math> with <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_18' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi><mo>≠</mo><mi>m</mi></mrow><annotation encoding='application/x-tex'>n \ne m</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_19' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>n</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>m</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(n) = f(m)</annotation></semantics></math>.</li> </ul> <p>In contrast to the previous three notions, Dedekind-finite <a class='existingWikiWord' href='/nlab/show/diff/infinite+set'>infinite sets</a> can coexist with <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a>, although <a class='existingWikiWord' href='/nlab/show/diff/countable+choice'>countable choice</a> suffices to banish them. The above two versions of Dedekind-finiteness are equivalent with excluded middle, but constructively they may differ. In addition, there are other forms of Dedekind-finiteness that are strictly stronger even with excluded middle; see <a href='https://mathoverflow.net/q/410013/'>this MO question</a> for instance.</p> </li> </ul> <p>In constructive mathematics, one is usually interested in the finite sets, although the finitely indexed sets are also sometimes useful, as are the Dedekind-finite sets in the second sense.</p> <p>\subsubsection{Properties and relationships}</p> <p>Of course, we have</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_20' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd /> <mtd /> <mtd><mi>finitely</mi><mspace width='thickmathspace' /><mi>indexed</mi></mtd></mtr> <mtr><mtd /> <mtd><mo>⇗</mo></mtd> <mtd /> <mtd><mo>⇘</mo></mtd></mtr> <mtr><mtd><mi>finite</mi></mtd> <mtd /> <mtd /> <mtd /> <mtd><mi>subfinitely</mi><mspace width='thickmathspace' /><mi>indexed</mi></mtd></mtr> <mtr><mtd /> <mtd><mo>⇘</mo></mtd> <mtd /> <mtd><mo>⇗</mo></mtd></mtr> <mtr><mtd /> <mtd /> <mtd><mi>subfinite</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding='application/x-tex'> \array{ & & finitely\;indexed\\ & \neArrow & & \seArrow\\ finite & & & & subfinitely\;indexed\\ & \seArrow & & \neArrow\\ & & subfinite } </annotation></semantics></math></div> <p>Moreover:</p> <ul> <li> <p>Finite and subfinite sets have <a class='existingWikiWord' href='/nlab/show/diff/decidable+equality'>decidable equality</a>. Conversely, any <a class='existingWikiWord' href='/nlab/show/diff/complement'>complemented</a> subset of a finite set is finite.</p> </li> <li> <p>Finite sets are closed under finite limits and colimits.</p> </li> <li> <p>A finitely indexed set with decidable equality must actually be finite. For it is then the quotient of a decidable equivalence relation, hence a coequalizer of finite sets. In particular, a set which is both finitely indexed and subfinite must be finite, i.e. the above “commutative square” of implications is also a “pullback”.</p> </li> <li> <p>In particular, a set with a <a class='existingWikiWord' href='/nlab/show/diff/split+epimorphism'>split surjection</a> from <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_21' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>n</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[n]</annotation></semantics></math> is finite, since it has both a surjection from and an injection into <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_22' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>n</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[n]</annotation></semantics></math>.</p> </li> <li> <p>Finite sets are always <a class='existingWikiWord' href='/nlab/show/diff/projective+object'>projective</a>; that is, the “finite <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>axiom of choice</a>” always holds.</p> </li> <li> <p>However, if a finite set with <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_23' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn></mrow><annotation encoding='application/x-tex'>2</annotation></semantics></math> elements (or any set, finite or not, with at least <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_24' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn></mrow><annotation encoding='application/x-tex'>2</annotation></semantics></math> distinct elements) is <a class='existingWikiWord' href='/nlab/show/diff/choice+object'>choice</a>, or if every finitely-indexed set (or even any <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_25' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn></mrow><annotation encoding='application/x-tex'>2</annotation></semantics></math>-indexed set) is projective, then the logic must be classical (see <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> for a proof).</p> </li> <li> <p>Finite sets are also Dedekind-finite (in either sense).</p> </li> <li> <p>If <em><a class='existingWikiWord' href='/nlab/show/diff/filtered+category'>filtered category</a></em> means <em>admitting cocones of every Bishop-finite diagram</em>, then a set is Bishop-finite iff it is a <a class='existingWikiWord' href='/nlab/show/diff/compact+object'>finitely presented object</a> in Set and it is Kuratowski-finite iff it is a <a class='existingWikiWord' href='/nlab/show/diff/finitely+generated+object'>finitely generated object</a> in Set.</p> </li> </ul> <p id='Finitist'>\subsubsection{Finiteness without infinity}</p> <p>All of the above definitions except for Dedekind-finiteness only make sense given the set of natural numbers. However, they can all be rephrased to make sense even without the <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+infinity'>axiom of infinity</a> in <a class='existingWikiWord' href='/nlab/show/diff/set+theory'>set theory</a>, and thus in a topos without a <a class='existingWikiWord' href='/nlab/show/diff/natural+numbers+object'>natural numbers object</a>. Basically, you define (for a given set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_26' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>) the concept of ‘collection of subsets of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_27' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> that includes all of the finite subsets’ by requiring it to be closed under inductive operations appropriate for the sense of ‘finite’ that you want; then <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_28' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is finite if and only if it is an element of all such collections. Namely, for any set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_29' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> we define the following subsets of the <a class='existingWikiWord' href='/nlab/show/diff/power+set'>power set</a> <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_30' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>P</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P(S)</annotation></semantics></math>.</p> <ul> <li><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_31' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>K</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>K(S)</annotation></semantics></math> is the smallest subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_32' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>P</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P(S)</annotation></semantics></math> containing the empty set and closed under the operation <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_33' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>↦</mo><mi>A</mi><mo>∪</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>A \mapsto A \cup B</annotation></semantics></math> for <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_34' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> a subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_35' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_36' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> a <a class='existingWikiWord' href='/nlab/show/diff/singleton'>singleton</a> in <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_37' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>. Then <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_38' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is finitely-indexed iff <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_39' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>∈</mo><mi>K</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>S \in K(S)</annotation></semantics></math>. Note that <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_40' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>K</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>K(S)</annotation></semantics></math> is also the free <a class='existingWikiWord' href='/nlab/show/diff/semilattice'>semilattice</a> generated by <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_41' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>.</li> <li><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_42' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mover><mi>K</mi><mo stretchy='false'>˜</mo></mover><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\tilde{K}(S)</annotation></semantics></math> is the smallest subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_43' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>P</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P(S)</annotation></semantics></math> containing the empty set and closed under the operation <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_44' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>↦</mo><mi>A</mi><mo>∪</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>A \mapsto A \cup B</annotation></semantics></math> for <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_45' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> a subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_46' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_47' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> a <a class='existingWikiWord' href='/nlab/show/diff/subsingleton'>subsingleton</a> in <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_48' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>. Then <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_49' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is subfinitely-indexed iff <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_50' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>∈</mo><mover><mi>K</mi><mo stretchy='false'>˜</mo></mover><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>S \in \tilde{K}(S)</annotation></semantics></math>.</li> <li><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_51' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>B(S)</annotation></semantics></math> is the smallest subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_52' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>P</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P(S)</annotation></semantics></math> containing the empty set and closed under the operation <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_53' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>↦</mo><mi>A</mi><mo>∪</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>A \mapsto A \cup B</annotation></semantics></math> for <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_54' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> a subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_55' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_56' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> a singleton in <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_57' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> <a class='existingWikiWord' href='/nlab/show/diff/disjoint+subsets'>disjoint</a> from <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_58' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>. Then <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_59' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is finite iff <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_60' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>∈</mo><mi>B</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>S \in B(S)</annotation></semantics></math>.</li> <li><math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_61' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mover><mi>B</mi><mo stretchy='false'>˜</mo></mover><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\tilde{B}(S)</annotation></semantics></math> is the smallest subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_62' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>P</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P(S)</annotation></semantics></math> containing the empty set and closed under the operation <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_63' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>↦</mo><mi>A</mi><mo>∪</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>A \mapsto A \cup B</annotation></semantics></math> for <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_64' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> a subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_65' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_66' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> a subsingleton in <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_67' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> disjoint from <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_68' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>. Then <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_69' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is subfinite iff <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_70' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>∈</mo><mover><mi>B</mi><mo stretchy='false'>˜</mo></mover><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>S \in \tilde{B}(S)</annotation></semantics></math>.</li> </ul> <p>In addition, finite sets are <a class='existingWikiWord' href='/nlab/show/diff/decidable+subset'>decidable subsets</a> of themselves, so one could use the set of decidable subsets <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_71' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mn>2</mn> <mi>S</mi></msup></mrow><annotation encoding='application/x-tex'>2^S</annotation></semantics></math> in the definition of finite set instead of <a class='existingWikiWord' href='/nlab/show/diff/power+set'>power sets</a>:</p> <ul> <li>Let <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_72' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>B(S)</annotation></semantics></math> denote the smallest subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_73' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mn>2</mn> <mi>S</mi></msup></mrow><annotation encoding='application/x-tex'>2^S</annotation></semantics></math> containing the empty set and closed under the operation <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_74' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>↦</mo><mi>A</mi><mo>∪</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>A \mapsto A \cup B</annotation></semantics></math> for <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_75' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> a decidable subset of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_76' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_77' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> a singleton in <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_78' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> <a class='existingWikiWord' href='/nlab/show/diff/disjoint+subsets'>disjoint</a> from <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_79' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>. Then a set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_80' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is finite iff <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_81' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>∈</mo><mi>B</mi><mo stretchy='false'>(</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>S \in B(S)</annotation></semantics></math>.</li> </ul> <p>The definitions of subfinite, finitely indexed, and subfinitely indexed follow from above:</p> <ul> <li> <p>A set is <a class='existingWikiWord' href='/nlab/show/diff/finite+object'>subfinite</a> if it admits an <a class='existingWikiWord' href='/nlab/show/diff/injection'>injection</a> into some finite set.</p> </li> <li> <p>A set is finitely indexed if it admits a <a class='existingWikiWord' href='/nlab/show/diff/surjection'>surjection</a> from some finite set.</p> </li> <li> <p>A set is subfinitely indexed if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set.</p> </li> </ul> <p id='External'>\subsection{In a topos}</p> <p>In a topos, there are both “external” and “internal” versions of all the above notions of finiteness, depending on whether we interpret their meaning “globally” or in the <a class='existingWikiWord' href='/nlab/show/diff/internal+logic'>internal logic</a> of the topos. See <a class='existingWikiWord' href='/nlab/show/diff/finite+object'>finite object</a>.</p> <p>\section{Properties of the category of finite sets}</p> <p>The <a class='existingWikiWord' href='/nlab/show/diff/category'>category</a> <a class='existingWikiWord' href='/nlab/show/diff/FinSet'>FinSet</a> of finite sets is <a class='existingWikiWord' href='/nlab/show/diff/equivalence+of+categories'>equivalent</a> to that of finite <a class='existingWikiWord' href='/nlab/show/diff/Boolean+algebra'>Boolean algebras</a> by the <a class='existingWikiWord' href='/nlab/show/diff/power+set'>power set</a>-<a class='existingWikiWord' href='/nlab/show/diff/functor'>functor</a>. See at <em><a href='FinSet#OppositeCategory'>FinSet – Opposite category</a></em> for details and see at <em><a class='existingWikiWord' href='/nlab/show/diff/Stone+duality'>Stone duality</a></em> for more.</p> <p>\section{Viewing as schemes}</p> <p>Every finite set can be viewed as an <a class='existingWikiWord' href='/nlab/show/diff/affine+scheme'>affine scheme</a>. Indeed, since a <em>finite</em> coproduct of affine schemes <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_82' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><msub><mi>R</mi> <mi>i</mi></msub></mrow><annotation encoding='application/x-tex'>Spec R_i</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_83' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>i</mi><mo>=</mo><mn>1</mn><mo>,</mo><mi>…</mi><mo>,</mo><mi>n</mi></mrow><annotation encoding='application/x-tex'>i=1,\ldots,n</annotation></semantics></math>, is again affine, <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_84' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><mo stretchy='false'>(</mo><msub><mi>R</mi> <mn>1</mn></msub><mo>×</mo><mi>⋯</mi><mo>×</mo><msub><mi>R</mi> <mi>n</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Spec (R_1 \times \cdots \times R_n)</annotation></semantics></math>, given a finite set <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_85' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>, the coproduct of <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_86' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> many copies of the terminal scheme, <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_87' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><mi>ℤ</mi></mrow><annotation encoding='application/x-tex'>Spec \mathbb{Z}</annotation></semantics></math>, is the affine scheme <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_88' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><mo stretchy='false'>(</mo><msup><mi>ℤ</mi> <mi>X</mi></msup><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Spec (\mathbb{Z}^X)</annotation></semantics></math>.</p> <p>Equipping <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_89' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> with a <a class='existingWikiWord' href='/nlab/show/diff/total+order'>total order</a>, we can view it (up to isomorphism, that is, <a class='existingWikiWord' href='/nlab/show/diff/bijection'>bijection</a>) as a set of <a class='existingWikiWord' href='/nlab/show/diff/integer'>integers</a> <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_90' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo>{</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>x</mi> <mi>n</mi></msub><mo>}</mo></mrow></mrow><annotation encoding='application/x-tex'>\left\{ x_1, \ldots, x_n \right\}</annotation></semantics></math>. One can then view <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_91' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> as the set of zeroes of the set of <a class='existingWikiWord' href='/nlab/show/diff/polynomial'>polynomials</a> in one variable <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_92' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> given by <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_93' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo>{</mo><mi>y</mi><mo>−</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><mi>y</mi><mo>−</mo><msub><mi>x</mi> <mi>n</mi></msub><mo>}</mo></mrow></mrow><annotation encoding='application/x-tex'>\left\{ y - x_1, \ldots, y - x_n \right\}</annotation></semantics></math>, or of the single polynomial given by the product of all these.</p> <p>Thus, one can view <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_94' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> as the affine scheme (over <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_95' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><mo stretchy='false'>(</mo><mi>ℤ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Spec(\mathbb{Z})</annotation></semantics></math>) given as the <a class='existingWikiWord' href='/nlab/show/diff/spectrum+of+a+commutative+ring'>commutative ring spectrum</a> <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_96' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><mrow><mo>(</mo><mi>ℤ</mi><mo stretchy='false'>[</mo><mi>y</mi><mo stretchy='false'>]</mo><mo stretchy='false'>/</mo><mi>I</mi><mo>)</mo></mrow></mrow><annotation encoding='application/x-tex'>Spec\left( \mathbb{Z}[y] / I \right)</annotation></semantics></math>, where <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_97' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>I</mi></mrow><annotation encoding='application/x-tex'>I</annotation></semantics></math> is the ideal generated by the afore-mentioned polynomial(s). Since <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_98' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℤ</mi><mo stretchy='false'>[</mo><mi>y</mi><mo stretchy='false'>]</mo><mo stretchy='false'>/</mo><mi>I</mi><mo>≃</mo><msup><mi>ℤ</mi> <mi>n</mi></msup></mrow><annotation encoding='application/x-tex'>\mathbb{Z}[y] / I \simeq \mathbb{Z}^n</annotation></semantics></math>, this agrees with the above description, but additionally lets us see <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_99' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> as a <a class='existingWikiWord' href='/nlab/show/diff/closed+subscheme'>closed subscheme</a> of the affine line <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_100' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Spec</mi><mo stretchy='false'>(</mo><mi>ℤ</mi><mo stretchy='false'>[</mo><mi>y</mi><mo stretchy='false'>]</mo><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Spec(\mathbb{Z}[y])</annotation></semantics></math>.</p> <p>One can view <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_101' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> as a ‘constant scheme’ over any other base scheme <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_102' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi></mrow><annotation encoding='application/x-tex'>Y</annotation></semantics></math> by <a class='existingWikiWord' href='/nlab/show/diff/base+change'>base change</a>, that is, by means of the canonical <a class='existingWikiWord' href='/nlab/show/diff/projection'>projection</a> morphism <math class='maruku-mathml' display='inline' id='mathml_1c307abfd67b3b42e8caa02a04194250f5a75dc3_103' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi><mo>×</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>Y \times X \to Y</annotation></semantics></math>.</p> <p>\section{Related concepts}</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/infinite+set'>infinite set</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/hereditarily+finite+set'>hereditarily finite set</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/FinSet'>FinSet</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/space+of+finite+subsets'>space of finite subsets</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+object'>finite object</a>, <a class='existingWikiWord' href='/nlab/show/diff/finite+type'>finite type</a></p> </li> <li> <p>the <a class='existingWikiWord' href='/nlab/show/diff/cardinal+number'>cardinality</a> of a finite set is a <a class='existingWikiWord' href='/nlab/show/diff/finite+number'>finite number</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/cofinite+subset'>cofinite subset</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/countable+ordinal'>countable ordinal</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite-dimensional+vector+space'>finite-dimensional vector space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+homotopy+type'>finite homotopy type</a>,</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/finite+CW+complex'>finite CW-complex</a>, <a class='existingWikiWord' href='/nlab/show/diff/finite+spectrum'>finite spectrum</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/profinite+space'>profinite set</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+cover'>finite cover</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+graph'>finite graph</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+category'>finite category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+limit'>finite limit</a>, <a class='existingWikiWord' href='/nlab/show/diff/L-finite+category'>L-finite limit</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finite+homotopy+type'>finite homotopy type</a>, <a class='existingWikiWord' href='/nlab/show/diff/homotopy+type+with+finite+homotopy+groups'>π-finite homotopy type</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/locally+finite+type'>locally finite type</a></p> </li> </ul> <p>\section{References}</p> <p>Original articles:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Kazimierz+Kuratowski'>C. Kuratowski</a>, <em>Sur la notion d’ensemble fini</em> , Fund. Math. <strong>I</strong> (1920) pp.130-131. (<a href='http://matwbn.icm.edu.pl/ksiazki/fm/fm1/fm1117.pdf'>pdf</a>)</li> </ul> <p>See also:</p> <ul> <li>Wikipedia, <em><a href='https://en.wikipedia.org/wiki/Finite_set'>Finite set</a></em></li> </ul> <p>Discussion of notions of finite sets in <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>:</p> <ul> <li id='SpiwackCoquand10'><a class='existingWikiWord' href='/nlab/show/diff/Arnaud+Spiwack'>Arnaud Spiwack</a>, <a class='existingWikiWord' href='/nlab/show/diff/Thierry+Coquand'>Thierry Coquand</a>, <em>Constructively Finite?</em>, in: <em>Contribuciones cientifícas en honor de Mirian Andrés Gómez</em>, Universidad de La Rioja (2010) 217-230 [ISBN:978-84-96487-50-5, inria-00503917]</li> </ul> <p>Formalization in <a class='existingWikiWord' href='/nlab/show/diff/homotopy+type+theory'>homotopy type theory</a>/<a class='existingWikiWord' href='/nlab/show/diff/univalent+foundations+for+mathematics'>univalent foundations of mathematics</a>:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Dan+Frumin'>Dan Frumin</a>, <a class='existingWikiWord' href='/nlab/show/diff/Herman+Geuvers'>Herman Geuvers</a>, <a class='existingWikiWord' href='/nlab/show/diff/L%C3%A9on+Gondelman'>Léon Gondelman</a>, <a class='existingWikiWord' href='/nlab/show/diff/Niels+van+der+Weide'>Niels van der Weide</a>, <em>Finite Sets in Homotopy Type Theory</em>, in <em>CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs</em> (2018) 201–214 [[doi:10.1145/3167085](https://doi.org/10.1145/3167085), <a href='http://cs.ru.nl/~nweide/FiniteSetsInHoTT.pdf'>pdf</a>]</li> </ul> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> </div> <div class="revisedby"> <p> Last revised on December 22, 2023 at 14:01:47. See the <a href="/nlab/history/finite+set" 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/finite+set" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/12198/#Item_17">Discuss</a><span class="backintime"><a href="/nlab/revision/diff/finite+set/66" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/finite+set" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Hide changes</a><a href="/nlab/history/finite+set" accesskey="S" class="navlink" id="history" rel="nofollow">History (66 revisions)</a> <a href="/nlab/show/finite+set/cite" style="color: black">Cite</a> <a href="/nlab/print/finite+set" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/finite+set" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>