• R/O
  • HTTP
  • SSH
  • HTTPS

提交

标签
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#windowsobjective-ccocoa誰得qtpythonphprubygameguibathyscaphec計画中(planning stage)翻訳omegatframeworktwitterdomtestvb.netdirectxゲームエンジンbtronarduinopreviewer

A database of categories


Commit MetaInfo

修订版7989f2fca513b79c7f78f0985f89f17a7dce37ef (tree)
时间2021-09-02 14:17:34
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Add many row templates.

更改概述

差异

Binary files a/catabase.db and b/catabase.db differ
--- /dev/null
+++ b/templates/row-catabase-categories_of_groups.html
@@ -0,0 +1,18 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set cat = display_rows[0]["parent"] %}
6+{% set grpcat = display_rows[0]["internal_groups"] %}
7+
8+<h1>Category of Groups: {{ grpcat }}</h1>
9+
10+<p>{{ grpcat }} is a subcategory of {{ cat }} whose objects are all internal
11+groups:</p>
12+
13+<div class="bigmath">
14+ Grp({{ cat }}) ≅ {{ grpcat }}
15+</div>
16+
17+{{ super() }}
18+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-categories_of_monoids.html
@@ -0,0 +1,21 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set cat = display_rows[0]["parent"] %}
6+{% set moncat = display_rows[0]["internal_monoids"] %}
7+
8+<h1>Category of Monoids: {{ moncat }}</h1>
9+
10+<p>{{ moncat }} is a subcategory of {{ cat }} whose objects are all internal
11+monoids:</p>
12+
13+<div class="bigmath">
14+ Mon({{ cat }}) ≅ {{ moncat }}
15+</div>
16+
17+<p>Note that {{ cat }} must be a monoidal category in order to even have
18+internal monoids. This is an instance of the Microcosm Principle.</p>
19+
20+{{ super() }}
21+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-categories_of_simplicial_objects.html
@@ -0,0 +1,20 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set cat = display_rows[0]["parent"] %}
6+{% set sscat = display_rows[0]["internal_simplicial_sets"] %}
7+
8+<h1>Category of Simplicial Objects: {{ sscat }}</h1>
9+
10+<p>{{ sscat }} is a full subcategory of {{ cat }} whose objects are all
11+internal simplicial objects. A simplicial object in {{ cat }} is a
12+contravariant functor from Δ to {{ cat }}, so the category of simplicial
13+objects is a contravariant functor category:</p>
14+
15+<div class="bigmath">
16+ {{ sscat }} ≅ [Δ°, {{ cat }}]
17+</div>
18+
19+{{ super() }}
20+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-equivalent_categories.html
@@ -0,0 +1,17 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set cat1 = display_rows[0]["cat1"] %}
6+{% set cat2 = display_rows[0]["cat2"] %}
7+
8+<h1>Equivalence of Categories: {{ cat1 }} ≅ {{ cat2 }}</h1>
9+
10+<p>{{ cat1 }} is equivalent to {{ cat2 }}, and vice versa.</p>
11+
12+<div class="bigmath">
13+ {{ cat1 }} ≅ {{ cat2 }}
14+</div>
15+
16+{{ super() }}
17+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-full_subcategories.html
@@ -0,0 +1,16 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set sub = display_rows[0]["subcategory"] %}
6+{% set sup = display_rows[0]["supercategory"] %}
7+
8+<h1>Full Subcategory: {{ sub }} ⊊ {{ sup }}</h1>
9+
10+<p>{{ sub }} is a full subcategory of {{ sup }}. When any two objects of
11+{{ sup }} are in {{ sub }}, so is every arrow between them. Put another way,
12+{{ sub }} has only some of the objects of {{ sup }}, but all of the
13+arrows.</p>
14+
15+{{ super() }}
16+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-limits.html
@@ -0,0 +1,18 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set diagram = display_rows[0]["diagram"] %}
6+{% set is_colimit = display_rows[0]["is_colimit"] %}
7+{% set construction = display_rows[0]["construction"] %}
8+{% set lim = "colimit" if is_colimit else "limit" %}
9+{% set Lim = "Colimit" if is_colimit else "Limit" %}
10+
11+<h1>{{ Lim }}: {{ construction }}</h1>
12+
13+<p>A {{ construction }} is a kind of {{ lim }}. Given a {{ diagram }},
14+considered as a diagram in some category, a {{ construction }} is the
15+{{ lim }} of that {{ diagram }} in that category.</p>
16+
17+{{ super() }}
18+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-opposite_categories.html
@@ -0,0 +1,21 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set cat = display_rows[0]["category"] %}
6+{% set opcat = display_rows[0]["op"] %}
7+
8+{% if cat == opcat %}
9+<h1>Self-Opposite Category: {{ cat }}</h1>
10+
11+<p>{{ cat }} is equivalent to its opposite category.</p>
12+{% else %}
13+<h1>Opposite Categories: {{ cat }} &amp; {{ opcat }}</h1>
14+
15+<p>{{ cat }} and {{ opcat }} are opposites; they are equivalent, except that
16+the arrows in {{ cat }} are pointed in the opposite direction from in
17+{{ opcat }}.</p>
18+{% endif %}
19+
20+{{ super() }}
21+{% endblock %}
--- /dev/null
+++ b/templates/row-catabase-skeletons.html
@@ -0,0 +1,20 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set skel = display_rows[0]["skeleton"] %}
6+{% set cat = display_rows[0]["category"] %}
7+
8+<h1>Skeleton: {{ skel }}</h1>
9+
10+<p>{{ skel }} is a skeleton of {{ cat }}; {{ skel }} is equivalent to
11+{{ cat }} but has no isomorphisms. Less cryptically, isomorphic objects in
12+{{ cat }} are mapped to single objects in {{ skel }} representing their
13+equivalence classes.</p>
14+
15+<p>Skeletons are not quite functorial, because their construction requires the
16+Axiom of Choice.</p>
17+
18+{{ super() }}
19+{% endblock %}
20+
--- /dev/null
+++ b/templates/row-catabase-topoi.html
@@ -0,0 +1,28 @@
1+{% extends "default:row.html" %}
2+
3+{% block content %}
4+
5+{% set topos = display_rows[0]["category"] %}
6+<h1>Topos: {{ topos }}</h1>
7+
8+<p>{{ topos }} is a topos.</p>
9+
10+{% if display_rows[0]["is_grothendieck"] %}
11+<p>{{ topos }} is Grothendieck; it acts like a category of sheaves.</p>
12+{% endif %}
13+
14+{% if display_rows[0]["has_nno"] %}
15+<p>{{ topos }} has a natural numbers object.</p>
16+{% endif %}
17+
18+{% if display_rows[0]["is_boolean"] %}
19+<p>{{ topos }} is Boolean; the Law of Excluded Middle is valid within
20+{{ topos }}.</p>
21+{% endif %}
22+
23+{% if display_rows[0]["is_well_pointed"] %}
24+<p>{{ topos }} is well-pointed.</p>
25+{% endif %}
26+
27+{{ super() }}
28+{% endblock %}