Commit: 5f48895d0069b686eb6a43605ee117304d7b874d - catabase (git)

A database of categories

Commit MetaInfo

• Revisión: 5f48895d0069b686eb6a43605ee117304d7b874d (tree)
• Tiempo: 2021-09-11 12:26:18
• Autor: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Refactor more subcategories.

Add double categories, fix up incorrect parts of simplicial objects,
improve restriction categories.

Cambiar Resumen

• modified: catabase.db
• modified: templates/row-catabase-categories.html
• modified: templates/row-catabase-categories_of_simplicial_objects.html
• add: templates/row-catabase-double_categories.html
• modified: templates/row-catabase-full_subcategories.html
• add: templates/row-catabase-reflective_subcategories.html
• modified: templates/row-catabase-restriction_categories.html
• add: templates/table-catabase-all_double_categories.html
• modified: templates/table-catabase-all_full_subcategories.html
• add: templates/table-catabase-restriction_categories.html

Diferencia incremental

Binary files a/catabase.db and b/catabase.db differ

--- a/templates/row-catabase-categories.html
+++ b/templates/row-catabase-categories.html
@@ -51,28 +51,17 @@ SSet).</p>
 <p>{{ name }} is semiadditive; products and sums coincide (enriched in CMon).</p>
 {% endif %}
 
-{% set subcats = sql("select subcategory from subcategories where parent = ?", [name]) %}
+{% set subcats = sql(
+"select * from all_subcategories where supercategory = ?", [name]) %}
 {% if subcats %}
-<h2>Subcategories</h2>
+<h2>Notable Subcategories</h2>
 <ul>
     {% for subcat in subcats %}
-    <li>{{ subcat["subcategory"] }}</li>
+    <li>{{ subcat["subcategory"] }} ({{ subcat["kind"] }})</li>
     {% endfor %}
 </ul>
-{% endif %}
-
-<h2>Derived Categories</h2>
-{% set birel = sql("select internal_relations from bicategories_of_relations where parent = ?", [name]) %}
-{% if birel %}
-<p>The bicategory-of-relations construction yields the category {{ birel[0]["internal_relations"] }}</p>
-{% endif %}
-{% set mon = sql("select * from categories_of_monoids where parent = ?", [name]) %}
-{% if mon %}
-<p>The internal monoids form the category {{ mon[0]["internal_monoids"] }}</p>
-{% endif %}
-{% set cmon = sql("select * from categories_of_commutative_monoids where parent = ?", [name]) %}
-{% if cmon %}
-<p>The internal commutative monoids form the category {{ cmon[0]["internal_commutative_monoids"] }}</p>
+{% else %}
+<p>({{ name }} doesn't seem to have any notable subcategories.)</p>
 {% endif %}
 
 <h2>Limits</h2>

--- a/templates/row-catabase-categories_of_simplicial_objects.html
+++ b/templates/row-catabase-categories_of_simplicial_objects.html
@@ -7,14 +7,14 @@
 
 <h1>Category of Simplicial Objects: {{ sscat }}</h1>
 
-<p>{{ sscat }} is a full subcategory of {{ cat }} whose objects are all
-internal simplicial objects. A simplicial object in {{ cat }} is a
-contravariant functor from Δ to {{ cat }}, so the category of simplicial
-objects is a contravariant functor category:</p>
+<p>{{ sscat }} is a contravariant functor category from Δ to {{ cat }}:</p>
 
 <div class="bigmath">
     {{ sscat }} ≅ [Δ°, {{ cat }}]
 </div>
 
+<p>The objects of {{ sscat }} are traditionally called "simplicial objects",
+and {{ sscat }} is a category of simplicial objects.</p>
+
 {{ super() }}
 {% endblock %}

--- /dev/null
+++ b/templates/row-catabase-double_categories.html
@@ -0,0 +1,39 @@
+{% extends "default:row.html" %}
+
+{% block content %}
+
+{% set v2cat = display_rows[0]["vertical_2cat"] %}
+{% set h2cat = display_rows[0]["horizontal_2cat"] %}
+{% set squares = display_rows[0]["2cells_hr"] %}
+{% set vrow = sql(
+"select objects_hr, arrows_hr from categories where name = ?", [v2cat])[0] %}
+{% set hrow = sql(
+"select objects_hr, arrows_hr from categories where name = ?", [h2cat])[0] %}
+{% set vobjs = vrow["objects_hr"] %}
+{% set varrs = vrow["arrows_hr"] %}
+{% set hobjs = hrow["objects_hr"] %}
+{% set harrs = hrow["arrows_hr"] %}
+
+{% set objs = vobjs if vobjs == hobjs else vobjs + " or " + hobjs %}
+
+<h1>Double Category: <u>{{ v2cat }}</u></h1>
+
+<p><u>{{ v2cat }}</u> is a double category assembled from the categories
+{{ v2cat }} and {{ h2cat }}. Its objects are {{ objs }}, its horizontal
+arrows are {{ harrs }}, its vertical arrows are {{ varrs }}, and its
+squares are {{ squares }}. As with all double categories, we may transpose
+horizontal and vertical arrows to obtain another double category.</p>
+
+<p>The horizontal and vertical 2-category functors send <u>{{ v2cat }}</u> to
+the 2-categories {{ h2cat }} and {{ v2cat }} respectively, augmented with
+{{ squares }} for 2-cells:</p>
+
+<div class="bigmath">
+    𝓗(<u>{{ v2cat }}</u>) ≅ {{ h2cat }}
+    <br />
+    𝓥(<u>{{ v2cat }}</u>) ≅ {{ v2cat }}
+</div>
+
+{{ super() }}
+{% endblock %}
+

--- a/templates/row-catabase-full_subcategories.html
+++ b/templates/row-catabase-full_subcategories.html
@@ -12,5 +12,8 @@
 {{ sub }} has only some of the objects of {{ sup }}, but all of the
 arrows.</p>
 
+<p>In terms of stuff, structure, and properties, objects of {{ sub }} are like
+objects of {{ sup }} but with extra properties.</p>
+
 {{ super() }}
 {% endblock %}

--- /dev/null
+++ b/templates/row-catabase-reflective_subcategories.html
@@ -0,0 +1,35 @@
+{% extends "default:row.html" %}
+
+{% block content %}
+
+{% set subcat = display_rows[0]["subcategory"] %}
+{% set supercat = display_rows[0]["supercategory"] %}
+{% set reflector = display_rows[0]["reflector_hr"] %}
+{% set reflection = display_rows[0]["reflection_hr"] %}
+
+<h1>Reflective Subcategory: {{ subcat }}</h1>
+
+<p>{{ subcat }} is a reflective subcategory of {{ supercat }}, by which we
+mean that {{ subcat }} is a full subcategory whose inclusion functor has
+a left adjoint. The inclusion functor i is called the <dfn>reflection</dfn>
+and the left adjoint is called the <dfn>reflector</dfn>.</p>
+
+{% if reflector %}
+<p>Reflectors tend to be meaningful, and in this case, the functor which
+reflects {{ supercat }} to {{ subcat }} is called the
+<em>{{ reflector }} functor</em> of {{ supercat }}.</p>
+{% endif %}
+
+{% if reflection %}
+<p>Similarly, reflections tend to be meaningful too, and in this case, the
+functor which includes {{ subcat }} into {{ supercat }} is called the
+<em>{{ reflection }} functor</em> of {{ subcat }}.</p>
+{% endif %}
+
+<p>In terms of stuff, structure, and properties, objects of {{ supercat }} are like
+objects of {{ subcat }} but with extra stuff; this is the reflection of the
+fact that, because {{ subcat }} is a full subcategory, objects of {{ subcat }}
+are like objects of {{ supercat }} but with extra properties.</p>
+
+{{ super() }}
+{% endblock %}

--- a/templates/row-catabase-restriction_categories.html
+++ b/templates/row-catabase-restriction_categories.html
@@ -8,16 +8,9 @@
 <h1>Restriction Categories: {{ parcat }}</h1>
 
 <p>{{ parcat }} is a restriction category; its arrows are partial maps and it
-contains {{ subcat }} as a subcategory with total maps.</p>
-
-<p>There is a functor from restriction categories to categories:</p>
-
-<div class="bigmath">
-    Total : RCat → Cat
-</div>
-
-<p>There are many subcategories, but only {{ subcat }} is the total
-subcategory of {{ parcat }}:</p>
+contains {{ subcat }} as a subcategory with total maps. There are many
+subcategories, but only {{ subcat }} is the total subcategory of
+{{ parcat }}:</p>
 
 <div class="bigmath">
     Total({{ parcat }}) ≅ {{ subcat }}

--- /dev/null
+++ b/templates/table-catabase-all_double_categories.html
@@ -0,0 +1,38 @@
+{% extends "default:table.html" %}
+
+{% block content %}
+
+<h1>Double Categories</h1>
+
+<p>A double category is a generalized 2-category. A 2-category has objects,
+arrows, and natural transformations; arrows have one type of composition, but
+natural transformations have two types of composition, vertical and horizontal
+composition. A double category has two types of arrows, vertical and
+horizontal arrows, as well as natural transformations.</p>
+
+<p>Every 2-category can be regarded as a double category with only one type of
+arrow. Similarly, every category can be regarded as a double category with
+only one type of arrow, using commuting squares of arrows for natural
+transformations. Every category's slice and coslice categories can be paired
+to form a double category.</p>
+
+<p>By the Macrocosm Principle, there is a category DblCat whose objects are
+double categories and arrows are double functors; this is the category of
+internal categories in Cat. There are two functors which designate the
+2-categories resulting from restricting the vertical and horizontal arrows
+respectively to identities; they are known as the horizontal and vertical
+2-categories.</p>
+
+<div class="bigmath">
+    𝓗, 𝓥 : DblCat → 2Cat
+</div>
+
+<p>There are several common constructions for double categories which are
+included from other tables:</p>
+
+<ul>
+    <li>Every restriction category gives a double category.</li>
+</ul>
+
+{{ super() }}
+{% endblock %}

--- a/templates/table-catabase-all_full_subcategories.html
+++ b/templates/table-catabase-all_full_subcategories.html
@@ -8,7 +8,7 @@
 There are several special cases:</p>
 
 <ul>
-    <li>Categories of simplicial objects are full.</li>
+    <li>Reflective subcategories are full.</li>
 </ul>
 
 {{ super() }}

--- /dev/null
+++ b/templates/table-catabase-restriction_categories.html
@@ -0,0 +1,29 @@
+{% extends "default:row.html" %}
+
+{% block content %}
+
+<h1>Restriction Categories</h1>
+
+<p>A restriction category is a category with a restriction operator which
+restricts each arrow to a subdomain. By analogy, the original category's
+arrows are partial, but the arrows of the subcategory obtained by restricting
+every arrow are total.</p>
+
+<p>The restriction operator extends to a functor from restriction categories
+to categories:</p>
+
+<div class="bigmath">
+    Total : RCat → Cat
+</div>
+
+<p>Additionally, every restriction category forms a double category whose
+vertical arrows are the original partial arrows and horizontal arrows are the
+restricted total arrows. This construction also extends to a functor from
+restriction categories to double categories:</p>
+
+<div class="bigmath">
+    Dc : RCat → DblCat
+</div>
+
+{{ super() }}
+{% endblock %}