diff --git a/content/aleph1-filtered-colimits-in-deloopings.md b/content/aleph1-filtered-colimits-in-deloopings.md index 8d9d8174..d9ad3311 100644 --- a/content/aleph1-filtered-colimits-in-deloopings.md +++ b/content/aleph1-filtered-colimits-in-deloopings.md @@ -3,7 +3,7 @@ title: ℵ₁-filtered colimits in deloopings description: We give a detailed proof that the delooping of the monoid of natural numbers, and likewise the delooping of the large monoid of ordinal numbers, has colimits indexed by ℵ₁-filtered categories. --- -# $\aleph_1$-filtered colimits in deloopings +## $\aleph_1$-filtered colimits in deloopings Every (possibly large) monoid $M$ induces a category $BM$ with just one object. We will show that this category has $\aleph_1$-filtered colimits in the cases $M = \IN$ and $M = \On$ (both respect to addition). diff --git a/content/inclusion-functors.md b/content/inclusion-functors.md index ed67b1b9..8cd2c071 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/sifted-colimits-in-groupoids.md b/content/sifted-colimits-in-groupoids.md index 49d54803..cc6c2530 100644 --- a/content/sifted-colimits-in-groupoids.md +++ b/content/sifted-colimits-in-groupoids.md @@ -5,7 +5,7 @@ description: A description of sifted colimits in groupoids, yielding a proof tha ## Sifted colimits in groupoids -While the combination of [this result](http://localhost:5173/category-implication/groupoid_consequence) and [this result](http://localhost:5173/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. +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. Let $D : \I \to \C$ be a [sifted](/category-property/sifted) diagram in a category and $i_0 \in \I$. We call $D$ _constant after_ $i_0$ when for all morphisms $i_0 \to i$ the morphism $D(i_0) \to D(i)$ is an isomorphism. Of course, in a groupoid, this is satisfied for every $i_0 \in \I$. If such an object $i_0$ exists, we call $D$ _eventually constant_. diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md index d707a87a..b57fb19c 100644 --- a/content/thin_algebraic_categories.md +++ b/content/thin_algebraic_categories.md @@ -5,9 +5,17 @@ description: A proof that the only thin algebraic categories are the terminal an ## Algebraic categories are "never" thin + + ::: Lemma Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq I$, where $I$ is the walking morphism. ::: _Proof._ Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$. $\square$ + +Remark: Another proof is possible by using the Lemma [here](/content/thin_extremal_generator). diff --git a/content/thin_extremal_generator.md b/content/thin_extremal_generator.md index efdc3f0b..f1a47f1c 100644 --- a/content/thin_extremal_generator.md +++ b/content/thin_extremal_generator.md @@ -3,7 +3,7 @@ title: Thin Category with an Extremal Generator description: A result restricting which thin categories can have an extremal generator --- -# Thin Category with an Extremal Generator +## Thin Category with an Extremal Generator ::: Lemma Suppose $G$ is an object of a thin category. Then $G$ is an extremal generator if and only if for every object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism. diff --git a/content/topos-with-generator.md b/content/topos-with-generator.md index 841b8244..475336ce 100644 --- a/content/topos-with-generator.md +++ b/content/topos-with-generator.md @@ -3,7 +3,7 @@ title: Topos with a Generator description: An elementary topos with a generator has at most two subterminal objects --- -# Topos with a Generator +## Topos with a Generator ::: Lemma Suppose a category is coregular, and it has disjoint finite coproducts, a terminal object, and a generator. Then every regular subterminal object (i.e. an object $X$ such that the unique morphism $X \to 1$ is a regular monomorphism) is either initial or terminal. diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index c70f0754..42c4b4d2 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -1,54 +1,69 @@ -import type { PropertyShort, StructureShort } from '$lib/commons/types' +import type { + ImplicationDB, + ImplicationDisplay, + PropertyShort, + StructureShort, + StructureType +} from '$lib/commons/types' import { db } from '$lib/server/db' +import { display_implication } from '../transforms' export function fetch_content_references(content_id: string) { - // TODO: make this more systematic - - const categories = db - .prepare<[string], StructureShort>( - `SELECT DISTINCT s.id, s.name + const structures = db + .prepare<[string], StructureShort & { type: StructureType }>( + `SELECT DISTINCT s.id, s.name, s.type FROM property_assignments pa INNER JOIN structures s ON s.id = pa.structure_id - WHERE pa.type = 'category' - AND pa.proof LIKE '%/content/' || ? || '%'` + WHERE pa.proof LIKE '%/content/' || ? || '%' + ORDER BY s.name` ) .all(content_id) - const functors = db - .prepare<[string], StructureShort>( - `SELECT DISTINCT s.id, s.name - FROM property_assignments pa - INNER JOIN structures s ON s.id = pa.structure_id - WHERE pa.type = 'functor' - AND pa.proof LIKE '%/content/' || ? || '%'` - ) - .all(content_id) + const structures_by_type: Partial> = {} - const morphisms = db - .prepare<[string], StructureShort>( - `SELECT DISTINCT s.id, s.name - FROM property_assignments pa - INNER JOIN structures s ON s.id = pa.structure_id - WHERE pa.type = 'morphism' - AND pa.proof LIKE '%/content/' || ? || '%'` - ) - .all(content_id) + for (const { type, ...structure } of structures) { + structures_by_type[type] ??= [] + structures_by_type[type].push(structure) + } - const category_properties = db - .prepare<[string], PropertyShort>( - `SELECT id, relation FROM properties - WHERE type = 'category' - AND description LIKE '%/content/' || ? || '%'` + const properties = db + .prepare<[string], PropertyShort & { type: StructureType }>( + `SELECT id, relation, type FROM properties + WHERE description LIKE '%/content/' || ? || '%' + ORDER BY lower(id)` ) .all(content_id) - const category_implications = db - .prepare<[string], { id: string }>( - `SELECT id FROM implications - WHERE type = 'category' - AND proof LIKE '%/content/' || ? || '%'` + const properties_by_type: Partial> = {} + + for (const { type, ...property } of properties) { + properties_by_type[type] ??= [] + properties_by_type[type].push(property) + } + + const implications = db + .prepare<[string], ImplicationDB & { type: StructureType }>( + `SELECT + id, + type, + is_equivalence, + is_deduced, + proof, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE proof LIKE '%/content/' || ? || '%' + ORDER BY lower(assumptions) || ' ' || lower(conclusions)` ) .all(content_id) - return { categories, category_properties, category_implications, functors, morphisms } + const implications_by_type: Partial> = {} + + for (const { type, ...rest } of implications) { + implications_by_type[type] ??= [] + implications_by_type[type].push(display_implication(rest)) + } + + return { structures_by_type, properties_by_type, implications_by_type } } diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte index d397ef18..7296ce4a 100644 --- a/src/routes/content/[id]/+page.svelte +++ b/src/routes/content/[id]/+page.svelte @@ -1,10 +1,19 @@ @@ -13,48 +22,31 @@ {@html data.html} - - -{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0 || data.functors.length > 0 || data.morphisms.length > 0} +{#if has_context}

Context

- {#if data.categories.length > 0} -

This page is referenced by the following categories.

- - - {/if} - - {#if data.category_properties.length > 0} -

- This page is referenced by the following properties of categories. -

- - - {/if} - - {#if data.category_implications.length > 0} -

This page is referenced by the following implications.

- -
    - {#each data.category_implications as { id }} -
  • - {id} -
    • - {/each} -
- {/if} + {#each STRUCTURE_TYPES as type} + {#if data.structures_by_type?.[type]?.length} +

This page is referenced by the following {PLURALS[type]}.

+ + {/if} - {#if data.functors.length > 0} -

This page is referenced by the following functors.

+ {#if data.properties_by_type?.[type]?.length} +

+ This page is referenced by the following properties of {PLURALS[type]}. +

- - {/if} + + {/if} - {#if data.morphisms.length > 0} -

This page is referenced by the following morphisms.

+ {#if data.implications_by_type?.[type]?.length} +

+ This page is referenced by the following {remove_underscores(type)} implications. +

- - {/if} + + {/if} + {/each} {/if}