add spell checking

ScriptRaccoon · ScriptRaccoon · commit b996dd9802f0 · 2026-03-17T12:17:32.000+01:00
diff --git a/.vscode/extensions.json b/.vscode/extensions.json
@@ -0,0 +1,8 @@
+{
+	"recommendations": [
+		"svelte.svelte-vscode",
+		"fivethree.vscode-svelte-snippets",
+		"esbenp.prettier-vscode",
+		"streetsidesoftware.code-spell-checker"
+	]
+}
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -5,5 +5,134 @@
 		".svelte-kit": true,
 		"node_modules": true,
 		"build": true
-	}
+	},
+	"cSpell.ignoreWords": ["Abfg", "Vect", "Zdiv", "Setne", "Xmark"],
+	"cSpell.words": [
+		"abelian",
+		"Adamek",
+		"algébriques",
+		"anneaux",
+		"Auslander",
+		"bijection",
+		"bijections",
+		"bijective",
+		"cancellative",
+		"Catabase",
+		"catdat",
+		"Clowder",
+		"cocomplete",
+		"cocompletion",
+		"cocontinuous",
+		"codiagonal",
+		"coequalizer",
+		"coequalizers",
+		"cofiltered",
+		"cogenerates",
+		"cogenerator",
+		"cokernel",
+		"colimit",
+		"colimits",
+		"conormal",
+		"coproduct",
+		"coproducts",
+		"corestricts",
+		"coslice",
+		"cospan",
+		"delooping",
+		"deloopings",
+		"Demazure",
+		"diffeomorphism",
+		"diffeomorphisms",
+		"dualizable",
+		"Dualization",
+		"Engelking",
+		"epimorphism",
+		"épimorphismes",
+		"epimorphisms",
+		"exponentials",
+		"finitary",
+		"Freyd",
+		"functor",
+		"functorial",
+		"functors",
+		"Gillam",
+		"Grothendieck",
+		"Groupes",
+		"groupoid",
+		"groupoids",
+		"Heyting",
+		"homotopy",
+		"infimum",
+		"infinitary",
+		"injection",
+		"injections",
+		"injective",
+		"Isbell",
+		"Kashiwara",
+		"katex",
+		"Kolmogorov",
+		"libsql",
+		"Malcev",
+		"Mathoverflow",
+		"metrizable",
+		"Moerdijk",
+		"monoid",
+		"monoidal",
+		"monoids",
+		"monomorphism",
+		"monomorphisms",
+		"morphism",
+		"morphisms",
+		"nlab",
+		"objectwise",
+		"pointwise",
+		"Pontrjagin",
+		"poset",
+		"posets",
+		"preadditive",
+		"preimage",
+		"preimages",
+		"preordered",
+		"prerender",
+		"prerendered",
+		"Prerendering",
+		"protomodular",
+		"pushout",
+		"pushouts",
+		"rng",
+		"rngs",
+		"Rosicky",
+		"Schapira",
+		"semisimple",
+		"setoid",
+		"Sheafifiable",
+		"simplicial",
+		"submonoid",
+		"subobject",
+		"subobjects",
+		"subscheme",
+		"subsheaf",
+		"suprema",
+		"supremum",
+		"surjection",
+		"surjections",
+		"surjective",
+		"Turso",
+		"unital",
+		"vercel",
+		"Vite",
+		"well-copowered",
+		"Yoneda",
+		"Zulip"
+	],
+	"cSpell.ignorePaths": [
+		"node_modules",
+		"pnpm-lock.yaml",
+		".git",
+		".vscode",
+		".svelte-kit",
+		".netlify",
+		"build"
+	],
+	"cSpell.ignoreRegExpList": ["\\$[^$]*\\$"]
 }
diff --git a/DATABASE.md b/DATABASE.md
@@ -50,7 +50,7 @@ The command `pnpm db:deduce` deduces implications, properties, and non-propertie
 
 Use `pnpm db:update` to run all the commands in sequence: `pnpm db:migrate`, `pnpm db:seed`, and `pnpm db:deduce`.
 
-Use `pnpm db:watch` to run this command automatically everytime a file in the subfolder [/database/data](/database/data) changes. This is useful in particular during development.
+Use `pnpm db:watch` to run this command automatically every time a file in the subfolder [/database/data](/database/data) changes. This is useful in particular during development.
 
 ## Diagram
 
diff --git a/database/data/001_categories.sql b/database/data/001_categories.sql
@@ -278,7 +278,7 @@ VALUES
 	),
 	(
 		'Zdiv',
-		'preorder of integers w.r.t. divisiblity',
+		'preorder of integers w.r.t. divisibility',
 		'$(\mathbb{Z},\mid)$',
 		'integers',
 		'a unique morphism $(a,b) : a \to b$ if $a$ divides $b$',
diff --git a/database/data/005_properties.sql b/database/data/005_properties.sql
@@ -373,8 +373,6 @@ VALUES
 	),
 
     -- other properties
-
-
 	(
 		'inhabited',
 		'is',
@@ -442,15 +440,15 @@ VALUES
 	(
 		'zero morphisms',
 		'has',
-		'A category has <i>zero morphisms</i> if for every pair of objects $A,B$ there is a distinugished morphism $0_{A,B} : A \to B$, called the zero morphism, such that we have $f \circ 0_{A,B} = 0_{A,C}$ and $0_{B,C} \circ g = 0_{A,C}$ for all morphisms $f : B \to C$ and $g : A \to B$. The zero morphisms are unique if they exist, hence this is actually a property of the category.',
+		'A category has <i>zero morphisms</i> if for every pair of objects $A,B$ there is a distinguished morphism $0_{A,B} : A \to B$, called the zero morphism, such that we have $f \circ 0_{A,B} = 0_{A,C}$ and $0_{B,C} \circ g = 0_{A,C}$ for all morphisms $f : B \to C$ and $g : A \to B$. The zero morphisms are unique if they exist, hence this is actually a property of the category.',
 		'https://ncatlab.org/nlab/show/zero+morphism',
 		'zero morphisms',
 		TRUE
 	),
 	(
 		'preadditive',
 		'is',
-		'A category is <i>preadditive</i> when it is locally essentially small* and each hom-set carries the structure of an abelian group such that the composition is bilinear. Notice that "preadditive" is an extra structure. The property here just says that some preadditive structure exists.<br>*We demand this instead of the more common "locall small" to ensure that preadditive categories are invariant under equivalences of categories.',
+		'A category is <i>preadditive</i> when it is locally essentially small* and each hom-set carries the structure of an abelian group such that the composition is bilinear. Notice that "preadditive" is an extra structure. The property here just says that some preadditive structure exists.<br>*We demand this instead of the more common "locally small" to ensure that preadditive categories are invariant under equivalences of categories.',
 		'https://ncatlab.org/nlab/show/Ab-enriched+category',
 		'preadditive',
 		TRUE
diff --git a/database/data/007_category-properties.sql b/database/data/007_category-properties.sql
@@ -802,7 +802,7 @@ VALUES
 	(
 		'Met_c',
 		'countable products',
-		 'For finite products, we take the cartesian product with, say, the sup-metric. The prouct of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking''s book <i>General Topoloy</i>.'
+		 'For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking''s book <i>General Topology</i>.'
 	),
 
 	(
@@ -889,7 +889,7 @@ VALUES
 	(
 		'Sch',
 		'pullbacks',
-		'This is the well-known construction of the fiber product of schemes, see e.g. EGA I, Chap. I, Théorème 3.2.1.'
+		'This is the well-known construction of the fiber product of schemes, see e.g. EGA I, Chap. I, Thm. 3.2.1.'
 	),
     (
         'Sch',
@@ -1398,7 +1398,7 @@ VALUES
 	(
 		'Sp',
 		'epi-regular',
-		'This follows from the corresponding fact for $\mathbf{FinSet}$ since there every epiomorphism is even effective.'
+		'This follows from the corresponding fact for $\mathbf{FinSet}$ since there every epimorphism is even effective.'
 	),
 	(
 		'Sp',
diff --git a/database/data/008_category-non-properties.sql b/database/data/008_category-non-properties.sql
@@ -1161,5 +1161,4 @@ VALUES
 		'Setne',
 		'skeletal',
 		'trivial'
-	);
-
+	);
diff --git a/database/data/012_epimorphisms.sql b/database/data/012_epimorphisms.sql
@@ -202,7 +202,7 @@ VALUES
 	(
 		'FinOrd',
 		'surjective order-preserving maps',
-		'The proof is similar to the one for $\mathbf{Set}$: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphismus $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^*(A) = f^*(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^*(A) \setminus f^*(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.'
+		'The proof is similar to the one for $\mathbf{Set}$: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphisms $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^*(A) = f^*(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^*(A) \setminus f^*(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.'
 	),
 	(
 		'Rel',
diff --git a/database/data/013_implications.sql b/database/data/013_implications.sql
@@ -293,7 +293,7 @@ VALUES
 		FALSE
 	),
 	(
-		'locally_countabley_presentable_raise',
+		'locally_countably_presentable_raise',
 		'["locally ℵ₁-presentable"]',
 		'["locally presentable"]',
 		'trivial',
@@ -582,7 +582,7 @@ VALUES
 		FALSE
 	),
 	(
-		'subobject_classifier_wellpowered',
+		'subobject_classifier_well-powered',
 		'["subobject classifier", "locally essentially small"]',
 		'["well-powered"]',
 		'<a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Prop. I.3.1',
@@ -647,7 +647,7 @@ VALUES
 		FALSE
 	),
 	(
-		'topos_wellcopowered_criterion',
+		'topos_well-copowered_criterion',
 		'["elementary topos", "locally essentially small"]',
 		'["well-copowered"]',
 		'This follows from <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Theorem IV.7.8 (and Prop. I.3.1).',
@@ -682,7 +682,7 @@ VALUES
 		FALSE
 	),
 	(
-		'grothendieck_abelian_selfdual',
+		'grothendieck_abelian_self-dual',
 		'["Grothendieck abelian", "self-dual"]',
 		'["trivial"]',
 		'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, <i>Abelian categories</i>, p. 116.',

Original file line number	Diff line number	Diff line change
`@@ -278,7 +278,7 @@ VALUES`
`278`	`278`	`),`
`279`	`279`	`(`
`280`	`280`	`'Zdiv',`
`281`		`- 'preorder of integers w.r.t. divisiblity',`
	`281`	`+ 'preorder of integers w.r.t. divisibility',`
`282`	`282`	`'$(\mathbb{Z},\mid)$',`
`283`	`283`	`'integers',`
`284`	`284`	`'a unique morphism $(a,b) : a \to b$ if $a$ divides $b$',`
Original file line number	Diff line number	Diff line change
`@@ -802,7 +802,7 @@ VALUES`
`802`	`802`	`(`
`803`	`803`	`'Met_c',`
`804`	`804`	`'countable products',`
`805`		`- 'For finite products, we take the cartesian product with, say, the sup-metric. The prouct of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking''s book <i>General Topoloy</i>.'`
	`805`	`+ 'For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking''s book <i>General Topology</i>.'`
`806`	`806`	`),`
`807`	`807`
`808`	`808`	`(`
`@@ -889,7 +889,7 @@ VALUES`
`889`	`889`	`(`
`890`	`890`	`'Sch',`
`891`	`891`	`'pullbacks',`
`892`		`- 'This is the well-known construction of the fiber product of schemes, see e.g. EGA I, Chap. I, Théorème 3.2.1.'`
	`892`	`+ 'This is the well-known construction of the fiber product of schemes, see e.g. EGA I, Chap. I, Thm. 3.2.1.'`
`893`	`893`	`),`
`894`	`894`	`(`
`895`	`895`	`'Sch',`
`@@ -1398,7 +1398,7 @@ VALUES`
`1398`	`1398`	`(`
`1399`	`1399`	`'Sp',`
`1400`	`1400`	`'epi-regular',`
`1401`		`- 'This follows from the corresponding fact for $\mathbf{FinSet}$ since there every epiomorphism is even effective.'`
	`1401`	`+ 'This follows from the corresponding fact for $\mathbf{FinSet}$ since there every epimorphism is even effective.'`
`1402`	`1402`	`),`
`1403`	`1403`	`(`
`1404`	`1404`	`'Sp',`
Original file line number	Diff line number	Diff line change
`@@ -202,7 +202,7 @@ VALUES`
`202`	`202`	`(`
`203`	`203`	`'FinOrd',`
`204`	`204`	`'surjective order-preserving maps',`
`205`		- 'The proof is similar to the one for $\mathbf{Set}$: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphismus $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^(A) = f^(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^(A) \setminus f^(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.'
	`205`	+ 'The proof is similar to the one for $\mathbf{Set}$: If $f : X \to Y$ is an epimorphism of (finite) orders, in particular for all morphisms $g,h : Y \to \{0 < 1\}$ with $g \circ f = h \circ f$ we have $g = h$. This means for all upper sets $A,B \subseteq Y$ with $f^(A) = f^(B)$ we have $A = B$. If $y \in Y$, apply this to the intervals $A = Y_{\geq y}$ and $B = Y_{> y}$, which are different. Hence, there is some $x \in f^(A) \setminus f^(B)$, which means $f(x) \geq y$ but not $f(x) > y$, so that $f(x) = y$.'
`206`	`206`	`),`
`207`	`207`	`(`
`208`	`208`	`'Rel',`