{"id":2991,"date":"2022-06-19T14:50:46","date_gmt":"2022-06-19T21:50:46","guid":{"rendered":"https:\/\/harrydole.com\/wp\/?p=2991"},"modified":"2023-12-14T10:57:54","modified_gmt":"2023-12-14T18:57:54","slug":"catecon-identity-is-isomorphism","status":"publish","type":"post","link":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/","title":{"rendered":"Catecon: Identity Is Isomorphism"},"content":{"rendered":"\n<iframe loading=\"lazy\" src=\"https:\/\/www.youtube.com\/embed\/_GaV4xR0EpY\" title=\"YouTube video player\" allow=\"accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen=\"\" width=\"560\" height=\"315\" frameborder=\"0\"><\/iframe>\n\n\n\n<p>See diagrams at <a href=\"https:\/\/catecon.net\/d\/hdole\/identity\">https:\/\/catecon.net\/d\/hdole\/identity<\/a> and <a href=\"https:\/\/catecon.net\/d\/hdole\/isomorphism\">https:\/\/catecon.net\/d\/hdole\/isomorphism<\/a>.<\/p>\n<p>Today, let&#8217;s define the notions of identity and isomorphism.<\/p>\n<p>Then show in Catecon how an identity is an isomorphism.<\/p>\n<p>Let&#8217;s get morphing!<\/p>\n<p>Create a new diagram called identity.<\/p>\n<p>CT&#8217;s say &#8220;The morphism id on an object A in the category D is an identity if for every f with domain A that f composed with id is f, and for every g with codomain A that id composed with g is g.&#8221;<\/p>\n<p>Let&#8217;s express this in a diagrammatic form with quantifiers.<\/p>\n<p>The so-called internal version has been handled in a different video on the internal defintion of a category.<\/p>\n<p>Create a category D and switch the categorical context.<\/p>\n<p>In the category D, create a morphism called id from A to A.<\/p>\n<p>Next create a morphism f from A to B and attach thusly.<\/p>\n<p>Now similarly for a g from B to A.<\/p>\n<p>Assert both cells, select something on both blobs, and hit definition<\/p>\n<p>First we see the three morphisms listed: id, f and g.<\/p>\n<p>Hover over f and notice the upsidedown A for universal quantifier.<\/p>\n<p>Click on it for f and noticeit moves next to the blob that uses f.<\/p>\n<p>Notice that the commutativity symbol for f&#8217;s cell now has a pair of parenthesis denoting that it comes after the universal quantifier.<\/p>\n<p>Do the same for g.<\/p>\n<p>Now we create our definition for identity.<\/p>\n<p>Next up, the definition of an isomorphism.<\/p>\n<p>Create a diagram called isomorphism.<\/p>\n<p>No universal quantifiers needed here.<\/p>\n<p>The morphism f from A to B in the category D is said to be invertible (an isomorphism) if there exists a morphism f inverse from B to A such that f composed with the inverse is the identity, and the inverse with f also the identity.<\/p>\n<p>Or, such that the following diagrams commute.<\/p>\n<p>In the category D create the morphism f from A to B, and f inverse from B to A.<\/p>\n<p>Arrange appropriately and assert.<\/p>\n<p>Copy and assert.<\/p>\n<p>Now select both blobs and click definition.<\/p>\n<p>No need for quantifiers as what we&#8217;re trying to express is that when presented with the pair f and f inverse, then the pair is an isomorphism when the following cells commute.<\/p>\n<p>Call it iso and create.<\/p>\n<p>Now show an identity is an isomorphism.<\/p>\n<p>How to do that?<\/p>\n<p>Classically one says &#8220;Let id be an identity on the object T in the category D&#8221;.<\/p>\n<p>In Catecon, we instantiate in this diagram our prior definition of identity.<\/p>\n<p>The identity diagram is in our current session, click on the background and access definitions.<\/p>\n<p>Select our context for the definition to be D and then select identity.<\/p>\n<p>For the instantiation, we need to give two base names, one corresponding to the A in the original definition of identity, and similarly for the id morphism.<\/p>\n<p>We&#8217;ll put in T for A, and leave id as it is.<\/p>\n<p>Submitting then creates the text entry &#8220;Let id from T to T as identity&#8221;.<\/p>\n<p>Now select the definition of isomorphism and note the &#8216;form theorm&#8217; action.<\/p>\n<p>Click it.<\/p>\n<p>We then map the morphisms of the definition instance of the identity to the morphisms of the definition of isomorphism.<\/p>\n<p>Give it a name, id is iso.<\/p>\n<p>Do the action.<\/p>\n<p>You now see two cells generated from the definition of isomorphism with the morphisms from the identity instance.<\/p>\n<p>It is good to see that the equality engine notes that these are commutative cells.<\/p>\n<p>And we see our theorem stated as a text object, but there is another way to see it.<\/p>\n<p>If we look at the Actions diagram, and control-home to the end where the user actions are added, and we see the morphism from id to iso that represents our proof.<\/p>\n<p>Quod erat demonstrandum, identity is isomorphism.<\/p>\n<p>&nbsp;<\/p>\n\n\n","protected":false},"excerpt":{"rendered":"<p>See diagrams at https:\/\/catecon.net\/d\/hdole\/identity and https:\/\/catecon.net\/d\/hdole\/isomorphism. Today, let&#8217;s define the notions of identity and isomorphism. Then show in Catecon how an identity is an isomorphism. Let&#8217;s get morphing! Create a new diagram called identity. CT&#8217;s say &#8220;The morphism id on an object A in the category D is an identity if for every f with&hellip; <\/p>\n<p class=\"more-link-p\"><a class=\"more-link\" href=\"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":2,"featured_media":2993,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[32],"tags":[33,28,41],"class_list":["post-2991","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-catecon","tag-catecon","tag-category-theory","tag-math","xfolkentry","clearfix"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.5 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Catecon: Identity Is Isomorphism - Harry Dole<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Catecon: Identity Is Isomorphism - Harry Dole\" \/>\n<meta property=\"og:description\" content=\"See diagrams at https:\/\/catecon.net\/d\/hdole\/identity and https:\/\/catecon.net\/d\/hdole\/isomorphism. Today, let&#8217;s define the notions of identity and isomorphism. Then show in Catecon how an identity is an isomorphism. Let&#8217;s get morphing! Create a new diagram called identity. CT&#8217;s say &#8220;The morphism id on an object A in the category D is an identity if for every f with&hellip; Continue reading &rarr;\" \/>\n<meta property=\"og:url\" content=\"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/\" \/>\n<meta property=\"og:site_name\" content=\"Harry Dole\" \/>\n<meta property=\"article:published_time\" content=\"2022-06-19T21:50:46+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2023-12-14T18:57:54+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png\" \/>\n\t<meta property=\"og:image:width\" content=\"3840\" \/>\n\t<meta property=\"og:image:height\" content=\"2160\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/png\" \/>\n<meta name=\"author\" content=\"Harry Dole\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Harry Dole\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"3 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/\"},\"author\":{\"name\":\"Harry Dole\",\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#\\\/schema\\\/person\\\/da373a629b425372a0d15abd61d36610\"},\"headline\":\"Catecon: Identity Is Isomorphism\",\"datePublished\":\"2022-06-19T21:50:46+00:00\",\"dateModified\":\"2023-12-14T18:57:54+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/\"},\"wordCount\":638,\"publisher\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#\\\/schema\\\/person\\\/da373a629b425372a0d15abd61d36610\"},\"image\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/i0.wp.com\\\/harrydole.com\\\/wp\\\/wp-content\\\/uploads\\\/2022\\\/06\\\/identity-thumbnail.png?fit=3840%2C2160&ssl=1\",\"keywords\":[\"Catecon\",\"Category Theory\",\"Math\"],\"articleSection\":[\"Catecon\"],\"inLanguage\":\"en-US\"},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/\",\"url\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/\",\"name\":\"Catecon: Identity Is Isomorphism - Harry Dole\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/i0.wp.com\\\/harrydole.com\\\/wp\\\/wp-content\\\/uploads\\\/2022\\\/06\\\/identity-thumbnail.png?fit=3840%2C2160&ssl=1\",\"datePublished\":\"2022-06-19T21:50:46+00:00\",\"dateModified\":\"2023-12-14T18:57:54+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#primaryimage\",\"url\":\"https:\\\/\\\/i0.wp.com\\\/harrydole.com\\\/wp\\\/wp-content\\\/uploads\\\/2022\\\/06\\\/identity-thumbnail.png?fit=3840%2C2160&ssl=1\",\"contentUrl\":\"https:\\\/\\\/i0.wp.com\\\/harrydole.com\\\/wp\\\/wp-content\\\/uploads\\\/2022\\\/06\\\/identity-thumbnail.png?fit=3840%2C2160&ssl=1\",\"width\":3840,\"height\":2160},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/2022\\\/06\\\/19\\\/catecon-identity-is-isomorphism\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Catecon: Identity Is Isomorphism\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#website\",\"url\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/\",\"name\":\"Harry Dole\",\"description\":\"&quot;...And one day a great and mighty wind will encompass the surface of the earth and wipe clean the scourge of wooly thinking once and for all!&quot; -- Time Bandits\",\"publisher\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#\\\/schema\\\/person\\\/da373a629b425372a0d15abd61d36610\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"},{\"@type\":[\"Person\",\"Organization\"],\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#\\\/schema\\\/person\\\/da373a629b425372a0d15abd61d36610\",\"name\":\"Harry Dole\",\"logo\":{\"@id\":\"https:\\\/\\\/harrydole.com\\\/wp\\\/#\\\/schema\\\/person\\\/image\\\/\"},\"sameAs\":[\"https:\\\/\\\/harrydole.com\"]}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Catecon: Identity Is Isomorphism - Harry Dole","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/","og_locale":"en_US","og_type":"article","og_title":"Catecon: Identity Is Isomorphism - Harry Dole","og_description":"See diagrams at https:\/\/catecon.net\/d\/hdole\/identity and https:\/\/catecon.net\/d\/hdole\/isomorphism. Today, let&#8217;s define the notions of identity and isomorphism. Then show in Catecon how an identity is an isomorphism. Let&#8217;s get morphing! Create a new diagram called identity. CT&#8217;s say &#8220;The morphism id on an object A in the category D is an identity if for every f with&hellip; Continue reading &rarr;","og_url":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/","og_site_name":"Harry Dole","article_published_time":"2022-06-19T21:50:46+00:00","article_modified_time":"2023-12-14T18:57:54+00:00","og_image":[{"width":3840,"height":2160,"url":"https:\/\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png","type":"image\/png"}],"author":"Harry Dole","twitter_card":"summary_large_image","twitter_misc":{"Written by":"Harry Dole","Est. reading time":"3 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#article","isPartOf":{"@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/"},"author":{"name":"Harry Dole","@id":"https:\/\/harrydole.com\/wp\/#\/schema\/person\/da373a629b425372a0d15abd61d36610"},"headline":"Catecon: Identity Is Isomorphism","datePublished":"2022-06-19T21:50:46+00:00","dateModified":"2023-12-14T18:57:54+00:00","mainEntityOfPage":{"@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/"},"wordCount":638,"publisher":{"@id":"https:\/\/harrydole.com\/wp\/#\/schema\/person\/da373a629b425372a0d15abd61d36610"},"image":{"@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#primaryimage"},"thumbnailUrl":"https:\/\/i0.wp.com\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png?fit=3840%2C2160&ssl=1","keywords":["Catecon","Category Theory","Math"],"articleSection":["Catecon"],"inLanguage":"en-US"},{"@type":"WebPage","@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/","url":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/","name":"Catecon: Identity Is Isomorphism - Harry Dole","isPartOf":{"@id":"https:\/\/harrydole.com\/wp\/#website"},"primaryImageOfPage":{"@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#primaryimage"},"image":{"@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#primaryimage"},"thumbnailUrl":"https:\/\/i0.wp.com\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png?fit=3840%2C2160&ssl=1","datePublished":"2022-06-19T21:50:46+00:00","dateModified":"2023-12-14T18:57:54+00:00","breadcrumb":{"@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#primaryimage","url":"https:\/\/i0.wp.com\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png?fit=3840%2C2160&ssl=1","contentUrl":"https:\/\/i0.wp.com\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png?fit=3840%2C2160&ssl=1","width":3840,"height":2160},{"@type":"BreadcrumbList","@id":"https:\/\/harrydole.com\/wp\/2022\/06\/19\/catecon-identity-is-isomorphism\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/harrydole.com\/wp\/"},{"@type":"ListItem","position":2,"name":"Catecon: Identity Is Isomorphism"}]},{"@type":"WebSite","@id":"https:\/\/harrydole.com\/wp\/#website","url":"https:\/\/harrydole.com\/wp\/","name":"Harry Dole","description":"&quot;...And one day a great and mighty wind will encompass the surface of the earth and wipe clean the scourge of wooly thinking once and for all!&quot; -- Time Bandits","publisher":{"@id":"https:\/\/harrydole.com\/wp\/#\/schema\/person\/da373a629b425372a0d15abd61d36610"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/harrydole.com\/wp\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"},{"@type":["Person","Organization"],"@id":"https:\/\/harrydole.com\/wp\/#\/schema\/person\/da373a629b425372a0d15abd61d36610","name":"Harry Dole","logo":{"@id":"https:\/\/harrydole.com\/wp\/#\/schema\/person\/image\/"},"sameAs":["https:\/\/harrydole.com"]}]}},"jetpack_featured_media_url":"https:\/\/i0.wp.com\/harrydole.com\/wp\/wp-content\/uploads\/2022\/06\/identity-thumbnail.png?fit=3840%2C2160&ssl=1","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/posts\/2991","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/comments?post=2991"}],"version-history":[{"count":3,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/posts\/2991\/revisions"}],"predecessor-version":[{"id":3001,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/posts\/2991\/revisions\/3001"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/media\/2993"}],"wp:attachment":[{"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/media?parent=2991"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/categories?post=2991"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/harrydole.com\/wp\/wp-json\/wp\/v2\/tags?post=2991"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}