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> stuff, structure, property 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> stuff, structure, property </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/4106/#Item_25" 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>Stuff, structure, and properties</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="category_theory">Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></p> <h2 id="sidebar_concepts">Concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> </li> </ul> <h2 id="sidebar_universal_constructions">Universal constructions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit">limit</a>/<a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weighted+limit">weighted limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/end">end</a>/<a class="existingWikiWord" href="/nlab/show/coend">coend</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kan+extension">Kan extension</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Isbell+duality">Isbell duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monadicity+theorem">monadicity theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+lifting+theorem">adjoint lifting theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tannaka+duality">Tannaka duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gabriel-Ulmer+duality">Gabriel-Ulmer duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/small+object+argument">small object argument</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freyd-Mitchell+embedding+theorem">Freyd-Mitchell embedding theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></p> </li> </ul> <h2 id="sidebar_extensions">Extensions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf+and+topos+theory">sheaf and topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+category+theory">enriched category theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> </li> </ul> <h2 id="sidebar_applications">Applications</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/applications+of+%28higher%29+category+theory">applications of (higher) category theory</a></li> </ul> <div> <p> <a href="/nlab/edit/category+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="stuff_structure_and_properties">Stuff, structure, and properties</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <li><a href='#definitions'>Definitions</a></li> <ul> <li><a href='#interpretation_in_terms_of_ksurjectivity'>Interpretation in terms of k-surjectivity</a></li> <li><a href='#generalization_to_higher_groupoids'>Generalization to higher groupoids</a></li> <li><a href='#generalization_to_categories_and_higher_categories'>Generalization to categories and higher categories</a></li> </ul> <li><a href='#AFactorizationSystem'>A factorisation system</a></li> <li><a href='#examples'>Examples</a></li> <ul> <li><a href='#the_classical_categories_of_sets_with_extra_structure'>The classical categories of sets with extra structure</a></li> <li><a href='#more_examples'>More examples</a></li> </ul> <li><a href='#logical_interpretation'>Logical interpretation</a></li> <li><a href='#formulation_in_homotopy_type_theory'>Formulation in homotopy type theory</a></li> <li><a href='#related_entries'>Related entries</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="Idea">Idea</h2> <p>It is common in <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> to speak of</p> <ol> <li> <p>objects enjoying “extra properties” (for instance a <a class="existingWikiWord" href="/nlab/show/ring">ring</a> being <a class="existingWikiWord" href="/nlab/show/commutative+ring">commutative ring</a>);</p> </li> <li> <p>objects carrying “extra <a class="existingWikiWord" href="/nlab/show/structure">structure</a>” (for instance a <a class="existingWikiWord" href="/nlab/show/set">set</a> carrying a <a class="existingWikiWord" href="/nlab/show/topological+space">topology</a>);</p> </li> <li> <p>objects being equipped with “extra stuff” (for instance a <a class="existingWikiWord" href="/nlab/show/ring">ring</a> being equipped with a <a class="existingWikiWord" href="/nlab/show/module">module</a>).</p> </li> </ol> <p>In <a class="existingWikiWord" href="/nlab/show/model+theory">model theory</a> there is a formalization of what it means to equip a <a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/mathematical+structure">mathematical structure</a>, and one may say what it means for a function between these sets to have the property of preserving this extra structure. But this formalization captures only parts of the situations in which it is useful to speak of “extra property”, “extra structure”, and “extra stuff”.</p> <p>Now <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> is precisely the kind of mathematical meta-theory that allows a nice and general formalization of such matters. Here we discuss such a formalization, due to (<a href="#BaezBartelsDolan98">Baez-Bartels-Dolan 98</a>, see also <a href="#BaezShulman06">Baez-Shulman 06, section 2.4</a>), phrased in terms of properties of <a class="existingWikiWord" href="/nlab/show/functors">functors</a> that compare a <a class="existingWikiWord" href="/nlab/show/category">category</a> of <a class="existingWikiWord" href="/nlab/show/objects">objects</a> with extra structure/property/stuff to the underlying category of objects without.</p> <p>In fact this formalization involves the generalization of what in <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a> is called the <a class="existingWikiWord" href="/nlab/show/Postnikov+tower">Postnikov tower</a> theory (or <a class="existingWikiWord" href="/nlab/show/%28n-connected%2C+n-truncated%29+factorization+system">(n-connected, n-truncated) factorization system</a>), generalizing this from <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a> to <a class="existingWikiWord" href="/nlab/show/categories">categories</a> (<a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy types</a>).</p> <p>For related discussion see also at <em><a class="existingWikiWord" href="/nlab/show/structure+type">structure type</a></em> and <em><a class="existingWikiWord" href="/nlab/show/stuff+type">stuff type</a></em>.</p> <p>Note that this account operates under the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a>, where constructions are taken to be invariant under morphisms which are invertible in a maximally weak sense. When working with various amounts of <a class="existingWikiWord" href="/nlab/show/strict+n-category">strictness</a>, further requirements are appropriate, some of which are noted below.</p> <h2 id="definitions">Definitions</h2> <p>To begin with, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> be <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a>, and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">F: C \to D</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/functor">functor</a>. By fiat, declare <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> to be a <a class="existingWikiWord" href="/nlab/show/forgetful+functor">forgetful functor</a>. Then</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets nothing</strong> if it is an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets only properties</strong> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/full+and+faithful+functor">fully faithful</a>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets at most structure</strong> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/faithful+functor">faithful</a>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets at most stuff</strong> regardless.</li> </ul> <p>Another way to break down the possibilities (used in a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-way <a class="existingWikiWord" href="/nlab/show/factorization+system">factorisation system</a>) is as follows:</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets only properties</strong> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/full+functor">full</a> and faithful;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets purely structure</strong> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/essentially+surjective+functor">essentially surjective</a> (on objects) and faithful;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> <strong>forgets purely stuff</strong> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is essentially surjective and full.</li> </ul> <p id="Strengthening"> Depending on author and the strictness of the situation, more properties are required of a functor to forget structure (<a href="#Ehresmann57">Ehresmann 57</a>, <a href="#Ehresmann65">Ehresmann 65</a>, <a href="#AdamekRosickyVitale">Adamek-Rosicky-Vitale 09, remark 13.18</a>):</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/amnestic+functor">amnestic functor</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math>-vertical <a class="existingWikiWord" href="/nlab/show/isomorphisms">isomorphisms</a> are <a class="existingWikiWord" href="/nlab/show/identities">identities</a>),</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/isofibration">isofibration</a>.</p> </li> </ol> <p>However, notice that these two conditions violate the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> for <a class="existingWikiWord" href="/nlab/show/categories">categories</a>. In the terminology of <em><a class="existingWikiWord" href="/nlab/show/strict+categories">strict categories</a></em> one might hence refer to these conditions as expressing “strict extra structure”.</p> <h3 id="interpretation_in_terms_of_ksurjectivity">Interpretation in terms of k-surjectivity</h3> <p>The pattern here is best understood in terms of the notion of <a class="existingWikiWord" href="/nlab/show/k-surjective+functor">essentially k-surjective functor</a>.</p> <p>Recall that for a functor between ordinary categories (1-categories)</p> <ul> <li>essentially surjective <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> essentially 0-surjective</li> <li>full <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> essentially 1-surjective</li> <li>faithful <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math> essentially 2-surjective</li> </ul> <p>and that every 1-functor is essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math>-surjective for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi><mo>≥</mo><mn>3</mn></mrow><annotation encoding="application/x-tex">k \geq 3</annotation></semantics></math>.</p> <p>So the above says for a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">F : C \to D</annotation></semantics></math>:</p> <table><thead><tr><th>If it is …</th><th>then it …</th><th>but it …</th></tr></thead><tbody><tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≥</mo><mn>0</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \geq 0)</annotation></semantics></math>-surjective</td><td style="text-align: left;">forgets nothing</td><td style="text-align: left;">remembers everything</td></tr> <tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≥</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \geq 1)</annotation></semantics></math>-surjective</td><td style="text-align: left;">forgets only properties</td><td style="text-align: left;">remembers at least stuff and structure</td></tr> <tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≥</mo><mn>2</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \geq 2)</annotation></semantics></math>-surjective</td><td style="text-align: left;">forgets at most structure</td><td style="text-align: left;">remembers at least stuff</td></tr> <tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≥</mo><mn>3</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \geq 3)</annotation></semantics></math>-surjective</td><td style="text-align: left;">may forget everything</td><td style="text-align: left;">may remember nothing</td></tr> </tbody></table> <p>It is worth noting that this formalism captures the intuition of how “stuff”, “structure”, and “properties” are expected to be related:</p> <ul> <li>stuff may be equipped with structure;</li> <li>structure may have (be equipped with) properties.</li> </ul> <p>The <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-way breakdown looks like this:</p> <table><thead><tr><th>If it is …</th><th>then it …</th><th>but it …</th></tr></thead><tbody><tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≠</mo><mn>0</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \ne 0)</annotation></semantics></math>-surjective</td><td style="text-align: left;">forgets only properties</td><td style="text-align: left;">remembers at least stuff and structure</td></tr> <tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≠</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \ne 1)</annotation></semantics></math>-surjective</td><td style="text-align: left;">forgets purely structure</td><td style="text-align: left;">remembers at least stuff and properties</td></tr> <tr><td style="text-align: left;">essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≠</mo><mn>2</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k \ne 2)</annotation></semantics></math>-surjective</td><td style="text-align: left;">forgets purely stuff</td><td style="text-align: left;">remembers at least structure and properties</td></tr> </tbody></table> <p>This formalism does <em>not</em> capture the intuition so well, and in fact the ‘properties’ (and ‘structure’) remembered by a functor that forgets purely structure (or purely stuff) may not match what one expects.</p> <p>See also the examples below.</p> <h3 id="generalization_to_higher_groupoids">Generalization to higher groupoids</h3> <p>The formulation in terms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math>-surjectivity induces an immediate generalization of the notions of stuff, structure and properties to the context of <a class="existingWikiWord" href="/nlab/show/infinity-category">infinity-groupoids</a>. Baez’s students speak of “2-stuff,” “3-stuff,” and so on. Of course, structure and properties can then be called 0-stuff and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-stuff, respectively.</p> <h3 id="generalization_to_categories_and_higher_categories">Generalization to categories and higher categories</h3> <p>The theory is easiest when restricted to groupoids as above; for <a class="existingWikiWord" href="/nlab/show/category">categories</a>, there are several ways to go. One is to keep the definition as phrased above (a functor between categories forgets only properties if it is fully faithful, forgets at most structure if it is faithful, etc.). Another is to apply the above definition instead to the functor between the <a class="existingWikiWord" href="/nlab/show/core">underlying groupoids</a> of the categories in question.</p> <p>To tell the difference, ask yourself whether the difference between a <a class="existingWikiWord" href="/nlab/show/monoid">monoid</a> and a <a class="existingWikiWord" href="/nlab/show/semigroup">semigroup</a> is the <em>structure</em> of being equipped with an <a class="existingWikiWord" href="/nlab/show/identity+element">identity element</a> or only the <em>property</em> that an identity element exists. Note that an identity element, if it exists, must be unique and must be preserved by semigroup isomorphisms and by monoid homomorphisms but not by semigroup homomorphisms.</p> <p>A third option is to define a new notion: a functor <strong>forgets at most property-like structure</strong> if it is <a class="existingWikiWord" href="/nlab/show/pseudomonic+functor">pseudomonic</a>. This means that (1) the functor is faithful and (2) its induced functor between underlying groupoids is fully faithful. Intuitively, property-like structure can be described as consisting of “properties which need not be automatically preserved by morphisms” or “structure which, if it exists, is uniquely determined.” Examples include that a category has all limits of a specified sort.</p> <p>Property-like structure becomes much more prevalent for higher categories. For example, the forgetful functor from the 2-category of <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+categories">cartesian monoidal categories</a> (and product-preserving functors) to <a class="existingWikiWord" href="/nlab/show/Cat">Cat</a> is essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≥</mo><mn>2</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k\ge 2)</annotation></semantics></math>-surjective, and its induced functor between 2-groupoids is essentially <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>k</mi><mo>≥</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(k\ge 1)</annotation></semantics></math>-surjective; thus it forgets property-like structure. See also <a class="existingWikiWord" href="/nlab/show/lax-idempotent+2-monad">lax-idempotent 2-monad</a>.</p> <p>Note that property-like structure is known in traditional <a class="existingWikiWord" href="/nlab/show/logic">logic</a> as <strong>categorical</strong> structure. Obviously, this term can be confusing in <a class="existingWikiWord" href="/nlab/show/categorial+logic">categorial logic</a>!</p> <h2 id="AFactorizationSystem">A factorisation system</h2> <p>Just as the category <a class="existingWikiWord" href="/nlab/show/Set">Set</a> has the best known <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>-way <a class="existingWikiWord" href="/nlab/show/factorization+system">factorisation system</a>, in which every <a class="existingWikiWord" href="/nlab/show/function">function</a> is factored into a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a> followed by an <a class="existingWikiWord" href="/nlab/show/injection">injection</a>, so the <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> <a class="existingWikiWord" href="/nlab/show/Cat">Cat</a> has a <a class="existingWikiWord" href="/nlab/show/ternary+factorisation+system">ternary factorisation system</a>, in which every functor is factored into parts which forget ‘purely’ stuff, structure, and properties.</p> <p>Specifically, given a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">F: C \to D</annotation></semantics></math>, let the <strong><a class="existingWikiWord" href="/nlab/show/1-image">1-image</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mi>im</mi><mi>F</mi></mrow><annotation encoding="application/x-tex">1 im F</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> be the category whose objects are objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> and whose morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \to y</annotation></semantics></math> are morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>F</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F(x) \to F(y)</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>; let the <strong><a class="existingWikiWord" href="/nlab/show/2-image">2-image</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mi>im</mi><mi>F</mi></mrow><annotation encoding="application/x-tex">2 im F</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> be the category whose objects are objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> and whose morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \to y</annotation></semantics></math> are morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>:</mo><mi>F</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>F</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">b: F(x) \to F(y)</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>=</mo><mi>F</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">b = F(a)</annotation></semantics></math> for some <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>y</mi></mrow><annotation encoding="application/x-tex">a: x \to y</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. (So the only difference bewteen <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mi>im</mi><mi>F</mi></mrow><annotation encoding="application/x-tex">2 im F</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> itself is equality of morphisms.) If you want to be complete, call <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> itself the <strong><a class="existingWikiWord" href="/nlab/show/3-image">3-image</a></strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> the <strong><a class="existingWikiWord" href="/nlab/show/0-image">0-image</a></strong>.</p> <p>The situation looks like this:</p> <table><thead><tr><th>This category …</th><th>gets objects from …</th><th>and morphisms from …</th><th>and equality of morphisms from …</th></tr></thead><tbody><tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mi>im</mi><mi>F</mi></mrow><annotation encoding="application/x-tex">2 im F</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mi>im</mi><mi>F</mi></mrow><annotation encoding="application/x-tex">1 im F</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math></td></tr> </tbody></table> <p>Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> can be factored into functors</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>C</mi><mover><mo>→</mo><mrow><msub><mi>F</mi> <mn>2</mn></msub></mrow></mover><mn>2</mn><mi>im</mi><mi>F</mi><mover><mo>→</mo><mrow><msub><mi>F</mi> <mn>1</mn></msub></mrow></mover><mn>1</mn><mi>im</mi><mi>F</mi><mover><mo>→</mo><mrow><msub><mi>F</mi> <mn>0</mn></msub></mrow></mover><mi>D</mi><mo>,</mo></mrow><annotation encoding="application/x-tex"> C \stackrel{F_2}\to 2 im F \stackrel{F_1}\to 1 im F \stackrel{F_0}\to D ,</annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>F</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">F_2</annotation></semantics></math> forgets purely stuff, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>F</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">F_1</annotation></semantics></math> forgets purely structure, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>F</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">F_0</annotation></semantics></math> forgets only properties. Conversely, this ternary factorization suffices to determine the notions of faithful, full, and essentially surjective functors: see <a class="existingWikiWord" href="/nlab/show/ternary+factorization+system">ternary factorization system</a>.</p> <h2 id="examples">Examples</h2> <h3 id="the_classical_categories_of_sets_with_extra_structure">The classical categories of sets with extra structure</h3> <p>The classical examples are the forgetful functors to <a class="existingWikiWord" href="/nlab/show/Set">Set</a> that define the classical categories such as <a class="existingWikiWord" href="/nlab/show/Top">Top</a>, <a class="existingWikiWord" href="/nlab/show/Grp">Grp</a>, <a class="existingWikiWord" href="/nlab/show/Vect">Vect</a>, etc. All these categories are categories of <em>sets equipped with extra structure</em> (e.g. with a topology, with a group structure, etc). Accordingly the obvious functors to <a class="existingWikiWord" href="/nlab/show/Set">Set</a> are</p> <ul> <li>faithful</li> <li>not full.</li> </ul> <p>Hence indeed, by the above yoga, they forget this extra structure but remember the stuff in question (the underlying set).</p> <h3 id="more_examples">More examples</h3> <p>The embedding of abelian groups into all groups, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo></mrow><annotation encoding="application/x-tex">F :</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Ab">Ab</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Grp">Grp</a> is faithful and full, but not essentially surjective. Hence it should remember stuff and structure but forget properties. Indeed, the property it forgets is the property “is abelian” which is a property of the group <em>structure</em> sitting on the underlying set of a group. Hence the sequence of functors</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>→</mo><mi>Grp</mi><mo>→</mo><mi>Set</mi><mo>→</mo><mi>pt</mi></mrow><annotation encoding="application/x-tex"> Ab \to Grp \to Set \to pt </annotation></semantics></math></div> <p>(with <a class="existingWikiWord" href="/nlab/show/point">pt</a> the terminal category) successively forgets first a property (being abelian) then structure (the group structure on a set) then stuff (the underlying set).</p> <p>Notice that the order here is backwards from the automatic factorisation given by the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-way factorisation system described above. (And in fact, the structure forgotten here is not ‘pure’; <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Grp</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Grp \to Set</annotation></semantics></math> is not essentially surjective.) Indeed, the above factorisation is arbitrary; it comes from seeing an abelian group as a group with an extra property and a group as a set with extra structure, but one may view things differently (for example, that an abelian group is a <a class="existingWikiWord" href="/nlab/show/monoid">monoid</a> with extra property, or a set with two group structures that are related as in the <a class="existingWikiWord" href="/nlab/show/Eckmann-Hilton+argument">Eckmann-Hilton argument</a>).</p> <p>The automatic factorisation is in fact like this (up to <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a>):</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>→</mo><mo lspace="0em" rspace="thinmathspace">pt</mo><mo>→</mo><mo lspace="0em" rspace="thinmathspace">pt</mo><mo>→</mo><mo lspace="0em" rspace="thinmathspace">pt</mo></mrow><annotation encoding="application/x-tex"> Ab \to \pt \to \pt \to \pt </annotation></semantics></math></div> <p>because the original functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>→</mo><mo lspace="0em" rspace="thinmathspace">pt</mo></mrow><annotation encoding="application/x-tex">Ab \to \pt</annotation></semantics></math> is already essentially surjective and full. In other words, from the perspective of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="0em" rspace="thinmathspace">pt</mo></mrow><annotation encoding="application/x-tex">\pt</annotation></semantics></math>, an abelian group is simply extra stuff.</p> <p>More interestingly, we can factor the forgetful functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Ab \to Set</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>→</mo><mi>Ab</mi><mo>→</mo><mi>Set</mi><mo>∖</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex"> Ab \to Ab \to Set \setminus \{\empty\} \to Set </annotation></semantics></math></div> <p>Here, the first part is trivial because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Ab \to Set</annotation></semantics></math> is faithful. The category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi><mo>∖</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">Set \setminus \{\empty\}</annotation></semantics></math> is the category of <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>s, that is the category of sets that are capable of being equipped with the structure of an abelian group. So from the point of view of its underlying set, an abelian group is a set with the <em>property</em> that it is inhabited and the <em>structure</em> of an abelian group but no additional <em>stuff</em>.</p> <p>For something interesting at every level, take the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>×</mo><mi>Ab</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Ab \times Ab \to Set</annotation></semantics></math> that takes the underlying set of the first abelian group. This factors as follows:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo>×</mo><mi>Ab</mi><mo>→</mo><mi>Ab</mi><mo>→</mo><mi>Set</mi><mo>∖</mo><mo stretchy="false">{</mo><mi>∅</mi><mo stretchy="false">}</mo><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex"> Ab \times Ab \to Ab \to Set \setminus \{\empty\} \to Set </annotation></semantics></math></div> <p>So a pair of abelian groups (from the perspective of the underlying set of the first one) consists of the <em>property</em> that the set is inhabited, then the <em>structure</em> of an abelian group on that set, and finally extra <em>stuff</em> consisting of the entire second group.</p> <h2 id="logical_interpretation">Logical interpretation</h2> <p>In <a class="existingWikiWord" href="/nlab/show/logic">logic</a> a property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is given by a <a class="existingWikiWord" href="/nlab/show/predicate">predicate</a>, which we may think of as an operation that takes a thing <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 the <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a> of the statement “<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> has property <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>”. Note that a truth value is a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%28-1%29-groupoid">groupoid</a>; we get structure and stuff by replacing this with a <a class="existingWikiWord" href="/nlab/show/set">set</a> (a <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>-<a class="existingWikiWord" href="/nlab/show/0-groupoid">groupoid</a>) or a <a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a> (a <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>-<a class="existingWikiWord" href="/nlab/show/1-groupoid">groupoid</a>) and we get <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>-stuff by replacing this with an <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>-<a class="existingWikiWord" href="/nlab/show/n-groupoid">groupoid</a>.</p> <p>Now, if a property of objects of a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> that respects the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> holds for some object <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>, then it must hold for any object <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphic</a> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>. That is, the predicate defining that property is actually a <a class="existingWikiWord" href="/nlab/show/functor">functor</a> from the <a class="existingWikiWord" href="/nlab/show/core">core</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">C_iso</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> to the groupoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>TV</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">TV_iso</annotation></semantics></math> of truth values. Given such a predicate functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>, it's immediate how to define a <a class="existingWikiWord" href="/nlab/show/full+subcategory">full subcategory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">C_P</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> consisting of those objects with the property; the <a class="existingWikiWord" href="/nlab/show/inclusion+functor">inclusion functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>P</mi></msub><mo>↪</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">C_P \hookrightarrow C</annotation></semantics></math> is fully faithful, as it should be for extra property. Conversely, given a fully faithful functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F: D \to C</annotation></semantics></math>, define a property of objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> that respects the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> as follows: an object <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> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> has the property if there is some object <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> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≅</mo><mi>F</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \cong F(a)</annotation></semantics></math>. If you apply this to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>P</mi></msub><mo>↪</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">C_P \hookrightarrow C</annotation></semantics></math>, then you get the predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> back; if you start with an arbitrary fully faithful <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F: D \to C</annotation></semantics></math>, define a predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>, and then form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>F</mi></msub></mrow><annotation encoding="application/x-tex">C_F</annotation></semantics></math>, you'll find that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>F</mi></msub></mrow><annotation encoding="application/x-tex">C_F</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a>, even as <a class="existingWikiWord" href="/nlab/show/bundle">bundle</a>s over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>.</p> <p>Diagrammatically this may be phrased as saying that every fully faithful functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">D \to C</annotation></semantics></math> arises as a <a class="existingWikiWord" href="/nlab/show/2-limit">weak pullback</a> of the <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>-<a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></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><msub><mi>D</mi> <mi>iso</mi></msub></mtd> <mtd><mo>→</mo></mtd> <mtd><mo>*</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd><mo>⇓</mo></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mi>true</mi></msup></mtd></mtr> <mtr><mtd><msub><mi>C</mi> <mi>iso</mi></msub></mtd> <mtd><mover><mo>→</mo><mi>P</mi></mover></mtd> <mtd><mo stretchy="false">{</mo><mo lspace="0em" rspace="thinmathspace">true</mo><mo>,</mo><mi>false</mi><mo stretchy="false">}</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ D_{iso} &\to& * \\ \downarrow &\Downarrow& \downarrow^{true} \\ C_{iso} &\stackrel{P}{\to}& \{\true, false \} } </annotation></semantics></math></div> <p>Similarly, any structure on objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> that respects the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> is given by a functor from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">C_iso</annotation></semantics></math> to the groupoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">Set_iso</annotation></semantics></math> of sets. Given such a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">C_P</annotation></semantics></math> be the <a class="existingWikiWord" href="/nlab/show/category+of+elements">category of elements</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>, which comes with a faithful functor from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">C_P</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. Conversely, given any faithful functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F: D \to C</annotation></semantics></math> and an object <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> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(x)</annotation></semantics></math> be the <a class="existingWikiWord" href="/nlab/show/essential+fiber">essential fiber</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, which (because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> is faithful) is a <a class="existingWikiWord" href="/nlab/show/discrete+category">discrete category</a> and hence (equivalent to) a set. These operations are also invertible, up to equivalence.</p> <p>Diagrammatically this may be phrased as saying that every faithful functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">D \to C</annotation></semantics></math> arises as a <a class="existingWikiWord" href="/nlab/show/2-limit">weak pullback</a> of the <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>-subobject classifier (as described at <a class="existingWikiWord" href="/nlab/show/generalized+universal+bundle">generalized universal bundle</a> and at <a class="existingWikiWord" href="/nlab/show/category+of+elements">category of elements</a>)</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><msub><mi>D</mi> <mi>iso</mi></msub></mtd> <mtd><mo>→</mo></mtd> <mtd><mo stretchy="false">(</mo><msub><mi>Set</mi> <mo>*</mo></msub><msub><mo stretchy="false">)</mo> <mi>iso</mi></msub></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd><mo>⇓</mo></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><msub><mi>C</mi> <mi>iso</mi></msub></mtd> <mtd><mover><mo>→</mo><mrow></mrow></mover></mtd> <mtd><msub><mi>Set</mi> <mi>iso</mi></msub></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \array{ D_{iso} &\to& (Set_*)_{iso} \\ \downarrow &\Downarrow& \downarrow \\ C_{iso} &\stackrel{}{\to}& Set_{iso} } \,. </annotation></semantics></math></div> <p>Next, any stuff on objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> that respects the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> is given by a functor from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">C_iso</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">Grpd_iso</annotation></semantics></math>. Here <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">Grpd_iso</annotation></semantics></math> should be taken to be the <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>-<a class="existingWikiWord" href="/nlab/show/2-groupoid">groupoid</a> whose objects are groupoids, whose morphisms are equivalences, and whose <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>-morphisms are <a class="existingWikiWord" href="/nlab/show/natural+isomorphism">natural isomorphism</a>s; similarly, the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><msub><mi>C</mi> <mi>iso</mi></msub><mo>→</mo><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">P: C_iso \to Grpd_iso</annotation></semantics></math> should be taken in the weakest sense (often called a <a class="existingWikiWord" href="/nlab/show/pseudofunctor">pseudofunctor</a>). Then the <a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a> turns <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> into a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">C_P</annotation></semantics></math> equipped with a functor to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>; again, the essential fiber converts any functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F: D \to C</annotation></semantics></math> into such a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> (although really you must take the core of the essential fiber to get a groupoid).</p> <p>Diagrammatically this may be phrased as saying that every functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">D \to C</annotation></semantics></math> arises as a <a class="existingWikiWord" href="/nlab/show/2-limit">weak pullback</a> of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-subobject classifier (as described at <a class="existingWikiWord" href="/nlab/show/generalized+universal+bundle">generalized universal bundle</a> )</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><msub><mi>D</mi> <mi>iso</mi></msub></mtd> <mtd><mo>→</mo></mtd> <mtd><mo stretchy="false">(</mo><msub><mi>Grpd</mi> <mo>*</mo></msub><msub><mo stretchy="false">)</mo> <mi>iso</mi></msub></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd><mo>⇓</mo></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><msub><mi>C</mi> <mi>iso</mi></msub></mtd> <mtd><mover><mo>→</mo><mrow></mrow></mover></mtd> <mtd><msub><mi>Grpd</mi> <mi>iso</mi></msub></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \array{ D_{iso} &\to& (Grpd_*)_{iso} \\ \downarrow &\Downarrow& \downarrow \\ C_{iso} &\stackrel{}{\to}& Grpd_{iso} } \,. </annotation></semantics></math></div> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a mere <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>-<a class="existingWikiWord" href="/nlab/show/1-category">category</a>, then any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><msub><mi>C</mi> <mi>iso</mi></msub><mo>→</mo><mn>2</mn><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">P: C_iso \to 2 Grpd_iso</annotation></semantics></math> is equivalent to some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><msub><mi>C</mi> <mi>iso</mi></msub><mo>→</mo><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">P: C_iso \to Grpd_iso</annotation></semantics></math>, but in general we need to consider <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><msub><mi>C</mi> <mi>iso</mi></msub><mo>→</mo><mi>n</mi><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">P: C_iso \to n Grpd_iso</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><msub><mi>C</mi> <mi>iso</mi></msub><mo>→</mo><mn>∞</mn><msub><mi>Grpd</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">P: C_iso \to \infty Grpd_iso</annotation></semantics></math> to study higher forms of <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>-stuff.</p> <p>Lest we forget, to be even more simple than an extra property, the groupoid of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>2</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-2)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%28-2%29-groupoid">groupoid</a>s is the <a class="existingWikiWord" href="/nlab/show/point">point</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>pt</mi></mrow><annotation encoding="application/x-tex">pt</annotation></semantics></math>, and there is exactly one functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> from any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>iso</mi></msub></mrow><annotation encoding="application/x-tex">C_iso</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>pt</mi></mrow><annotation encoding="application/x-tex">pt</annotation></semantics></math>, corresponding to the unique (up to equivalence) category equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>.</p> <p>For the <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a> <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-Grpd">∞-Grpd</a> of <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-groupoid">∞-groupoid</a>s the analog of the subobject classifier is the <a class="existingWikiWord" href="/nlab/show/universal+fibration+of+%28%E2%88%9E%2C1%29-categories">universal fibration of (∞,1)-categories</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Z</mi><msub><mo stretchy="false">|</mo> <mrow><mn>∞</mn><mi>Grpd</mi></mrow></msub><mo>→</mo><mn>∞</mn><mi>Grpd</mi></mrow><annotation encoding="application/x-tex">Z|_{\infty Grpd} \to \infty Grpd</annotation></semantics></math>. See also section 6.1.6 <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-Topoi and Classifying objects</em> of <a class="existingWikiWord" href="/nlab/show/Higher+Topos+Theory">HTT</a>.</p> <h2 id="formulation_in_homotopy_type_theory">Formulation in homotopy type theory</h2> <p>A map between <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy types</a> is equivalent to a <a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> projection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f: \sum_{x: A} B(x) \to A</annotation></semantics></math>. If the types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(x)</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/homotopy+n-type">n-types</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> forgets <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>-stuff.</p> <h2 id="related_entries">Related entries</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structure">structure</a>, <a class="existingWikiWord" href="/nlab/show/structure+type">structure type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/stuff+type">stuff type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+property">topological property</a>, <a class="existingWikiWord" href="/nlab/show/uniform+property">uniform property</a></p> </li> </ul> <h2 id="references">References</h2> <p>The original proposal for formalizing notions of <a class="existingWikiWord" href="/nlab/show/mathematical+structures">mathematical structures</a> via <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>, specifically via the <a class="existingWikiWord" href="/nlab/show/forgetful+functors">forgetful functors</a> between the <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a> which they form:</p> <ul> <li id="Ehresmann57"> <p><a class="existingWikiWord" href="/nlab/show/Charles+Ehresmann">Charles Ehresmann</a>, <em>Gattungen von lokalen Strukturen</em>, Jahresbericht der Deutschen Mathematiker-Vereinigung <strong>60</strong> (1958) 49-77 [<a href="https://eudml.org/doc/146434">dml:146434</a>]</p> </li> <li id="Ehresmann65"> <p><a class="existingWikiWord" href="/nlab/show/Charles+Ehresmann">Charles Ehresmann</a>, <em>Catégories et Structures</em>, Séminaire Ehresmann. Topologie et géométrie différentielle <strong>6</strong> (1964) 1-31 [<a href="http://www.numdam.org/item?id=SE_1964__6__A8_0">numdam:SE_1964__6__A8_0</a>, <a href="https://eudml.org/doc/112200">dml:112200</a>]</p> </li> </ul> <p>Exposition and re-amplification:</p> <ul> <li id="BaezBartelsDolan98"> <p><a href="http://math.ucr.edu/home/baez/qg-spring2004/discussion.html">original UseNet discussion</a> on <code>sci.physics.research</code> in 1998;</p> </li> <li> <p>a pedagogical comparison to quadratic, linear, and constant polynomials (<a href="http://math.ucr.edu/home/baez/qg-spring2004/polynomials.pdf">PDF</a>) by Toby Bartels in 2004;</p> </li> <li id="BaezShulman06"> <p><a href="http://arxiv.org/PS_cache/math/pdf/0608/0608420v2.pdf#page=15">section 2.4, p. 15</a> and <a href="http://arxiv.org/PS_cache/math/pdf/0608/0608420v2.pdf#page=17">section 3.1, p. 17</a> of J. Baez and M. Shulman, <em><a class="existingWikiWord" href="/nlab/show/Lectures+on+n-Categories+and+Cohomology">Lectures on n-Categories and Cohomology</a></em> (<a href="http://arxiv.org/abs/math/0608420">arXiv</a>).</p> </li> </ul> <p>For modern accounts on mathematical structures via <a class="existingWikiWord" href="/nlab/show/categorical+algebra">categorical algebra</a> see also at <em><a class="existingWikiWord" href="/nlab/show/algebraic+theory">algebraic theory</a></em>, <em><a class="existingWikiWord" href="/nlab/show/monad">monad</a></em>, <em><a class="existingWikiWord" href="/nlab/show/sketch">sketch</a></em>.</p> </body></html> </div> <div class="revisedby"> <p> Last revised on February 1, 2024 at 01:08:27. See the <a href="/nlab/history/stuff%2C+structure%2C+property" 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/stuff%2C+structure%2C+property" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4106/#Item_25">Discuss</a><span class="backintime"><a href="/nlab/revision/stuff%2C+structure%2C+property/57" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/stuff%2C+structure%2C+property" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/stuff%2C+structure%2C+property" accesskey="S" class="navlink" id="history" rel="nofollow">History (57 revisions)</a> <a href="/nlab/show/stuff%2C+structure%2C+property/cite" style="color: black">Cite</a> <a href="/nlab/print/stuff%2C+structure%2C+property" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/stuff%2C+structure%2C+property" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>