From f78525698e4480d37902b9abf7116cce1892d282 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 8 Apr 2026 15:14:35 +0200 Subject: [PATCH 1/3] support for lemmas --- database/data/000_setup/001_clear.sql | 2 ++ database/migrations/016_lemma-table.sql | 6 ++++++ src/lib/commons/types.ts | 6 ++++++ src/routes/lemma/[id]/+page.server.ts | 21 +++++++++++++++++++++ src/routes/lemma/[id]/+page.svelte | 16 ++++++++++++++++ 5 files changed, 51 insertions(+) create mode 100644 database/migrations/016_lemma-table.sql create mode 100644 src/routes/lemma/[id]/+page.server.ts create mode 100644 src/routes/lemma/[id]/+page.svelte diff --git a/database/data/000_setup/001_clear.sql b/database/data/000_setup/001_clear.sql index 6f8a85c8..7c06f25d 100644 --- a/database/data/000_setup/001_clear.sql +++ b/database/data/000_setup/001_clear.sql @@ -1,5 +1,7 @@ PRAGMA foreign_keys = OFF; +DELETE FROM lemmas; + DELETE FROM implication_assumptions; DELETE FROM implication_conclusions; DELETE FROM implications; diff --git a/database/migrations/016_lemma-table.sql b/database/migrations/016_lemma-table.sql new file mode 100644 index 00000000..03a02797 --- /dev/null +++ b/database/migrations/016_lemma-table.sql @@ -0,0 +1,6 @@ +CREATE TABLE lemmas ( + id TEXT PRIMARY KEY, + title TEXT NOT NULL UNIQUE, + claim TEXT NOT NULL, + proof TEXT NOT NULL +); \ No newline at end of file diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 16603b80..ad73b918 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -155,3 +155,9 @@ export type FunctorPropertyAssignment = Replace< FunctorPropertyAssignmentDB, { is_deduced: boolean } > + +export type Lemma = { + title: string + claim: string + proof: string +} diff --git a/src/routes/lemma/[id]/+page.server.ts b/src/routes/lemma/[id]/+page.server.ts new file mode 100644 index 00000000..f591bc06 --- /dev/null +++ b/src/routes/lemma/[id]/+page.server.ts @@ -0,0 +1,21 @@ +import type { Lemma } from '$lib/commons/types' +import { query } from '$lib/server/db' +import { render_nested_formulas } from '$lib/server/rendering' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' + +export const load = async (event) => { + const id = event.params.id + + const { rows: lemmas, err } = await query(sql` + SELECT title, claim, proof FROM lemmas WHERE id = ${id} + `) + + if (err) error(500, 'Could not load lemma') + + if (!lemmas.length) error(404, 'Lemma not found') + + const lemma = lemmas[0] + + return render_nested_formulas({ lemma }) +} diff --git a/src/routes/lemma/[id]/+page.svelte b/src/routes/lemma/[id]/+page.svelte new file mode 100644 index 00000000..3519a6fd --- /dev/null +++ b/src/routes/lemma/[id]/+page.svelte @@ -0,0 +1,16 @@ + + + + +

{data.lemma.title}

+ +

Claim

+ +{@html data.lemma.claim} + +

Proof

+ +{@html data.lemma.proof} From 332db6eeaffae28f595869e023df0c7f41eb5d3e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 8 Apr 2026 15:14:51 +0200 Subject: [PATCH 2/3] add lemma about thin algebraic categories --- database/data/004_property-assignments/N_oo.sql | 6 ++++++ .../walking_commutative_square.sql | 2 +- .../walking_composable_pair.sql | 2 +- database/data/010_lemmas/000_lemmas.sql | 12 ++++++++++++ 4 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 database/data/010_lemmas/000_lemmas.sql diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql index b967fa44..8ebed5ee 100644 --- a/database/data/004_property-assignments/N_oo.sql +++ b/database/data/004_property-assignments/N_oo.sql @@ -29,6 +29,12 @@ VALUES TRUE, 'This is because the natural numbers with $\infty$ with respect to $<$ are well-founded.' ), +( + 'N_oo', + 'finitary algebraic', + FALSE, + 'This follows from this lemma.' +), ( 'N_oo', 'locally strongly finitely presentable', diff --git a/database/data/004_property-assignments/walking_commutative_square.sql b/database/data/004_property-assignments/walking_commutative_square.sql index ab4aed04..1016c173 100644 --- a/database/data/004_property-assignments/walking_commutative_square.sql +++ b/database/data/004_property-assignments/walking_commutative_square.sql @@ -57,5 +57,5 @@ VALUES 'walking_commutative_square', 'finitary algebraic', FALSE, - 'More generally, let $\mathcal{C}$ be a thin finitary algebraic category. Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \to A$ for some set $X$. But since $\mathcal{C}$ is left cancellative, every regular epimorphism must be an isomorphism. 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 $\mathcal{C}$ is thin). This shows that $\mathcal{C}$ must have at most $2$ objects up to isomorphism. In fact, either $\mathcal{C}$ is trivial or equivalent to the interval category $\{0 \to 1\}$ (which is finitary algebraic).' + 'This follows from this lemma.' ); diff --git a/database/data/004_property-assignments/walking_composable_pair.sql b/database/data/004_property-assignments/walking_composable_pair.sql index e89d1ef8..155825be 100644 --- a/database/data/004_property-assignments/walking_composable_pair.sql +++ b/database/data/004_property-assignments/walking_composable_pair.sql @@ -33,7 +33,7 @@ VALUES 'walking_composable_pair', 'finitary algebraic', FALSE, - 'More generally, let $\mathcal{C}$ be a thin finitary algebraic category. Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \to A$ for some set $X$. But since $\mathcal{C}$ is left cancellative, every regular epimorphism must be an isomorphism. 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 $\mathcal{C}$ is thin). This shows that $\mathcal{C}$ must have at most $2$ objects up to isomorphism. In fact, either $\mathcal{C}$ is trivial or equivalent to the interval category $\{0 \to 1\}$ (which is finitary algebraic).' + 'This follows from this lemma.' ), ( 'walking_composable_pair', diff --git a/database/data/010_lemmas/000_lemmas.sql b/database/data/010_lemmas/000_lemmas.sql new file mode 100644 index 00000000..83dab6c1 --- /dev/null +++ b/database/data/010_lemmas/000_lemmas.sql @@ -0,0 +1,12 @@ +INSERT INTO lemmas ( + id, + title, + claim, + proof +) VALUES +( + 'thin_algebraic_categories', + 'Algebraic categories are "never" thin', + 'Let $\mathcal{C}$ be a thin and finitary algebraic category. Then $\mathcal{C} \simeq 1$ or $\mathcal{C} \simeq \{0 < 1\}$.', + 'Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\mathcal{C}$ is thin, every regular epimorphism must be an isomorphism. 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 $\mathcal{C}$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\mathcal{C}$ is trivial. If not, then $\mathcal{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 $\mathcal{C}$ is thin, we conclude $\mathcal{C} \simeq \{0 \to 1\}$.' +); \ No newline at end of file From a26757f3ca8fe16e6120ad74bc80f2619a9cdfb9 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 8 Apr 2026 21:47:35 +0200 Subject: [PATCH 3/3] add lemma about Hilbert's Hotel --- .vscode/settings.json | 3 ++- database/data/004_property-assignments/Ab_fg.sql | 4 ++-- database/data/004_property-assignments/FinAb.sql | 2 +- database/data/004_property-assignments/FinSet.sql | 4 ++-- database/data/010_lemmas/000_lemmas.sql | 6 ++++++ 5 files changed, 13 insertions(+), 6 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 107a7c79..f852916e 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -15,7 +15,8 @@ "infty", "chartjs", "Prost", - "SetxSet" + "SetxSet", + "hilberts" ], "cSpell.words": [ "abelian", diff --git a/database/data/004_property-assignments/Ab_fg.sql b/database/data/004_property-assignments/Ab_fg.sql index 6c415059..dbbb9040 100644 --- a/database/data/004_property-assignments/Ab_fg.sql +++ b/database/data/004_property-assignments/Ab_fg.sql @@ -51,13 +51,13 @@ VALUES 'Ab_fg', 'countable powers', FALSE, - 'Assume that the power $P := \mathbb{Z}^{\mathbb{N}} = \prod_{n \geq 0} \mathbb{Z}$ exists in this category. Since products are associative and finite products exist, we have $P \cong \mathbb{Z} \times P$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $P_{\mathbb{Q}} \cong \mathbb{Q} \times P_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $P_{\mathbb{Q}}$ (i.e. the rank of $P$) would satisfy $d = 1+d$.' + 'If countable powers exist, then by Hilbert''s Hotel there is some object $P$ with $P \cong \mathbb{Z} \times P$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $P_{\mathbb{Q}} \cong \mathbb{Q} \times P_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $P_{\mathbb{Q}}$ (i.e. the rank of $P$) would satisfy $d = 1+d$.' ), ( 'Ab_fg', 'countable copowers', FALSE, - 'Assume that the copower $C := \mathbb{N} \otimes \mathbb{Z} = \coprod_{n \geq 0} \mathbb{Z}$ exists in this category. Since coproducts are associative and finite coproducts exist, we have $C \cong \mathbb{Z} \oplus C$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $C_{\mathbb{Q}} \cong \mathbb{Q} \oplus C_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $C_{\mathbb{Q}}$ (i.e. the rank of $C$) would satisfy $d = 1+d$.' + 'If countable powers exist, then by Hilbert''s Hotel there is some object $P$ with $P \cong \mathbb{Z} \oplus P$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $C_{\mathbb{Q}} \cong \mathbb{Q} \oplus C_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $C_{\mathbb{Q}}$ (i.e. the rank of $C$) would satisfy $d = 1+d$.' ), ( 'Ab_fg', diff --git a/database/data/004_property-assignments/FinAb.sql b/database/data/004_property-assignments/FinAb.sql index 720659df..ff7575ef 100644 --- a/database/data/004_property-assignments/FinAb.sql +++ b/database/data/004_property-assignments/FinAb.sql @@ -51,7 +51,7 @@ VALUES 'FinAb', 'countable powers', FALSE, - 'Assume that the power $P := (\mathbb{Z}/2)^{\mathbb{N}}$ exists. Since products are associative and finite products exist, we conclude $P \cong \mathbb{Z}/2 \times P$. If $P$ has $n$ elements, this means $n = 2n$, i.e. $n = 0$, a contradiction.' + 'If countable powers exist, then by Hilbert''s Hotel there is some object $P$ with $P \cong \mathbb{Z}/2 \times P$. If $P$ has $n$ elements, this means $n = 2n$, i.e. $n = 0$, a contradiction.' ), ( 'FinAb', diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index 24d84a0b..45236ce2 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/database/data/004_property-assignments/FinSet.sql @@ -51,13 +51,13 @@ VALUES 'FinSet', 'countable copowers', FALSE, - 'Assume that the copower $C := \mathbb{N} \otimes 1$ exists. Since coproducts are associative and finite coproducts exist, we get $C \cong 1 \sqcup C$. It $C$ has $m \in \mathbb{N}$ elements, this implies $m = 1 + m$, which is a contradiction.' + 'If countable copowers exist, then by Hilbert''s Hotel there is some object $C$ with $C \cong 1 \sqcup C$. If $C$ has $m \in \mathbb{N}$ elements, this implies the contradiction $m = 1 + m$.' ), ( 'FinSet', 'countable powers', FALSE, - 'Assume that the power $P := \{0,1\}^{\mathbb{N}}$ exists. Since products are associative and finite products exists, we get $P \cong \{0,1\} \times P$. If $P$ has $m \in \mathbb{N}$ elements, this implies $m = 2m$ and hence $m = 0$, i.e. $P = \varnothing$. But there is a diagonal morphism $\{0,1\} \to P$, making $P = \varnothing$ impossible.' + 'If countable powers exist, then by Hilbert''s Hotel there is an object $P$ with $P \cong \{0,1\} \times P$ and a morphism $\{0,1\} \to P$. If $P$ has $m \in \mathbb{N}$ elements, this implies $m = 2m$ and hence $m = 0$, i.e. $P = \varnothing$. But then there cannot be a map $\{0,1\} \to P$.' ), ( 'FinSet', diff --git a/database/data/010_lemmas/000_lemmas.sql b/database/data/010_lemmas/000_lemmas.sql index 83dab6c1..cbdcf1e7 100644 --- a/database/data/010_lemmas/000_lemmas.sql +++ b/database/data/010_lemmas/000_lemmas.sql @@ -9,4 +9,10 @@ INSERT INTO lemmas ( 'Algebraic categories are "never" thin', 'Let $\mathcal{C}$ be a thin and finitary algebraic category. Then $\mathcal{C} \simeq 1$ or $\mathcal{C} \simeq \{0 < 1\}$.', 'Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\mathcal{C}$ is thin, every regular epimorphism must be an isomorphism. 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 $\mathcal{C}$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\mathcal{C}$ is trivial. If not, then $\mathcal{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 $\mathcal{C}$ is thin, we conclude $\mathcal{C} \simeq \{0 \to 1\}$.' +), +( + 'hilberts_hotel', + 'Hilbert''s Hotel', + 'Let $\mathcal{C}$ be a category with countable powers. Then for every object $X \in \mathcal{C}$ there is an object $P \in \mathcal{C}$ with $P \cong X \times P$ and which has a morphism $X \to P$.', + 'Take $P := X^{\mathbb{N}}$. Since $\mathbb{N} \cong 1 + \mathbb{N}$ as sets, we have $P \cong X \times P$. The diagonal provides a morphism $X \to P$.' ); \ No newline at end of file