Support lemmas

.vscode/settings.json

@@ -15,7 +15,8 @@
 		"infty",
 		"chartjs",
 		"Prost",
-		"SetxSet"
+		"SetxSet",
+		"hilberts"
 	],
 	"cSpell.words": [
 		"abelian",

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;

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 <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> 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 <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> 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',

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 <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> 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',

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 <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> 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 <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> 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',

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 <a href="/lemma/thin_algebraic_categories">this lemma</a>.'
+),
 (
 	'N_oo',
 	'locally strongly finitely presentable',

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 <a href="/category/walking_morphism">interval category</a> $\{0 \to 1\}$ (which <i>is</i> finitary algebraic).'
+	'This follows from <a href="/lemma/thin_algebraic_categories">this lemma</a>.'
 );

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 <a href="/category/walking_morphism">interval category</a> $\{0 \to 1\}$ (which <i>is</i> finitary algebraic).'
+	'This follows from <a href="/lemma/thin_algebraic_categories">this lemma</a>.'
 ),
 (
 	'walking_composable_pair',

database/data/010_lemmas/000_lemmas.sql

@@ -0,0 +1,18 @@
+INSERT INTO lemmas (
+    id,
+    title,
+    claim,
+    proof
+) VALUES 
+(
+    'thin_algebraic_categories',
+    'Algebraic categories are "never" thin',
+    'Let $\mathcal{C}$ be a <a href="/category-property/thin">thin</a> and <a href="/category-property/finitary_algebraic">finitary algebraic</a> 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$.'
+);

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
+);

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
+}

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<Lemma>(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 })
+}

src/routes/lemma/[id]/+page.svelte

@@ -0,0 +1,16 @@
+<script lang="ts">
+	import MetaData from '$components/MetaData.svelte'
+	let { data } = $props()
+</script>
+
+<MetaData title={data.lemma.title} />
+
+<h2>{data.lemma.title}</h2>
+
+<h3>Claim</h3>
+
+{@html data.lemma.claim}
+
+<h3>Proof</h3>
+
+{@html data.lemma.proof}