From ed13f79c6f0c8a1b8062a7e24f3055ec1759ca4a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 1 Sep 2026 09:53:40 +0200 Subject: [PATCH 01/14] improve structure selector styling - use variant prop - refactor scoped styling - show label in nav mobile - put label next to selector in header --- src/components/Header.svelte | 2 +- src/components/NavMobile.svelte | 8 +---- src/components/StructureSelector.svelte | 47 +++++++++++++------------ 3 files changed, 26 insertions(+), 31 deletions(-) diff --git a/src/components/Header.svelte b/src/components/Header.svelte index 9cbdd9535..9d1a77ec1 100644 --- a/src/components/Header.svelte +++ b/src/components/Header.svelte @@ -33,7 +33,7 @@
- +
-
- -
+ {/snippet} - + diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructurePage.svelte similarity index 100% rename from src/pages/StructureDetailPage.svelte rename to src/pages/StructurePage.svelte diff --git a/src/routes/[type]/[id]/+page.svelte b/src/routes/[type]/[id]/+page.svelte index 51e3acc60..0e8f53fb5 100644 --- a/src/routes/[type]/[id]/+page.svelte +++ b/src/routes/[type]/[id]/+page.svelte @@ -1,12 +1,12 @@ {#if data.special_structure_data.type === 'category'} - + {:else} - + {/if} From 86adb0a2ba6cc0d87b1fcb7dacdaa1d9591a6efd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 1 Sep 2026 19:19:46 +0200 Subject: [PATCH 09/14] update end-to-end tests --- tests/categories.spec.ts | 12 ++++++------ tests/category-properties.spec.ts | 4 ++-- tests/functor-properties.spec.ts | 6 ++---- tests/functors.spec.ts | 10 +++++----- tests/morphism-properties.spec.ts | 6 ++---- tests/morphisms.spec.ts | 4 ++-- tests/symmetric_monoidal_categories.spec.ts | 2 +- 7 files changed, 20 insertions(+), 24 deletions(-) diff --git a/tests/categories.spec.ts b/tests/categories.spec.ts index 129179e8d..5ecf6387e 100644 --- a/tests/categories.spec.ts +++ b/tests/categories.spec.ts @@ -105,8 +105,8 @@ test('user can view category details', async ({ page }) => { const body = page.locator('body') - await expect(body).toContainText('Objects: commutative rings') - await expect(body).toContainText('Morphisms: ring homomorphisms') + await expect(body).toContainText('Objects commutative rings') + await expect(body).toContainText('Morphisms ring homomorphisms') await expect(page.getByRole('link', { name: 'nLab link' })).toBeVisible() await expect(body).toContainText('is cocomplete') await expect(body).toContainText('is locally finitely presentable') @@ -196,7 +196,7 @@ test('user can navigate to a related category', async ({ page }) => { await page.goto('/category/FinSet', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Related categories:' }) + .locator('strong:has-text("Related") + span') .getByRole('link', { name: 'category of sets', exact: true @@ -226,7 +226,7 @@ test('user can navigate to the dual category if it exists in the database', asyn ).toBeVisible() await page - .locator('li', { hasText: 'Dual category' }) + .locator('strong:has-text("Dual") + span') .getByRole('link', { name: 'dual of the category of sets', exact: true @@ -247,7 +247,7 @@ test('user can navigate to a child category', async ({ page }) => { await page.goto('/category/BG', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Children:' }) + .locator('strong:has-text("Children") + span') .getByRole('link', { name: 'delooping of a non-trivial finite group', exact: true @@ -268,7 +268,7 @@ test('user can navigate to a parent category', async ({ page }) => { await page.goto('/category/Ring', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Parent:' }) + .locator('strong:has-text("Parent") + span') .getByRole('link', { name: 'category of algebras', exact: true diff --git a/tests/category-properties.spec.ts b/tests/category-properties.spec.ts index 44f715298..1d87c12bb 100644 --- a/tests/category-properties.spec.ts +++ b/tests/category-properties.spec.ts @@ -54,7 +54,7 @@ test('user can view category property details', async ({ page }) => { ) const related_link = page - .locator('li', { hasText: 'Related properties:' }) + .locator('strong:has-text("Related") + span') .getByRole('link', { name: 'accessible', exact: true @@ -116,7 +116,7 @@ test('user can navigate to the dual property', async ({ page }) => { ).toBeVisible() await page - .locator('li', { hasText: 'Dual property:' }) + .locator('strong:has-text("Dual") + span') .getByRole('link', { name: 'coequalizers', exact: true diff --git a/tests/functor-properties.spec.ts b/tests/functor-properties.spec.ts index a74adf9f7..1ee8bd916 100644 --- a/tests/functor-properties.spec.ts +++ b/tests/functor-properties.spec.ts @@ -52,7 +52,7 @@ test('user can view functor property details', async ({ page }) => { await expect(page.locator('body')).toContainText('is faithful when') const related_link = page - .locator('li', { hasText: 'Related properties' }) + .locator('strong:has-text("Related") + span') .getByRole('link', { name: 'fully faithful', exact: true @@ -114,9 +114,7 @@ test('user can navigate to the dual property', async ({ page }) => { ).toBeVisible() await page - .locator('li', { - hasText: 'Dual property:' - }) + .locator('strong:has-text("Dual") + span') .getByRole('link', { name: 'right exact', exact: true diff --git a/tests/functors.spec.ts b/tests/functors.spec.ts index ee70244ea..8f3120388 100644 --- a/tests/functors.spec.ts +++ b/tests/functors.spec.ts @@ -146,7 +146,7 @@ test('user can navigate to a related functor', async ({ page }) => { await page.goto('/functor/forget_ring', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Related functors:' }) + .locator('strong:has-text("Related") + span') .getByRole('link', { name: 'forgetful functor for groups', exact: true @@ -167,7 +167,7 @@ test('user can navigate to the domain category', async ({ page }) => { await page.goto('/functor/forget_ring', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Domain:' }) + .locator('strong:has-text("Domain") + span') .getByRole('link', { name: 'category of rings', exact: true @@ -188,7 +188,7 @@ test('user can navigate to the codomain category', async ({ page }) => { await page.goto('/functor/group_units', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Codomain:' }) + .locator('strong:has-text("Codomain") + span') .getByRole('link', { name: 'category of groups', exact: true @@ -209,7 +209,7 @@ test('user can navigate to the left adjoint functor', async ({ page }) => { await page.goto('/functor/group_units', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Left adjoint:' }) + .locator('strong:has-text("Left adjoint") + span') .getByRole('link', { name: 'forgetful functor from groups to monoids', exact: true @@ -230,7 +230,7 @@ test('user can navigate to the right adjoint functor', async ({ page }) => { await page.goto('/functor/forget_topology', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Right adjoint:' }) + .locator('strong:has-text("Right adjoint") + span') .getByRole('link', { name: 'indiscrete topology functor', exact: true diff --git a/tests/morphism-properties.spec.ts b/tests/morphism-properties.spec.ts index f84df3d05..3a8b15bf4 100644 --- a/tests/morphism-properties.spec.ts +++ b/tests/morphism-properties.spec.ts @@ -52,7 +52,7 @@ test('user can view morphism property details', async ({ page }) => { await expect(page.locator('body')).toContainText('is an effective epimorphism if') const related_link = page - .locator('li', { hasText: 'Related properties' }) + .locator('strong:has-text("Related") + span') .getByRole('link', { name: 'regular epimorphism', exact: true @@ -114,9 +114,7 @@ test('user can navigate to the dual property', async ({ page }) => { ).toBeVisible() await page - .locator('li', { - hasText: 'Dual property:' - }) + .locator('strong:has-text("Dual") + span') .getByRole('link', { name: 'strict monomorphism', exact: true diff --git a/tests/morphisms.spec.ts b/tests/morphisms.spec.ts index b89d8650b..bcf6896bb 100644 --- a/tests/morphisms.spec.ts +++ b/tests/morphisms.spec.ts @@ -123,7 +123,7 @@ test('user can navigate to a related morphism', async ({ page }) => { await page.goto('/morphism/id_X', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Related morphisms:' }) + .locator('strong:has-text("Related") + span') .getByRole('link', { name: 'identity map of a group', exact: true @@ -144,7 +144,7 @@ test('user can navigate to the ambient category', async ({ page }) => { await page.goto('/morphism/fork-handle', { waitUntil: 'networkidle' }) await page - .locator('li', { hasText: 'Category:' }) + .locator('strong:has-text("Category") + span') .getByRole('link', { name: 'walking fork', exact: true diff --git a/tests/symmetric_monoidal_categories.spec.ts b/tests/symmetric_monoidal_categories.spec.ts index 749acddd1..35f40383e 100644 --- a/tests/symmetric_monoidal_categories.spec.ts +++ b/tests/symmetric_monoidal_categories.spec.ts @@ -66,7 +66,7 @@ test('user can navigate to the underlying category', async ({ page }) => { }) await page - .locator('li', { hasText: 'Underlying category:' }) + .locator('strong:has-text("Underlying category") + span') .getByRole('link', { name: 'category of sets', exact: true From 12b87d50c56c7f4acb253801bcaafdc30f184354 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 2 Sep 2026 08:14:06 +0200 Subject: [PATCH 10/14] shift heading hierarchy: h2 -> h1 and h3 -> h2 --- content/Top-embeds-in-LRS.md | 2 +- content/cocongruences_of_groups.md | 2 +- content/cogenerators_in_product_categories.md | 2 +- content/comphaus_copresentable.md | 4 +-- content/congruences_in_rel.md | 2 +- content/constant_morphisms.md | 2 +- content/contribute.md | 8 ++--- content/coslice-effective-congruences.md | 2 +- content/dual-properties.md | 10 +++---- content/effective-congruence-quotients.md | 2 +- content/foundations.md | 16 +++++----- content/functors_on_discrete_categories.md | 2 +- content/generator_construction.md | 2 +- content/inclusion-functors.md | 2 +- content/missing_cogenerating_sets.md | 2 +- content/missing_cogenerator.md | 2 +- content/monic_sequential_colimits.md | 2 +- content/natural_numbers_objects.md | 2 +- content/preadditive_structure_unique.md | 2 +- ...houts-of-monos-via-congruence-quotients.md | 2 +- content/relationships-epis-monos.md | 6 ++-- content/resources.md | 2 +- content/sifted-colimits-in-groupoids.md | 2 +- content/special_sequential_colimits.md | 2 +- content/subcategories.md | 2 +- content/thin_algebraic_categories.md | 2 +- content/thin_extremal_generator.md | 2 +- content/topos-with-generator.md | 2 +- src/components/CommentList.svelte | 2 +- src/components/Header.svelte | 7 ++--- .../IndistinguishableStructures.svelte | 2 +- src/components/Popup.svelte | 4 +-- src/components/PropertyAssignmentList.svelte | 8 ++--- src/components/StructuresBasedOn.svelte | 2 +- src/pages/CategoryPage.svelte | 4 +-- src/pages/ComparisonPage.svelte | 2 +- src/pages/ComparisonResultPage.svelte | 2 +- src/pages/ImplicationListPage.svelte | 2 +- src/pages/ImplicationPage.svelte | 4 +-- src/pages/PropertyListPage.svelte | 2 +- src/pages/PropertyPage.svelte | 12 ++++---- src/pages/SearchPage.svelte | 2 +- src/pages/SearchResultsPage.svelte | 2 +- src/pages/StructureListPage.svelte | 2 +- src/pages/StructurePage.svelte | 2 +- src/pages/TaggedPropertiesPage.svelte | 2 +- src/pages/TaggedStructuresPage.svelte | 2 +- src/routes/+page.svelte | 30 +++++++++---------- src/routes/app.css | 4 +-- src/routes/content/+page.svelte | 2 +- src/routes/content/[id]/+page.svelte | 2 +- src/routes/download/+page.svelte | 4 +-- src/routes/missing/+page.svelte | 10 +++---- src/routes/settings/+page.svelte | 6 ++-- 54 files changed, 106 insertions(+), 107 deletions(-) diff --git a/content/Top-embeds-in-LRS.md b/content/Top-embeds-in-LRS.md index d560aaf7f..f1ea2bbe4 100644 --- a/content/Top-embeds-in-LRS.md +++ b/content/Top-embeds-in-LRS.md @@ -3,7 +3,7 @@ title: An embedding of the category of topological spaces in the category of loc description: Describes a functor which makes the category of topological spaces a coreflective and "almost reflective" subcategory of the category of locally ringed spaces. From the properties of this embedding, we can rule out several properties for the category of locally ringed spaces, using the corresponding failures of these properties for the category of topological spaces. --- -## An embedding of the category of topological spaces in the category of locally ringed spaces +# An embedding of the category of topological spaces in the category of locally ringed spaces For much of this development, we will be dealing with the case of $\LRS_k$ where $k$ is a field. We begin by describing $\Top$ as a reflective subcategory of $\LRS_k$. diff --git a/content/cocongruences_of_groups.md b/content/cocongruences_of_groups.md index b17046b15..5bf9f650f 100644 --- a/content/cocongruences_of_groups.md +++ b/content/cocongruences_of_groups.md @@ -3,7 +3,7 @@ title: Cocongruences on groups are effective description: This result will be proved more generally for categories in which pushouts and monomorphisms interact in a suitable way. --- -## Cocongruences on groups are effective +# Cocongruences on groups are effective Our goal is to prove that every cocongruence in $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way. diff --git a/content/cogenerators_in_product_categories.md b/content/cogenerators_in_product_categories.md index 307dfd35a..84551062d 100644 --- a/content/cogenerators_in_product_categories.md +++ b/content/cogenerators_in_product_categories.md @@ -3,7 +3,7 @@ title: Cogenerators in product categories description: How to construct a cogenerator in a product category --- -## Cogenerators in product categories +# Cogenerators in product categories ::: Lemma For a family of categories $(\C_i)_{i \in I}$, each having a cogenerator $Q_i$ which is weakly terminal, the object $(Q_i)_{i \in I}$ is a cogenerator in the product category $\prod_{i \in I} \C_i$. diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md index 3e2bf1ce7..c888aa060 100644 --- a/content/comphaus_copresentable.md +++ b/content/comphaus_copresentable.md @@ -3,7 +3,7 @@ title: Local ℵ₁-copresentability of the category of compact Hausdorff spaces description: We gather several relevant results about the category of compact Hausdorff spaces, and provide accessible proofs of these facts leading up to a proof that it is locally ℵ₁-copresentable. --- -## Local ℵ₁-copresentability of the category of compact Hausdorff spaces +# Local ℵ₁-copresentability of the category of compact Hausdorff spaces Our purpose here is to gather several relevant results about $\CompHaus$, the [category of compact Hausdorff spaces](/category/CompHaus), and provide accessible (sic) proofs of these facts leading up to a proof that it is locally $\aleph_1$-copresentable. @@ -101,7 +101,7 @@ The first automatically preserves $\aleph_1$-filtered colimits (and in fact all Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\T \to \Set$ preserving countable products, where $\T$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\T$ is essentially small. We thus reproduce a result from [Isb82](#references) which also provides a nice description of a small set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in [MR17](#references) refines this by providing a nice axiomatization of the relations of that theory. ::: -### References +## References [Dus69]  J. Duskin, _Variations on Beck’s tripleability criterion_. Reports of the Midwest Category Seminar III, pages 74–129. Springer Berlin Heidelberg, 1969 diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md index 278027e95..96357a423 100644 --- a/content/congruences_in_rel.md +++ b/content/congruences_in_rel.md @@ -3,7 +3,7 @@ title: A classification of congruences in the category of sets and relations description: The classification will prove in particular that the category of sets and relations has quotients of congruences and that congruences are effective. --- -## A classification of congruences in the category of sets and relations +# A classification of congruences in the category of sets and relations We will give a classification of congruences in $\Rel$, the [category of sets and relations](/category/Rel). This classification will prove in particular that $\Rel$ has quotients of congruences and that congruences are effective. diff --git a/content/constant_morphisms.md b/content/constant_morphisms.md index 25b185457..e095263ed 100644 --- a/content/constant_morphisms.md +++ b/content/constant_morphisms.md @@ -3,7 +3,7 @@ title: Results on constant morphisms description: We prove some results that help determine whether a morphism in a category is constant. --- -## Results on constant morphisms +# Results on constant morphisms ::: Lemma 1 A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map in the usual sense. diff --git a/content/contribute.md b/content/contribute.md index 8dd0b74ee..9e7745e7b 100644 --- a/content/contribute.md +++ b/content/contribute.md @@ -3,7 +3,7 @@ title: How to contribute to CatDat description: CatDat welcomes contributions from the community, including filling in missing information or discovering new combinations of properties --- -## How to contribute +# How to contribute _CatDat_ is developed in an open-source [GitHub repository](https://github.com/ScriptRaccoon/catdat) by [Martin Brandenburg](https://ncatlab.org/nlab/show/Martin+Brandenburg). It welcomes contributions from the community, including filling in missing information or discovering new combinations of properties. @@ -11,16 +11,16 @@ _CatDat_ is developed in an open-source [GitHub repository](https://github.com/S There are three ways to contribute: -### Option 1: Use the Suggestion Form +## Option 1: Use the Suggestion Form On most pages of CatDat, you will find a suggestion form at the bottom. Use it to contribute new data, report an issue, or make a suggestion. After submission, the form automatically creates a GitHub issue, which we then review and try to resolve and implement. This option does not require any knowledge of GitHub or coding, making it accessible to everyone. It also does not require following any guidelines for adding new data. -### Option 2: Create an Issue +## Option 2: Create an Issue Create an [issue](https://github.com/ScriptRaccoon/CatDat/issues/new) on GitHub. You will need a GitHub account. -### Option 3: Create a Pull Request +## Option 3: Create a Pull Request Create a [pull request](https://github.com/ScriptRaccoon/CatDat/pulls) on GitHub. You will need a GitHub account and some coding knowledge. Make sure to follow the [contribution guidelines](https://github.com/ScriptRaccoon/CatDat/blob/main/CONTRIBUTING.md). diff --git a/content/coslice-effective-congruences.md b/content/coslice-effective-congruences.md index 888e2f28e..40cb22ffd 100644 --- a/content/coslice-effective-congruences.md +++ b/content/coslice-effective-congruences.md @@ -3,7 +3,7 @@ title: Inheritance of effective congruences in coslice categories description: An extensive category has effective congruences when some of its coslice categories has effective congruences. --- -## Inheritance of effective congruences in coslice categories +# Inheritance of effective congruences in coslice categories ::: Lemma Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice category $A \backslash \C$ has effective congruences, then so does $\C$. diff --git a/content/dual-properties.md b/content/dual-properties.md index b6dfddb7b..7842047b7 100644 --- a/content/dual-properties.md +++ b/content/dual-properties.md @@ -3,9 +3,9 @@ title: Dual properties description: A short explanation of what we mean by dual properties in CatDat. --- -## Dual properties +# Dual properties -### Categories +## Categories Given a property $P$ of categories, its dual property $P^{\op}$ is defined as follows: a category $\C$ satisfies $P^{\op}$ if and only if its dual category $\C^{\op}$ satisfies $P$. @@ -13,7 +13,7 @@ For example, since a category has an [initial object](/category-property/initial Notice that $(P^{\op})^{\op} = P$, and that $\C$ satisfies $P$ if and only if $\C^{\op}$ satisfies $P^{\op}$. -### Functors +## Functors Given a property $P$ of functors, its dual property $P^{\op}$ is defined as follows: a functor $F : \C \to \D$ satisfies $P^{\op}$ if and only if its dual functor $F^{\op} : \C^{\op} \to \D^{\op}$ satisfies $P$. Notice that taking the dual does not reverse the direction of the functor. @@ -21,7 +21,7 @@ For example, since a functor is [essentially injective](/functor-property/essent Again, notice that $(P^{\op})^{\op} = P$, and that $F : \C \to \D$ satisfies $P$ if and only if $F^{\op} : \C^{\op} \to \D^{\op}$ satisfies $P^{\op}$. -### Morphisms +## Morphisms Given a property $P$ of morphisms, its dual property $P^{\op}$ is defined as follows: a morphism $f : X \to Y$ in a category $\C$ satisfies $P^{\op}$ if and only if its dual morphism $f^{\op} : Y \to X$ in the dual category $\C^{\op}$ satisfies $P$. @@ -29,7 +29,7 @@ For example, the property [monomorphism](/morphism-property/monomorphism) is dua Notice that $(P^{\op})^{\op} = P$, and that $f$ satisfies $P$ if and only if $f^{\op}$ satisfies $P^{\op}$. -### Symmetric Monoidal Categories +## Symmetric Monoidal Categories The dual of a symmetric monoidal category $(\C,\otimes,1)$ is defined by $(\C^{\op},\otimes,1)$ (and the obvious coherence isomorphisms). Given a property $P$ of symmetric monoidal categories, its dual property $P^{\op}$ is defined as follows: a symmetric monoidal category satisfies $P^{\op}$ if and only if its dual satisfies $P$. diff --git a/content/effective-congruence-quotients.md b/content/effective-congruence-quotients.md index 831717471..897a6dfcc 100644 --- a/content/effective-congruence-quotients.md +++ b/content/effective-congruence-quotients.md @@ -3,7 +3,7 @@ title: Quotients of effective congruences are strict quotients description: Quotients by effective congruences are characterized via a pullback --- -## Quotients of effective congruences are strict quotients +# Quotients of effective congruences are strict quotients ::: Lemma Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square diff --git a/content/foundations.md b/content/foundations.md index 9eda43438..c799b3eed 100644 --- a/content/foundations.md +++ b/content/foundations.md @@ -3,11 +3,11 @@ title: Foundations description: How to make sense of categories in set theory --- -## Foundations +# Foundations In _CatDat_, we work with the following convenient set-theoretic foundation for category theory. -### Sets, collections, and hypercollections +## Sets, collections, and hypercollections We work with [ZFC](https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory) and two [Grothendieck universes](https://en.wikipedia.org/wiki/Grothendieck_universe), which we denote by $$\mathrm{Set} \in \mathrm{Set}^+.$$ @@ -35,7 +35,7 @@ A family $(X_i)_{i \in I}$ of collections is called _small_ when its index colle A collection is called _countable_ if it admits a surjective map from $\IN$. In particular, every finite collection is countable. -### Categories +## Categories A _category_ $\C$ consists of a pair of collections $O, M$, whose elements are called _objects_ and _morphisms_, respectively, together with maps @@ -62,7 +62,7 @@ For example, the category of sets $\Set$ has $\Ob(\Set) = \mathrm{Set}$, the col Collections are the objects of a hypercategory $\Set^+$. -### Functors +## Functors A _functor_ $F : \C \to \D$ between two categories (or small categories, or hypercategories) is defined as usual; it consists of maps $$\Ob(F) : \Ob(\C) \to \Ob(\D),$$ @@ -77,7 +77,7 @@ If $\C, \D$ are categories, we can construct the functor category $[\C, \D]$ as It is better to state explicitly when the assumption of being locally small is needed. -### Representable Functors +## Representable Functors If $\C$ is any category and $A \in \C$, we have the Hom-functor @@ -89,7 +89,7 @@ Adjunctions are defined as usual via natural isomorphisms $$\Hom(F(A),B) \cong \Hom(A,G(B))$$ of functors valued in $\Set^+$. No local smallness assumption is required. Equivalently, they can be defined via morphisms of functors $\id \to G \circ F$ and $F \circ G \to \id$ satisfying the triangle identities. -### Limits and Colimits +## Limits and Colimits Let $\C$ be a category. If $D : \I \to \C$ is a functor (in this context called a _diagram_), a _cone_ over $D$ is an object $X \in \C$ equipped with morphisms $p_i : X \to D(i)$ for all $i \in \I$ such that for every morphism $i \to j$ the evident triangle commutes. Cones form a category, and a terminal object in this category is called a _limit_ of $D$. The dual notion is a _colimit_. @@ -97,10 +97,10 @@ Unless stated otherwise, we consider only small diagrams and hence small limits There are special types of limits, such as equalizers, products, and cofiltered limits, and their duals, such as coequalizers, coproducts, and filtered colimits. By convention, products and coproducts are indexed by a set, not a collection (unless stated otherwise). Filtered colimits are indexed by a small filtered category (unless stated otherwise). -### Well-powered categories +## Well-powered categories If $A$ is an object of a category, the collection of all monomorphisms $B \to A$ need not be a set. If, for every $A$, there exists a small family of such monomorphisms such that every monomorphism $B \to A$ is isomorphic over $A$ to one in the family, then the category is called _well-powered_. The dual notion of being _well-copowered_ is defined using epimorphisms $A \to B$. Every small category is well-powered, but there are many well-powered categories that are not small and not even equivalent to a small category. -### Conclusion +## Conclusion There is much more to say about set-theoretic foundations for category theory (in fact, many papers have been written on the subject, and the approach developed above is just _one_ of [many](https://xkcd.com/927/) approaches), but this suffices for the purposes of _CatDat_. diff --git a/content/functors_on_discrete_categories.md b/content/functors_on_discrete_categories.md index 72b80ccb6..5514064eb 100644 --- a/content/functors_on_discrete_categories.md +++ b/content/functors_on_discrete_categories.md @@ -3,7 +3,7 @@ title: Functors on discrete categories description: We describe which functors on discrete categories are continuous or cocontinuous. --- -## Functors on discrete categories +# Functors on discrete categories Let $\S$ be a discrete category. Thus, a functor $F : \S \to \C$ is the same as a family of objects $F(s) \in \C$ indexed by the objects $s \in \S$. Here, we want to determine under which conditions $F$ is continuous (or cocontinuous). The case $\S = \varnothing$ is rather boring, which is why we assume from now on that $\S \neq \varnothing$, i.e. that $\S$ is inhabited. diff --git a/content/generator_construction.md b/content/generator_construction.md index eceb44a04..d0bf28a4d 100644 --- a/content/generator_construction.md +++ b/content/generator_construction.md @@ -3,7 +3,7 @@ title: Construction of generators description: How to construct a generator from a generating set --- -## Construction of generators +# Construction of generators ::: Lemma In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating set, then $U$ is an extremal generator. diff --git a/content/inclusion-functors.md b/content/inclusion-functors.md index 82a51647e..122dbf62c 100644 --- a/content/inclusion-functors.md +++ b/content/inclusion-functors.md @@ -3,7 +3,7 @@ title: Inclusion functors description: We gather results about inclusion functors --- -## Inclusion functors +# Inclusion functors ::: Lemma 1 Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous. diff --git a/content/missing_cogenerating_sets.md b/content/missing_cogenerating_sets.md index bf71c2b38..9a97f67ce 100644 --- a/content/missing_cogenerating_sets.md +++ b/content/missing_cogenerating_sets.md @@ -3,7 +3,7 @@ title: Missing cogenerating sets description: A generalization of the proof that the category of commutative rings has no cogenerating set. --- -## Missing cogenerating sets +# Missing cogenerating sets ::: Lemma Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md index 6e1915950..da80c70a8 100644 --- a/content/missing_cogenerator.md +++ b/content/missing_cogenerator.md @@ -3,7 +3,7 @@ title: Missing cogenerator description: A generalization of the proof that the category of groups has no cogenerator. --- -## Missing cogenerator +# Missing cogenerator ::: Lemma diff --git a/content/monic_sequential_colimits.md b/content/monic_sequential_colimits.md index aed0b8ccc..a5b773285 100644 --- a/content/monic_sequential_colimits.md +++ b/content/monic_sequential_colimits.md @@ -3,7 +3,7 @@ title: The colimit of a sequence of monomorphisms description: We find conditions under which a countably extensive category has colimits of sequences of monomorphisms. --- -## The colimit of a sequence of monomorphisms +# The colimit of a sequence of monomorphisms ::: Lemma 1 Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms. diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md index 54feb572e..a601b9bde 100644 --- a/content/natural_numbers_objects.md +++ b/content/natural_numbers_objects.md @@ -3,7 +3,7 @@ title: Natural numbers objects description: We prove some results on natural numbers objects. --- -## Natural numbers objects +# Natural numbers objects The definition of a [natural numbers object](/category-property/natural_numbers_object) a priori only allows for recursively defined morphisms in which the next value $\Phi(s(n))$ depends only on the previous value $\Phi(n)$. In many cases, however, we would also like to use $n$ itself to define $\Phi(s(n))$. This can be done in categories with finite products: diff --git a/content/preadditive_structure_unique.md b/content/preadditive_structure_unique.md index c478d9b9e..3587e719c 100644 --- a/content/preadditive_structure_unique.md +++ b/content/preadditive_structure_unique.md @@ -3,7 +3,7 @@ title: Uniqueness of preadditive structures description: In the presence of finite products, a preadditive structure on a given category is uniquely determined. --- -## Uniqueness of preadditive structures +# Uniqueness of preadditive structures ::: Lemma Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products and finite coproducts. Then for all objects $X,Y$ the canonical morphism diff --git a/content/pushouts-of-monos-via-congruence-quotients.md b/content/pushouts-of-monos-via-congruence-quotients.md index ac88890b9..8b31f08a9 100644 --- a/content/pushouts-of-monos-via-congruence-quotients.md +++ b/content/pushouts-of-monos-via-congruence-quotients.md @@ -3,7 +3,7 @@ title: Construction of a pushout of monomorphisms as a quotient of a congruence description: An extensive category with quotients of congruences has pushouts of monomorphisms. --- -## Construction of a pushout of monomorphisms as a quotient of a congruence +# Construction of a pushout of monomorphisms as a quotient of a congruence ::: Lemma Let $\C$ be an extensive category with quotients of congruences. Then $\C$ has pushouts of monomorphisms. diff --git a/content/relationships-epis-monos.md b/content/relationships-epis-monos.md index 20d296fcd..06ae813ad 100644 --- a/content/relationships-epis-monos.md +++ b/content/relationships-epis-monos.md @@ -3,11 +3,11 @@ title: Relationships between epimorphisms and monomorphisms description: A graphical overview of the relationships between the various types of epimorphisms and monomorphisms --- -## Relationships between epimorphisms and monomorphisms +# Relationships between epimorphisms and monomorphisms There are several [properties of morphisms](/morphism-properties), including various types of epimorphisms and monomorphisms. The [implications](/morphism-implications) establish various relationships between these types. Here we present a graphical overview of these relationships. -### The various types of epimorphisms +## The various types of epimorphisms In the diagram, an arrow $X \Longrightarrow Y$ means that every morphism with property $X$ also has property $Y$. If it is labelled with a category property $P$, the implication does not hold in general, but it holds in categories satisfying $P$. For example, in a category with pullbacks, every strict epimorphism is effective. @@ -25,7 +25,7 @@ In the diagram, an arrow $X \Longrightarrow Y$ means that every morphism with pr Fun fact: This describes a category in itself: We define the composition of $P : X \Rightarrow Y$ and $Q : Y \Rightarrow Z$ as $P \wedge Q : X \Rightarrow Z$. -### The various types of monomorphisms +## The various types of monomorphisms This diagram is just the dual of the previous diagram. The same notation applies. diff --git a/content/resources.md b/content/resources.md index 00cf48466..249a953fc 100644 --- a/content/resources.md +++ b/content/resources.md @@ -3,7 +3,7 @@ title: Resources on category theory description: This is an (incomplete) list of resources on category theory. --- -## Resources on category theory +# Resources on category theory This is an (incomplete) list of resources on category theory. diff --git a/content/sifted-colimits-in-groupoids.md b/content/sifted-colimits-in-groupoids.md index 8c58850d3..202e4d171 100644 --- a/content/sifted-colimits-in-groupoids.md +++ b/content/sifted-colimits-in-groupoids.md @@ -3,7 +3,7 @@ title: Sifted colimits in groupoids description: A description of sifted colimits in groupoids, yielding a proof that every essentially small groupoid is a generalized variety. --- -## Sifted colimits in groupoids +# Sifted colimits in groupoids While the combination of [this result](/category-implication/groupoid_consequence) and [this result](/category-implication/sifted_colimits_criterion) already implies that groupoids have sifted colimits, we can make these colimits more explicit and also prove their existence without using any non-trivial theorem. We also do this in a more general setting. diff --git a/content/special_sequential_colimits.md b/content/special_sequential_colimits.md index a33338ce1..80daa4467 100644 --- a/content/special_sequential_colimits.md +++ b/content/special_sequential_colimits.md @@ -3,7 +3,7 @@ title: Finite structures usually have no sequential colimits description: A generalization of the proof that the category of finite groups has no filtered colimits. --- -## Finite structures usually have no sequential colimits +# Finite structures usually have no sequential colimits ::: Lemma Let $\C$ be a category with finite powers, including a terminal object $1$. Let $a : 1 \to X$ be a morphism. Assume that the sequence of morphisms $(X^n,a) : X^n \to X^{n+1}$ for $n \geq 0$ admits a colimit $(i_n : X^n \to C)$. Then for every $m \geq 0$ there is a split epimorphism $C \to X^m$. In particular, if $U : \C \to \Set$ is a functor preserving finite powers and $\card(U(X)) \geq 2$, then $U(C)$ is infinite. diff --git a/content/subcategories.md b/content/subcategories.md index 5385297ad..a7aac4051 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -3,7 +3,7 @@ title: Results on subcategories description: We prove that several properties of categories descend to suitable subcategories. --- -## Results on subcategories +# Results on subcategories This page collects several useful results of the following form: if $U : \C \to \D$ is a faithful functor (perhaps even fully faithful, or satisfying additional assumptions) and $\D$ has a certain property, then $\C$ has this property as well. diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md index e101ee9fd..da0ec1299 100644 --- a/content/thin_algebraic_categories.md +++ b/content/thin_algebraic_categories.md @@ -3,7 +3,7 @@ title: Algebraic categories are "never" thin description: A proof that the only thin algebraic categories are the terminal and the interval category. --- -## Algebraic categories are "never" thin +# Algebraic categories are "never" thin - +
diff --git a/src/components/IndistinguishableStructures.svelte b/src/components/IndistinguishableStructures.svelte index efb91c325..8815a205f 100644 --- a/src/components/IndistinguishableStructures.svelte +++ b/src/components/IndistinguishableStructures.svelte @@ -14,7 +14,7 @@ {#if structures.length}
-

Indistinguishable {PLURALS[type]}

+

Indistinguishable {PLURALS[type]}

These {PLURALS[type]} in the database currently have exactly the same properties diff --git a/src/components/Popup.svelte b/src/components/Popup.svelte index 4dcbebdda..c264bb8e8 100644 --- a/src/components/Popup.svelte +++ b/src/components/Popup.svelte @@ -75,7 +75,7 @@ an issue when clicking two proofs in a row. So it's a

then. >
-

{popup_state.heading}

+

{popup_state.heading}

+
+ + 
{normalized_code}
+
+ + diff --git a/src/routes/app.css b/src/routes/app.css index 3bc953c5e..31b32227a 100644 --- a/src/routes/app.css +++ b/src/routes/app.css @@ -107,7 +107,6 @@ h2 { h3 { font-size: 1.125rem; - margin-block: 1.5rem 0.5rem; } /* various elements */ diff --git a/src/routes/download/+page.svelte b/src/routes/download/+page.svelte index dce67390e..0acb4813f 100644 --- a/src/routes/download/+page.svelte +++ b/src/routes/download/+page.svelte @@ -1,4 +1,5 @@