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.dtd" > <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en-ca"> <head> <title>nForum - structural induction over categories</title> <link rel="shortcut icon" href="/themes/nforum/styles/nforum/favicon.ico" /> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <link rel="stylesheet" type="text/css" href="/extensions/TagThis/theme/tagthis.css" /> <link rel="stylesheet" type="text/css" href="/themes/nforum/styles/nforum/vanilla.css" media="screen" /> <link rel="stylesheet" type="text/css" href="/themes/nforum/styles/nforum/vanilla.print.css" media="print" /> <link rel="stylesheet" type="text/css" href="/extensions/GuestPost/style.css" /> <link rel="stylesheet" type="text/css" href="/extensions/GuestSignIn/style.css" /> <link rel="stylesheet" type="text/css" href="/extensions/OpenID/css/openid.css" /> <link rel="stylesheet" type="text/css" href="/extensions/PreviewPost/preview.css" /> <script type="text/javascript" src="/js/global.js"></script> <script type="text/javascript" src="/js/vanilla.js"></script> <script type="text/javascript" src="/js/ajax.js"></script> <script type="text/javascript" src="/js/ac.js"></script> <script type="text/javascript" src="/extensions/JQuery/jquery-1.4.2.min.js"></script> <script type="text/javascript" src="/extensions/OpenID/js/openid-jquery.js"></script> <script type="text/javascript" src="/extensions/OpenID/js/openid-en.js"></script> <script type="text/javascript" src="/extensions/MarkdownItex/itex.js"></script> <script type="text/javascript" src="/extensions/MembersList/library/tablesort.js"></script> <script type="text/javascript" src="/extensions/MembersList/library/paginate.js"></script> <script type="text/javascript" src="/extensions/PreviewPost/preview.js"></script> <script type="text/javascript" src="/extensions/CustomStyles/functions.js"></script> <script type="text/javascript" src="/js/prototype.js"></script> <script type="text/javascript" src="/js/scriptaculous.js"></script> <script type="text/javascript" src="/extensions/Notify/functions.js"></script> <link rel="alternate" type="application/rss+xml" href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Comments&Page=1&Feed=RSS2&DiscussionID=3782&FeedTitle=Discussion+Feed+%28structural+induction+over+categories%29" title="Discussion Feed (RSS2)" /> <link rel="alternate" type="application/atom+xml" href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Comments&Page=1&Feed=ATOM&DiscussionID=3782&FeedTitle=Discussion+Feed+%28structural+induction+over+categories%29" title="Discussion Feed (ATOM)" /> <script type="text/javascript"> ( function($) { $(document).ready(function() { openid.init('openid_identifier',true); openid.setFormID('frmSignInOpenID'); }); }) (jQuery ); </script><script type="text/x-mathjax-config">MathJax.Hub.Config({TeX: {extensions: ["AMScd.js"]}});</script><script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=MML_HTMLorMML-full"></script></head> <body id="CommentsPage" > <div id="SiteContainer"><div id="Session">Not signed in (<a href="/people.php?ReturnUrl=http%3A%2F%2Fnforum.ncatlab.org%2Fdiscussion%2F3782%2Fstructural-induction-over-categories%2F">Sign In</a>)</div><div id="Header"> <a id="pgtop"></a> <span id="logo"></span> <h1> nForum </h1> <div id="TagLine">A discussion forum about contributions to the <a href="https://ncatlab.org/">nLab wiki</a> and related areas of mathematics, physics, and philosophy.</div><ul><li><a href="/extension.php?PostBackAction=HomeCat" >Home</a></li><li class="TabOn"><a href="/" >Discussions</a></li><li><a href="/categories.php" >Categories</a></li><li><a href="/search.php" >Search</a></li><li><a href="https://ncatlab.org/nlab/show/HomePage" >nLab</a></li><li><a href="https://ncatlab.org/nlabmeta/show/Welcome+to+the+nForum" >Help</a></li></ul> </div><div id="Body"><div id="Panel"><ul> <li> <h2>Discussion Feed</h2> <ul><li> <a href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Comments&Page=1&Feed=RSS2&DiscussionID=3782&FeedTitle=Discussion+Feed+%28structural+induction+over+categories%29" title="Subscribe to this feed..." class="RSS2">RSS2</a></li><li> <a href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Comments&Page=1&Feed=ATOM&DiscussionID=3782&FeedTitle=Discussion+Feed+%28structural+induction+over+categories%29" title="Subscribe to this feed..." class="ATOM">ATOM</a></li></ul> </li> </ul><div id="GuestSignIn"> <h2>Not signed in</h2> <p>Want to take part in these discussions? Sign in if you have an account, or apply for one below</p> <fieldset><form id="frmSignInUser" method="post" action="https://nforum.ncatlab.org/people/"> <div> <input name="PostBackAction" value="SignIn" type="hidden" /> <input name="ReturnUrl" value="http://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/" type="hidden" /> <ul> <li><label for="txtUsername">Username</label> <input id="txtUsername" name="Username" value="" class="Input" maxlength="20" type="text" /> </li> <li><label for="txtPassword">Password</label> <input id="txtPassword" name="Password" value="" class="Input" type="password" /> </li> <li id="RememberMe"><label for="RememberMeID"> <input name="RememberMe" value="1" id="RememberMeID" type="checkbox" checked="checked" /> Remember me</label> </li> <li> <input name="userSignIn" value="Sign In" class="Button" type="submit" /> </li> </ul> </div> </form> </fieldset> <fieldset><form id="frmSignInOpenID" method="post" action="https://nforum.ncatlab.org/people/"> <input name="PostBackAction" value="SignIn" type="hidden" /> <div> <ul> <li>Sign in using OpenID <div id="openid_choice"> <div id="openid_btns"></div> </div> <div id="openid_input_area"> <input id="openid_identifier" name="openid_identifier" type="text" value="http://" /> </div> </li> <li id="RememberMe"><label for="RememberMeID"> <input name="RememberMe" value="1" id="RememberMeID" type="checkbox" checked="checked" /> Remember me</label> </li> <li><input name="openidSignIn" value="Sign In" class="Button" type="submit" /></li> </ul> </div></form></fieldset> <ul class="MembershipOptionLinks"> <li class="ForgotPasswordLink"><a href="https://nforum.ncatlab.org/people/?PostBackAction=PasswordRequestForm">Forgot your password?</a></li> <li class="ApplyForMembershipLink"><a href="https://nforum.ncatlab.org/people/?PostBackAction=ApplyForm">Apply for membership</a></li> </ul></div><h2>Discussion Tag Cloud</h2><div id="TagCloud"><span style="font-size:152%"><a href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Topics&Tag=category" class="TagLink">category</a></span> <span style="font-size:54%"><a href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Topics&Tag=induction" class="TagLink">induction</a></span> <span style="font-size:52%"><a href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Topics&Tag=structural" class="TagLink">structural</a></span> <span style="font-size:200%"><a href="https://nforum.ncatlab.org/search/?PostBackAction=Search&Type=Topics&Tag=theory" class="TagLink">theory</a></span></div><p id="AboutVanilla"><a href="http://getvanilla.com">Vanilla 1.1.10</a> is a product of <a href="http://lussumo.com">Lussumo</a>. More Information: <a href="http://lussumo.com/docs">Documentation</a>, <a href="http://lussumo.com/community">Community Support</a>.</p></div> <div id="Content"><div id="NoticeCollector" class="Notices"><div class="Notice"><strong>Welcome to nForum</strong> <br />If you want to take part in these discussions either <a href="/people.php?ReturnUrl=http%3A%2F%2Fnforum.ncatlab.org%2Fdiscussion%2F3782%2Fstructural-induction-over-categories%2F">sign in now</a> (if you have an account), <a href="https://nforum.ncatlab.org/people/?PostBackAction=ApplyForm">apply for one now</a> (if you don't).</div></div><div class="ContentInfo Top"> <h1><a href="https://nforum.ncatlab.org/19/"></a> <a href="https://nforum.ncatlab.org/19/">Atrium</a>: structural induction over categories</h1> <a href="#pgbottom">Bottom of Page</a> <div class="PageInfo"> <p>1 to 8 of 8</p> <ol class="PageList PageListEmpty"> <li> </li> </ol> </div> </div> <div id="ContentBody"> <script type="text/javascript"> //<![CDATA[ function toggle_source(id) { var mysrc = document.getElementById("CommentBody_" + id).firstChild; if (mysrc.className == "source") { if (mysrc.style.display == "none") { mysrc.style.display = "block"; } else { mysrc.style.display = "none"; } } } var commentIds = new Array(0); function hide_sources() { for (i = 0; i < commentIds.length; i++) { var myself = document.getElementById("Source" + commentIds[i]); var mycmt = document.getElementById("CommentBody_" + commentIds[i]); if (mycmt.firstChild.className != "source") { myself.style.display = "none"; } } } window.onload = hide_sources; //]]> </script> <ol id="Comments"><li id="Comment_31070"> <a id="Item_1"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>1.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></li> <li><span>CommentTime</span>May 4th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31070#Comment_31070">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31070"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>I am looking for any kind of paper that uses structural induction where the ordered set is actually a collection of categories and the ordering relation is any kind of functor. I am thinking of the category with only one morphism as a base case. In particular, I am interested in the collection of internal categories in a monoidal category, but any usage of this method (over cats) would be of interest. In the case of internal cats, given any structural inductive proof in the collection of internal categories, what does the proof say about the underlying monoidal category. Can we present an axiom of the underlying monoidal category M as an inductive proof. That is, proven inductively over the collection of internal categories of M, any proven axiom also is an axiom of the underlying category? If I am dead wrong in assuming you can do structural induction over categories, please help me to understand why.</code></div><div> <p>I am looking for any kind of paper that uses structural induction where the ordered set is actually a collection of categories and the ordering relation is any kind of functor. I am thinking of the category with only one morphism as a base case. In particular, I am interested in the collection of internal categories in a monoidal category, but any usage of this method (over cats) would be of interest. In the case of internal cats, given any structural inductive proof in the collection of internal categories, what does the proof say about the underlying monoidal category. Can we present an axiom of the underlying monoidal category M as an inductive proof. That is, proven inductively over the collection of internal categories of M, any proven axiom also is an axiom of the underlying category?</p> <p>If I am dead wrong in assuming you can do structural induction over categories, please help me to understand why.</p> </div> </div> </li><li id="Comment_31071" class="Alternate"> <a id="Item_2"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>2.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/3/">Mike Shulman</a></li> <li><span>CommentTime</span>May 4th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31071#Comment_31071">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31071"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/3/">Mike Shulman</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>Can you define more precisely what you mean by "structural induction"? To me "structural induction" usually means induction over some inductive definition.</code></div><div> <p>Can you define more precisely what you mean by “structural induction”? To me “structural induction” usually means induction over some inductive definition.</p> </div> </div> </li><li id="Comment_31077"> <a id="Item_3"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>3.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/20/">David_Corfield</a></li> <li><span>CommentTime</span>May 5th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31077#Comment_31077">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31077"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/20/">David_Corfield</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>Are there interesting cases where you have an initial 2-algebra in some 2-category of 2-algebras for a 2-functor: $Cat \to Cat$?</code></div><div> <p>Are there interesting cases where you have an initial 2-algebra in some 2-category of 2-algebras for a 2-functor: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>Cat</mi><mo>&rightarrow;</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat \to Cat</annotation></semantics></math>?</p> </div> </div> </li><li id="Comment_31111" class="Alternate"> <a id="Item_4"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>4.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></li> <li><span>CommentTime</span>May 7th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31111#Comment_31111">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31111"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>Hi, I looked up inductive type and now I see David's comment as a generalization of the inductive type where the types are categories themselves. Let me know if I have that right. I tried all weekend to create an inductive defintion for a class of categories which fit my interests. I couldn't do it. I will have to work out the idea, but I guess you will have to inductively define a collection of categories where the ordering relation is a suitable functor. The main idea in my posting is that, since in structural induction you can have induction over ordered structures that are partially ordered you might get a rich collection of categories over which to do the induction. While I have your attention, I might add another desired property for the partially ordered, inductively defined collection of categories. A while back, I posted about a concept I called "category update", where an update is a functor like adding a morphism or adding the data that two morphisms can be composed or adding a commuting arrow to a composed pair so that you get a triangle or a square. I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be "updates". The simple intuition here is that, starting at the base case of an empty category, an update functor adds the first arrow. From there on you have a rich collection of cats to get to and this forms a partially ordered collection of cats. I can't grasp the initial algebra as the inductive type. I will probably look into that next as an alternate route. Is there a suggestion that anyone has? Does this sound like anything?</code></div><div> <p>Hi,</p> <p>I looked up inductive type and now I see David’s comment as a generalization of the inductive type where the types are categories themselves. Let me know if I have that right. I tried all weekend to create an inductive defintion for a class of categories which fit my interests. I couldn’t do it. I will have to work out the idea, but I guess you will have to inductively define a collection of categories where the ordering relation is a suitable functor. The main idea in my posting is that, since in structural induction you can have induction over ordered structures that are partially ordered you might get a rich collection of categories over which to do the induction.</p> <p>While I have your attention, I might add another desired property for the partially ordered, inductively defined collection of categories. A while back, I posted about a concept I called “category update”, where an update is a functor like adding a morphism or adding the data that two morphisms can be composed or adding a commuting arrow to a composed pair so that you get a triangle or a square. I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be “updates”. The simple intuition here is that, starting at the base case of an empty category, an update functor adds the first arrow. From there on you have a rich collection of cats to get to and this forms a partially ordered collection of cats.</p> <p>I can’t grasp the initial algebra as the inductive type. I will probably look into that next as an alternate route.</p> <p>Is there a suggestion that anyone has? Does this sound like anything?</p> </div> </div> </li><li id="Comment_31113"> <a id="Item_5"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>5.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></li> <li><span>CommentTime</span>May 7th 2012</li><li><em>(edited May 7th 2012)</em></li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31113#Comment_31113">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31113"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>This is going to sound cracked, but this all looks like the foundation for a Bayesian inference "over structure itself". (I guess I am quoting myself here. Mike will have to double quote that to get me to explain what I mean. So many of my vague comments have garnered quotation and patient puzzlement. Panangaden was not impressed when I used vague language, so I want to thank you all for your patience.) :) If someone could say anything about the compact or finitely presentable categories in our collection of cats and updates (inductively defined), it would help me a lot. I will never be able to finish this work. It sounds really neat, though. We need to finish off the axioms for what a "category update is", identify that it forms an inductively defined collection of cats, and then understand how to do the proof by induction over the collection (what I called structural induction). Another thing: any proof by this kind of induction is a proof about the collection itself. So, say that our collection of cats was, in fact, every cat. Then any proof by this induction would actually be about categories themselves. Taken together, the theorems would constitute a presentation of the theory of categories.</code></div><div> <p>This is going to sound cracked, but this all looks like the foundation for a Bayesian inference “over structure itself”. (I guess I am quoting myself here. Mike will have to double quote that to get me to explain what I mean. So many of my vague comments have garnered quotation and patient puzzlement. Panangaden was not impressed when I used vague language, so I want to thank you all for your patience.) :)</p> <p>If someone could say anything about the compact or finitely presentable categories in our collection of cats and updates (inductively defined), it would help me a lot.</p> <p>I will never be able to finish this work. It sounds really neat, though. We need to finish off the axioms for what a “category update is”, identify that it forms an inductively defined collection of cats, and then understand how to do the proof by induction over the collection (what I called structural induction).</p> <p>Another thing: any proof by this kind of induction is a proof about the collection itself. So, say that our collection of cats was, in fact, every cat. Then any proof by this induction would actually be about categories themselves. Taken together, the theorems would constitute a presentation of the theory of categories.</p> </div> </div> </li><li id="Comment_31116" class="Alternate"> <a id="Item_6"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>6.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/3/">Mike Shulman</a></li> <li><span>CommentTime</span>May 7th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31116#Comment_31116">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31116"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/3/">Mike Shulman</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>> I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be "updates". Are you suggesting that the idea of one thing coming "after" another in the ordering relation used for structural induction is analogous to the idea of one category being generated by adding objects or morphisms or relations to another one? If so, then I think the phrase ordering *relation* is misleading, because a category can be generated in many such ways. Perhaps what you are looking for is the idea of categorical cell complexes. Suppose in some category (this in an "ambient" category, not the categories you want to build with updates) we have a collection of morphisms $S_i \to D_i$, called "cells" or "generating cofibrations". In topology we think of $S_i$ as a "sphere" of some dimension, $D_i$ as a "disc", and the map as the inclusion of a sphere as the boundary of the disc of one higher dimension. In terms of your "updates" you can think of $S_i$ as specifying the data that you might have before your update, and $D_i$ as the result of the update. Then the operation of "attaching a cell", which might roughly correspond to your "updates", means pushing out one of these morphisms: $$\array{ S_i & \to & X \\ \downarrow && \downarrow \\ D_i & \to & X \sqcup_{S_i} D_i }$$ For instance, in the ambient category $Cat$, we can consider the following morphisms as our cells: * The inclusion $0\to 1$ of the empty category into the trivial category. * The inclusion $2\to I$ of the two-object discrete category into the [[interval category]]. * The map $P \to I$ from the walking [[parallel pair]] (which has two objects $x$ and $y$ and two nonidentity morphism $x\rightrightarrows y$) to the interval category. Then attaching a cell of the first type means adding an object. Attaching a cell of the second type means adding a morphism (and, in consequence, freely adding all composites of that morphism with the existing morphisms in the category). And attaching a cell of the third type means forcing two given morphisms to become equal (along with all other equalities of morphisms that that entails). In general, a *cell complex* is an object together with a way to build it up with a (possibly transfinite) sequence of cell attachments of this sort. (In the transfinite sequence we just take colimits at limit ordinals.) Being a cell complex is *structure* on an object: we may be able to build up an object in more than one way as a cell complex, or perhaps in no ways at all. (This is clear in topology: not all topological spaces are cell complexes!) But in $Cat$ with the above three cells, there is the special property that every object admits a cell complex structure. The nice thing about cell complexes is that once you've *chosen* a cell complex structure on a particular object, then you can argue by induction up the cell complex. This gives us a way to prove things about all cell complexes. For instance, we can prove something about arbitrary categories if we can prove that it is preserved by all three types of cell attachments, and by passage to colimits. Is this is the analogy to structural induction that you're thinking of?</code></div><div> <blockquote> <p>I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be “updates”.</p> </blockquote> <p>Are you suggesting that the idea of one thing coming “after” another in the ordering relation used for structural induction is analogous to the idea of one category being generated by adding objects or morphisms or relations to another one? If so, then I think the phrase ordering <em>relation</em> is misleading, because a category can be generated in many such ways.</p> <p>Perhaps what you are looking for is the idea of categorical cell complexes. Suppose in some category (this in an “ambient” category, not the categories you want to build with updates) we have a collection of morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>S</mi> <mi>i</mi></msub><mo>&rightarrow;</mo><msub><mi>D</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">S_i \to D_i</annotation></semantics></math>, called “cells” or “generating cofibrations”. In topology we think of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>S</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">S_i</annotation></semantics></math> as a “sphere” of some dimension, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>D</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">D_i</annotation></semantics></math> as a “disc”, and the map as the inclusion of a sphere as the boundary of the disc of one higher dimension. In terms of your “updates” you can think of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>S</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">S_i</annotation></semantics></math> as specifying the data that you might have before your update, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>D</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">D_i</annotation></semantics></math> as the result of the update. Then the operation of “attaching a cell”, which might roughly correspond to your “updates”, means pushing out one of these morphisms:</p> <math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mi>S</mi> <mi>i</mi></msub></mtd> <mtd><mo>&rightarrow;</mo></mtd> <mtd><mi>X</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">&downarrow;</mo></mtd> <mtd/> <mtd><mo stretchy="false">&downarrow;</mo></mtd></mtr> <mtr><mtd><msub><mi>D</mi> <mi>i</mi></msub></mtd> <mtd><mo>&rightarrow;</mo></mtd> <mtd><mi>X</mi><msub><mo>&sqcup;</mo> <mrow><msub><mi>S</mi> <mi>i</mi></msub></mrow></msub><msub><mi>D</mi> <mi>i</mi></msub></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ S_i & \to & X \\ \downarrow && \downarrow \\ D_i & \to & X \sqcup_{S_i} D_i }</annotation></semantics></math> <p>For instance, in the ambient category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math>, we can consider the following morphisms as our cells:</p> <ul> <li><p>The inclusion <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mn>0</mn><mo>&rightarrow;</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">0\to 1</annotation></semantics></math> of the empty category into the trivial category.</p></li> <li><p>The inclusion <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mn>2</mn><mo>&rightarrow;</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">2\to I</annotation></semantics></math> of the two-object discrete category into the <a href="https://ncatlab.org/nlab/show/interval category">interval category</a>.</p></li> <li><p>The map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>P</mi><mo>&rightarrow;</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">P \to I</annotation></semantics></math> from the walking <a href="https://ncatlab.org/nlab/show/parallel pair">parallel pair</a> (which has two objects <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> and two nonidentity morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>x</mi><mo>&rightrightarrows;</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x\rightrightarrows y</annotation></semantics></math>) to the interval category.</p></li> </ul> <p>Then attaching a cell of the first type means adding an object. Attaching a cell of the second type means adding a morphism (and, in consequence, freely adding all composites of that morphism with the existing morphisms in the category). And attaching a cell of the third type means forcing two given morphisms to become equal (along with all other equalities of morphisms that that entails).</p> <p>In general, a <em>cell complex</em> is an object together with a way to build it up with a (possibly transfinite) sequence of cell attachments of this sort. (In the transfinite sequence we just take colimits at limit ordinals.) Being a cell complex is <em>structure</em> on an object: we may be able to build up an object in more than one way as a cell complex, or perhaps in no ways at all. (This is clear in topology: not all topological spaces are cell complexes!) But in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> with the above three cells, there is the special property that every object admits a cell complex structure.</p> <p>The nice thing about cell complexes is that once you’ve <em>chosen</em> a cell complex structure on a particular object, then you can argue by induction up the cell complex. This gives us a way to prove things about all cell complexes. For instance, we can prove something about arbitrary categories if we can prove that it is preserved by all three types of cell attachments, and by passage to colimits. Is this is the analogy to structural induction that you’re thinking of?</p> </div> </div> </li><li id="Comment_31573"> <a id="Item_7"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>7.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></li> <li><span>CommentTime</span>May 19th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31573#Comment_31573">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31573"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/304/">Ben_Sprott</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>Hi Mike, I apologize for not replying. The simple fact is that your answer went over my head. I notice that you have agreed with me in spirit that we seem to have, at least according to your perscription, a foundation to have theorems in the theory of categories which are given, or proved, in an inductive way. I need to go over your suggestion carefully to see if it is what I am thinking about. In any case, thanks for the response!</code></div><div> <p>Hi Mike,</p> <p>I apologize for not replying. The simple fact is that your answer went over my head. I notice that you have agreed with me in spirit that we seem to have, at least according to your perscription, a foundation to have theorems in the theory of categories which are given, or proved, in an inductive way. I need to go over your suggestion carefully to see if it is what I am thinking about. In any case, thanks for the response!</p> </div> </div> </li><li id="Comment_31589" class="Alternate"> <a id="Item_8"></a> <div class="CommentHeader"> <ul> <li><span>CommentRowNumber</span>8.</li><li><span>CommentAuthor</span><a href="https://nforum.ncatlab.org/account/3/">Mike Shulman</a></li> <li><span>CommentTime</span>May 20th 2012</li></ul></div> <div class="CommentActions"> <div class="CommentActionsInner"><ul class="CommentActionsList"><li><a href="https://nforum.ncatlab.org/discussion/3782/structural-induction-over-categories/?Focus=31589#Comment_31589">PermaLink</a></li></ul></div></div><div class="CommentBody" id="CommentBody_31589"><div class="source" style="display: none;"><span class="sourceType">Author: <a href="https://nforum.ncatlab.org/account/3/">Mike Shulman</a></span><br/><span class="sourceType">Format: MarkdownItex</span><code>Sorry about that; I guessed that it might. You could try learning some Quillen model category theory, which is where the abstract notion of cell complex originates.</code></div><div> <p>Sorry about that; I guessed that it might. You could try learning some Quillen model category theory, which is where the abstract notion of cell complex originates.</p> </div> </div> </li></ol> </div><div class="ContentInfo Middle"> <div class="PageInfo"> <p>1 to 8 of 8</p> <ol class="PageList PageListEmpty"> <li> </li> </ol> </div> </div></div> <a id="pgbottom" > </a> </div> </div></body> </html>