$\mu : A_1 \oplus \cdots \oplus A_n \to A_1 \times \cdots \times A_n$
is an isomorphism. Such a category is also called semi-additive, and it is automatically enriched over commutative monoids: the sum of $f,g : A \rightrightarrows B$ is defined as: -$A \xrightarrow{\Delta} A \times A \xrightarrow{f \times g} B \times B \xrightarrow{\mu^{-1}} B \oplus B \xrightarrow{\nabla} B$
', +$A \xrightarrow{(f,g)} B \times B \xrightarrow{\mu^{-1}} B \oplus B \xrightarrow{\nabla} B$
', 'https://ncatlab.org/nlab/show/biproduct', 'biproducts', TRUE diff --git a/database/data/003_properties/006_additional-structure.sql b/database/data/003_properties/006_additional-structure.sql index 76724a15..ace56231 100644 --- a/database/data/003_properties/006_additional-structure.sql +++ b/database/data/003_properties/006_additional-structure.sql @@ -34,7 +34,7 @@ VALUES ( 'additive', 'is', - 'A category is additive if it is preadditive and has finite products (equivalently, finite coproducts). Note that in the context of finite products, the preadditive structure is unique.', + 'A category is additive if it is preadditive and has finite products (equivalently, finite coproducts). Note that in the context of finite products, the preadditive structure is unique.', 'https://ncatlab.org/nlab/show/additive+category', 'additive', TRUE 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/Alg(R).sql b/database/data/004_property-assignments/Alg(R).sql index 9859632c..6d344167 100644 --- a/database/data/004_property-assignments/Alg(R).sql +++ b/database/data/004_property-assignments/Alg(R).sql @@ -35,12 +35,6 @@ VALUES TRUE, 'One can take the same proof as for $\mathbf{Ring}$.' ), -( - 'Alg(R)', - 'strict initial object', - FALSE, - 'The homomorphism $p_1 : R \times R \to R$ is not an isomorphism, and $R$ is initial.' -), ( 'Alg(R)', 'balanced', diff --git a/database/data/004_property-assignments/CAlg(R).sql b/database/data/004_property-assignments/CAlg(R).sql index 55936a86..f9fcd991 100644 --- a/database/data/004_property-assignments/CAlg(R).sql +++ b/database/data/004_property-assignments/CAlg(R).sql @@ -35,12 +35,6 @@ VALUES TRUE, 'One can use the same proof as for $\mathbf{CRing}$.' ), -( - 'CAlg(R)', - 'strict initial object', - FALSE, - 'The homomorphism $p_1 : R \times R \to R$ is not an isomorphism, and $R$ is initial.' -), ( 'CAlg(R)', 'balanced', diff --git a/database/data/004_property-assignments/CMon.sql b/database/data/004_property-assignments/CMon.sql index 42bffd78..57c2317c 100644 --- a/database/data/004_property-assignments/CMon.sql +++ b/database/data/004_property-assignments/CMon.sql @@ -33,7 +33,7 @@ VALUES 'CMon', 'preadditive', FALSE, - 'In categories with finite products and coproducts, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum $f+g : A \to B$ is the composite of $(f,g) : A \to B \times B$, the inverse of the canonical morphism $B \oplus B \to B \times B$ (which indeed must be an isomorphism), and the codiagonal $B \oplus B \to B$. In the case of $\mathbf{CMon}$, this is just the pointwise addition of maps, and this is indeed an enrichment of $\mathbf{CMon}$ over itself. But not over $\mathbf{Ab}$, since for example $\mathrm{Hom}(\mathbb{N},\mathbb{N}) \cong \mathbb{N}$ (with respect to addition) is not a group.' + 'In categories with finite products and finite coproducts, the preadditive structure is unique if it exists. In the case of $\mathbf{CMon}$, this is just the pointwise addition of maps. This is indeed an enrichment of $\mathbf{CMon}$ over itself, but not over $\mathbf{Ab}$, since for example $\mathrm{Hom}(\mathbb{N},\mathbb{N}) \cong \mathbb{N}$ (with respect to addition) is not a group.' ), ( 'CMon', diff --git a/database/data/004_property-assignments/CRing.sql b/database/data/004_property-assignments/CRing.sql index b0723750..8dd16e11 100644 --- a/database/data/004_property-assignments/CRing.sql +++ b/database/data/004_property-assignments/CRing.sql @@ -35,12 +35,6 @@ VALUES TRUE, '[Sketch] A ring homomorphism $f : A \times B \to R$ yields the idempotent element $e := f(1,0) \in R$, so that $R \cong eR \times (1-e)R$. Then $f$ decomposes into the ring homomorphisms $f_A : A \to eR$, $f_A(a) := f(a,0)$ and $f_B : B \to (1-e)R$, $f_B(b) := f(0,b)$.' ), -( - 'CRing', - 'strict initial object', - FALSE, - 'The homomorphism $p_1 : \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is not an isomorphism, and $\mathbb{Z}$ is initial.' -), ( 'CRing', 'balanced', 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 e9ce2f39..d85eedd2 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/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index 4d9180e2..16d5d589 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/database/data/004_property-assignments/Met.sql @@ -51,7 +51,7 @@ VALUES 'Met', 'strict initial object', TRUE, - 'This is because the initial object is the empty metric space.' + 'The empty metric space is initial and clearly strict.' ), ( 'Met', diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql index 636bd5f1..c301d62a 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/Rel.sql b/database/data/004_property-assignments/Rel.sql index db9c538f..17bbb152 100644 --- a/database/data/004_property-assignments/Rel.sql +++ b/database/data/004_property-assignments/Rel.sql @@ -57,7 +57,7 @@ VALUES 'Rel', 'preadditive', FALSE, - 'In categories with finite products and coproducts, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum $f+g : A \to B$ is the composite of $(f,g) : A \to B \times B$, the inverse of the canonical morphism $B \oplus B \to B \times B$ (which indeed must be an isomorphism), and the codiagonal $B \oplus B \to B$. In the case of $\mathbf{Rel}$, where both products and coproducts are just disjoint unions, this operation is just the set-theoretic union $f+g = f \cup g$ of relations. This clearly has no inverses.' + 'In categories with finite products and finite coproducts, the preadditive structure is unique if it exists. In the case of $\mathbf{Rel}$, where both products and coproducts are just disjoint unions, this operation is just the set-theoretic union $f+g = f \cup g$ of relations. This clearly has no inverses.' ), ( 'Rel', diff --git a/database/data/004_property-assignments/Ring.sql b/database/data/004_property-assignments/Ring.sql index 7bff0d0b..713ff07b 100644 --- a/database/data/004_property-assignments/Ring.sql +++ b/database/data/004_property-assignments/Ring.sql @@ -35,12 +35,6 @@ VALUES TRUE, 'To show that $A \sqcup_{A \times B} B$ is trivial, let $R$ be a ring which admits homomorphisms $f : A \to R$, $g : B \to R$ with $f(p_1(a,b))=g(p_2(a,b))$ for all $(a,b) \in A \times B$, i.e. $f(a)=g(b)$. Applying this to $a=0$, $b=1$ yields $1=0$ in $R$.' ), -( - 'Ring', - 'strict initial object', - FALSE, - 'The homomorphism $p_1 : \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is not an isomorphism, and $\mathbb{Z}$ is initial.' -), ( 'Ring', 'balanced', diff --git a/database/data/004_property-assignments/sSet.sql b/database/data/004_property-assignments/sSet.sql index a5e8903f..4dabcd11 100644 --- a/database/data/004_property-assignments/sSet.sql +++ b/database/data/004_property-assignments/sSet.sql @@ -21,7 +21,7 @@ VALUES 'sSet', 'generator', TRUE, - 'Let $\Delta^n := \mathrm{Hom}([n],)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\mathbf{sSet}$. Therefore, $\coprod_{n \geq 0} \Delta^n$ is a generator (see the proof of this implication).' + 'Let $\Delta^n := \mathrm{Hom}([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\mathbf{sSet}$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\mathbf{sSet}$.' ), ( 'sSet', diff --git a/database/data/004_property-assignments/walking_commutative_square.sql b/database/data/004_property-assignments/walking_commutative_square.sql index 2e34a52b..86551e68 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 086064d6..bbc83274 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/005_implications/003_size-constraints-implications.sql b/database/data/005_implications/003_size-constraints-implications.sql index e34cee57..5b4ee2cf 100644 --- a/database/data/005_implications/003_size-constraints-implications.sql +++ b/database/data/005_implications/003_size-constraints-implications.sql @@ -52,7 +52,7 @@ VALUES 'generator_via_coproduct', '["generating set", "coproducts", "zero morphisms"]', '["generator"]', - 'If $S$ is a generating set, we claim that $U := \coprod_{G \in S} G$ is a generator. For this it is not required to have zero morphisms, we only need that for all $G,G'' \in S$ there is at least one morphism $G \to G''$. This implies that each inclusion $G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphism with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.', + 'If $S$ is a generating set, we claim that $U := \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.', FALSE ), ( diff --git a/database/data/010_lemmas/000_lemmas.sql b/database/data/010_lemmas/000_lemmas.sql new file mode 100644 index 00000000..5ebf718d --- /dev/null +++ b/database/data/010_lemmas/000_lemmas.sql @@ -0,0 +1,43 @@ +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\}$.' +), +( + '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$.' +), +( + 'preadditive_structure_unique', + 'Uniqueness of preadditive structures', + 'Let $\mathcal{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 +$\alpha : X \oplus Y \to X \times Y$
+ is an isomorphism. Moreover, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum +$f+g : A \to B$
+ is the composite of $(f,g) : A \to B \times B$, the inverse $\alpha^{-1} : B \oplus B \to B \times B$, and the codiagonal $\nabla : B \oplus B \to B$.', + 'The morphism $\alpha : X \oplus Y \to X \times Y$ is defined by the equations +$p_1 \circ \alpha \circ i_1 = \mathrm{id}_X, \quad p_2 \circ \alpha \circ i_2 = \mathrm{id}_Y$
+$p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0$.
+ It does not depend on the choice of preadditive structure since zero morphisms are unique. It is an isomorphism: Define +$\beta := i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y$.
+ Then $\alpha \circ \beta = \mathrm{id}_{X \times Y}$ because +$p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \mathrm{id}_1 \circ p_1 + 0 \circ p_2 = p_1$
+ and likewise $p_2 \circ \alpha \circ \beta = p_2$. We also have $\beta \circ \alpha = \mathrm{id}_{X \oplus Y}$ with a very similar calculation that shows $\beta \circ \alpha \circ i_1 = i_1$ and $\beta \circ \alpha \circ i_2 = i_2$. +Therefore, for morphisms $f,g : A \rightrightarrows B$ the composite $A \to B$ in the claim is equal to
+ $\begin{aligned} \nabla \circ \beta \circ (f,g) & = \nabla \circ (i_1 \circ p_1 + i_2 \circ p_2) \circ (f,g) \\ & = \nabla \circ i_1 \circ p_1 \circ (f,g) + \nabla \circ i_2 \circ p_2 \circ (f,g) \\ & = p_1 \circ (f,g) + p_2 \circ (f,g) \\ & = f + g. \end{aligned}$' +), +( + 'generator_construction', + 'Construction of Generators', + 'In a category let $S$ be a generating set which is strongly connected (between any two objects in $S$ there is a morphism). If the coproduct $U := \coprod_{G \in S} G$ exists, then it is a generator.', + 'This is a straight forward generalization of this result. We remark that the assumption about $S$ implies that each inclusion $G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.' +); \ No newline at end of file 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