diff --git a/databases/catdat/data/functors/power_set_contravariant.yaml b/databases/catdat/data/functors/power_set_contravariant.yaml index f3737fcc..86882ad2 100644 --- a/databases/catdat/data/functors/power_set_contravariant.yaml +++ b/databases/catdat/data/functors/power_set_contravariant.yaml @@ -1,9 +1,9 @@ id: power_set_contravariant name: contravariant power set functor -notation: $\Hom(-,2)$ +notation: $P_{\forall}$ source: Set_op target: Set -description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$. It is isomorphic to the representable functor $\Hom(-,2) : \Set^{\op} \to \Set$.' +description: 'This functor $P_{\forall}$ maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$.' nlab_link: https://ncatlab.org/nlab/show/power+set tags: @@ -26,13 +26,13 @@ satisfied_properties: - property: right adjoint proof: >- - The functor $P : \Set^{\op} \to \Set$ is right adjoint to $P^{\op} : \Set \to \Set^{\op}$ since + The functor $P_{\forall} : \Set^{\op} \to \Set$ is right adjoint to $P_{\forall}^{\op} : \Set \to \Set^{\op}$ since $$\Hom_{\Set}(X,P(Y)) \cong P(X \times Y) \cong \Hom_{\Set}(Y,P(X)) = \Hom_{\Set^{\op}}(P(X),Y).$$ check_redundancy: false - property: preserves reflexive coequalizers proof: >- - This is contained in the proof of Theorem 2.2.7 (monadicity of $P$ for an elementary topos) in Johnstone, but we include a direct proof here for the sake of completeness, and also since we want the system to deduce monadicity automatically. + This is contained in the proof of Theorem 2.2.7 (monadicity of $P_{\forall}$ for an elementary topos) in Johnstone, but we include a direct proof here for the sake of completeness, and also since we want the system to deduce monadicity automatically. Let $f,g : X \rightrightarrows Y$ be two maps with a common retraction $r : Y \to X$, i.e. $rf = rg = \id_X$. Let $i : E \hookrightarrow X$ be their equalizer. We need to show that $i^* : P(X) \to P(E)$ is a coequalizer of $f^*,g^* : P(Y) \rightrightarrows P(X)$. First, $i^*$ is surjective since $i$ is injective, which implies that $A = i^*(i_*(A))$ for all $A \subseteq E$. Hence, $i^*$ is the quotient of $P(X)$ by the equivalence relation $\sim_1$ defined by $A \sim_1 B \iff i^*(A) = i^*(B)$, i.e. $A \cap E = B \cap E$. The coequalizer of $f^*,g^*$ is the quotient of $P(X)$ by the smallest equivalence relation $\sim_2$ satisfying $f^*(C) \sim_2 g^*(C)$ for all $C \subseteq Y$. We need to show that these equivalence relations coincide. diff --git a/databases/catdat/data/functors/power_set_covariant.yaml b/databases/catdat/data/functors/power_set_covariant.yaml index 4a9881d3..02d6cfbe 100644 --- a/databases/catdat/data/functors/power_set_covariant.yaml +++ b/databases/catdat/data/functors/power_set_covariant.yaml @@ -1,9 +1,9 @@ id: power_set_covariant name: covariant power set functor -notation: $P$ +notation: $P_{\exists}$ source: Set target: Set -description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.' +description: 'This functor $P_{\exists}$ maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.' nlab_link: https://ncatlab.org/nlab/show/power+set tags: @@ -17,7 +17,7 @@ satisfied_properties: proof: 'Let $f,g : X \rightrightarrows Y$ be two maps with $f_* = g_* : P(X) \rightrightarrows P(Y)$. Then $\{f(x)\} = f_*(\{x\}) = g_*(\{x\}) = \{g(x)\}$ and hence $f(x) = g(x)$ for all $x \in X$.' - property: preserves epimorphisms - proof: 'If $f : X \to Y$ is surjective, then $f_* \circ f^* = \id_{P(Y)}$, so that $f^*$ is surjective.' + proof: 'If $f : X \to Y$ is surjective, then $f_* \circ f^* = \id_{P(Y)}$, so that $f_*$ is surjective.' - property: preserves monomorphisms proof: 'If $f : X \to Y$ is injective, then $f^* \circ f_* = \id_{P(X)}$, so that $f_*$ is injective.' @@ -49,13 +49,13 @@ unsatisfied_properties: - property: preserves reflexive coequalizers proof: >- Consider the two maps $f,g : \IN \times \{0,1\} \rightrightarrows \IN$ defined by $f(n,i)=n$, $g(n,0)=n$, and $g(n,1)=n+1$. They form a reflexive pair with common section $n \mapsto (n,0)$. Their coequalizer is the quotient of $\IN$ by the equivalence relation generated by $n \sim n+1$, which collapses everything to a single point. Thus, the unique map $p : \IN \to \{\ast\}$ is a coequalizer of $f,g$. - The induced map $P(p) : P(\IN) \to P(\{\ast\}) = \{\varnothing,\{\ast\}\}$ sends $\varnothing$ to $\varnothing$ and every non-empty subset to $\{\ast\}$. In particular, all non-empty subsets of $\IN$ have the same image. + The induced map $p_* : P(\IN) \to P(\{\ast\}) = \{\varnothing,\{\ast\}\}$ sends $\varnothing$ to $\varnothing$ and every non-empty subset to $\{\ast\}$. In particular, all non-empty subsets of $\IN$ have the same image. - Next, we compute the coequalizer of $P(f),P(g) : P(\IN \times \{0,1\}) \rightrightarrows P(\IN)$. Identify $P(\IN \times \{0,1\})$ with $P(\IN) \times P(\IN)$. Under this identification, $P(f)$ sends a pair of subsets $(A,B)$ to $A \cup B$, while $P(g)$ sends it to $A \cup (B+1)$. + Next, we compute the coequalizer of $f_*, g_* : P(\IN \times \{0,1\}) \rightrightarrows P(\IN)$. Identify $P(\IN \times \{0,1\})$ with $P(\IN) \times P(\IN)$. Under this identification, $f_*$ sends a pair of subsets $(A,B)$ to $A \cup B$, while $g_*$ sends it to $A \cup (B+1)$. The coequalizer is the quotient of $P(\IN)$ by the equivalence relation generated by $$A \cup B \sim A \cup (B+1).$$ - This generated equivalence relation is the transitive closure of the symmetric closure. From this it follows that a finite subset is equivalent only to finite subsets. In particular, $\{0\}$ and $\IN$ are not equivalent, i.e. they do not have the same image in the coequalizer. Therefore, $P(p)$ cannot be the coequalizer. + This generated equivalence relation is the transitive closure of the symmetric closure. From this it follows that a finite subset is equivalent only to finite subsets. In particular, $\{0\}$ and $\IN$ are not equivalent, i.e. they do not have the same image in the coequalizer. Therefore, $p_*$ cannot be the coequalizer. - property: preserves equalizers proof: 'Any pair of distinct surjective maps $f,g : X \rightrightarrows Y$ provides a counterexample: Their equalizer $E$ is a proper subset of $X$, so that $P(E)$ cannot contain $X$. But $f_*(X) = Y = g_*(X)$ shows that $X$ is contained in the equalizer of $f_*,g_* : P(X) \rightrightarrows P(Y)$.' diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index aa6a2583..4ae32a78 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -10,35 +10,43 @@ import { error } from '@sveltejs/kit' export function fetch_category(id: string) { const { results, err } = batch< - [CategorySpecificDisplay, SpecialObject, SpecialMorphism] + [CategorySpecificDisplay, SpecialObject, SpecialMorphism, StructureShort] >([ // specific information for the category sql` - SELECT c.objects, c.morphisms - FROM categories c - WHERE c.id = ${id} - `, + SELECT c.objects, c.morphisms + FROM categories c + WHERE c.id = ${id} + `, // special objects sql` - SELECT s.type, s.description - FROM special_objects s - INNER JOIN special_object_types t ON t.type = s.type - WHERE s.category_id = ${id} - ORDER BY t.id - `, + SELECT s.type, s.description + FROM special_objects s + INNER JOIN special_object_types t ON t.type = s.type + WHERE s.category_id = ${id} + ORDER BY t.id + `, // special morphisms sql` - SELECT t.type, s.description, s.proof - FROM special_morphism_types t - LEFT JOIN special_morphisms s - ON s.type = t.type AND s.category_id = ${id} - ORDER BY t.id - `, + SELECT t.type, s.description, s.proof + FROM special_morphism_types t + LEFT JOIN special_morphisms s + ON s.type = t.type AND s.category_id = ${id} + ORDER BY t.id + `, + // functors whose source or target is the current category + sql` + SELECT f.id, s.name + FROM functors f + INNER JOIN structures s ON s.id = f.id + WHERE f.source = ${id} OR f.target = ${id} + ORDER BY lower(s.name) + `, ]) if (err) error(500, 'Could not load category') - const [categories, special_objects, special_morphisms] = results + const [categories, special_objects, special_morphisms, functors] = results if (!categories.length) error(404, `Could not find category with ID '${id}'`) @@ -46,6 +54,7 @@ export function fetch_category(id: string) { ...categories[0], special_objects, special_morphisms, + functors, } } diff --git a/src/lib/server/utils.ts b/src/lib/server/utils.ts index 09a9a3f7..6b7559e3 100644 --- a/src/lib/server/utils.ts +++ b/src/lib/server/utils.ts @@ -34,3 +34,11 @@ export function cache_page(event: RequestEvent) { // shared cache for 30min event.setHeaders({ 'cache-control': 'public, max-age=0, s-maxage=1800' }) } + +export function strip_math(s: string) { + return s.replaceAll('$', '') +} + +export function add_math(s: string) { + return `$${s}$` +} diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index 0baaa5c7..71fbbf65 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -30,6 +30,7 @@ comments: CommentObject[] definition?: Snippet specials?: Snippet + footer?: Snippet } let { @@ -45,6 +46,7 @@ comments, definition, specials, + footer, }: Props = $props() @@ -118,6 +120,8 @@ +{@render footer?.()} +