diff --git a/.cspell.json b/.cspell.json
index d060b9b65..2e78761b7 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -46,6 +46,7 @@
"Čech",
"characterisation",
"clopen",
+ "closedness",
"Clowder",
"coaccessible",
"cocartesian",
diff --git a/content/Top-embeds-in-LRS.md b/content/Top-embeds-in-LRS.md
new file mode 100644
index 000000000..5e50a217d
--- /dev/null
+++ b/content/Top-embeds-in-LRS.md
@@ -0,0 +1,52 @@
+---
+title: An embedding of the category of topological spaces in the category of locally ringed spaces
+description: Describes a functor which makes the category of topological spaces a coreflective and "almost reflective" subcategory of the category of locally ringed spaces. From the properties of this embedding, we can rule out several properties for the category of locally ringed spaces, using the corresponding failures of these properties for the category of topological spaces.
+author: Daniel Schepler
+---
+
+## An embedding of the category of topological spaces in the category of locally ringed spaces
+
+For much of this development, we will be dealing with the case of $\LRS_k$ where $k$ is a field. We begin by describing $\Top$ as a reflective subcategory of $\LRS_k$.
+
+::: Lemma 1
+The forgetful functor $U : \LRS_k \to \Top$ has a right adjoint $K : \Top \to \LRS_k$ of equipping a topological space $X$ with the constant sheaf $\underline{k}$. Furthermore, the functor $K$ is fully faithful, thus making $\Top$ into a reflective subcategory of $\LRS_k$.
+:::
+
+_Proof._ In this adjunction, the counit $UK \to \id$ is just the identity. To describe the unit $\id \to KU$, we need to define a morphism $(X, \O_X) \to (X, \underline{k})$ for any locally ringed space $(X, \O_X)$ over $k$. This morphism will be the identity on topological spaces, and the pullback operation $\underline{k} \to \O_X$ will be the unique morphism of sheaves induced by the given structure of $\O_X$ as a sheaf of $k$-algebras. It is now straightforward to check this indeed defines an adjunction; and since the counit is an isomorphism, that implies that $K$ is fully faithful. $\square$
+
+We now show that this reflective subcategory is in fact also a coreflective subcategory. Recall that for $f \in \O_X(U)$ we have its vanishing set $V(f) \coloneqq \{x\in U : f \in \m_{X,x}\} = \{x \in U : f(x) = 0\}$, where $f(x) \in \kappa(x)$ is the image of $f_x \in \O_{X,x}$ in the residue field.
+
+::: Lemma 2
+For each object $X$ of $\LRS_k$, let $X_0$ be the set of points $x \in X$ such that the induced morphism from $k$ to the residue field $\kappa(x)$ is an isomorphism. We give $X_0$ the following strengthening of the subspace topology: it will be the topology where a neighborhood subbasis at $x \in X_0$ is the collection of sets of the form $X_0 \cap V(f)$ where $f \in \O_X(U)$ for some neighborhood $U$ of $x$ in $X$, and $x \in V(f)$. Then $X \mapsto X_0$ defines a functor $S : \LRS_k \to \Top$ that is right adjoint to $K$.
+:::
+
+_Proof._ First, to see that $S$ is a functor, suppose we have a morphism $f : (X, \O_X) \to (Y, \O_Y)$. Then for $x \in X_0$, we have a sequence $k \to \kappa(f(x)) \to \kappa(x)$ where the composition is an isomorphism. Thus, $\kappa(f(x)) \to \kappa(x)$ is a surjective morphism of fields, and therefore an isomorphism. It follows that $k \to \kappa(f(x))$ is also an isomorphism of fields, so $f(x) \in Y_0$. To see that the restriction map $X_0 \to Y_0$ is continuous, suppose $g \in \O_Y(V)$ is such that $f(x) \in V(g)$. Then $x \in V(f^\sharp g)$, and
+$$X_0 \cap f^{-1}(Y_0 \cap V(g)) = X_0 \cap V(f^\sharp g)$$
+where $f^\sharp g \in \O_X(f^{-1}(V))$. In other words, we have shown that the inverse image in $X_0$ of any subbasic neighborhood of $f(x)$ is a neighborhood of $x$.
+
+Now if we apply the functor $S$ to a space of the form $(X, \underline{k})$, then since by definition any section of the constant sheaf $\underline{k}$ is locally constant, we see that we recover exactly $X$ with its original topology. Thus, we can define the unit $\id \to SK$ of the adjunction to be the identity.
+
+As for the counit $KS \to \id$, for any locally ringed space $(X, \O_X)$ over $k$ we need to define a morphism $(X_0, \underline{k}) \to (X, \O_X)$. The map of topological spaces will be the inclusion map $i : X_0 \hookrightarrow X$, which is continuous since in particular for $U$ an open neighborhood of $x \in X_0$ we have $X_0 \cap U = X_0 \cap V(0_U)$, where $0_U \in \O_X(U)$ is the zero element. The pullback map $\O_X \to i_* \underline{k}$ takes $f \in \O_X(U)$ to the function $X_0 \cap U \to k$ where $x \in X_0 \cap U$ maps to the inverse image of $f(x) \in \kappa(x)$ under the isomorphism $k \to \kappa(x)$. An alternative description of this pullback is that $x \in X_0 \cap U$ maps to the unique $a\in k$ such that $x \in V(f-a)$. Since $X_0 \cap V(f-a)$ is a neighborhood of $x$ in $X_0$ by definition, this shows that we get a locally constant function to $k$ as required.
+
+From here, it is straightforward to show that this does in fact define an adjunction. $\square$
+
+_Remark._ In the special case where $k$ is a finite field, we have
+$$\textstyle X_0 \cap V(f) = \bigcap_{a \in k^\times} (X_0 \cap D(f-a)),$$
+which is already open in the subspace topology. Therefore, in this case, $X_0$ is given exactly the subspace topology.
+
+::: Corollary 3
+For any non-trivial commutative ring $R$, fix a quotient field $k$. Then the functor $K_R : \Top \to \LRS_R$ of equipping a topological space with the constant sheaf $\underline{k}$ is fully faithful; has a right adjoint; and preserves all inhabited limits.
+:::
+
+_Proof._ The functor $K_R$ is the composition of $K : \Top \to \LRS_k$ and the forgetful functor $\LRS_k \to \LRS_R$. Since $\LRS_k$ is equivalent to the slice category of $\LRS_R$ over the subterminal object $\Spec k$, the forgetful functor is fully faithful; has right adjoint ${-} \times \Spec k$; and preserves all inhabited limits. Therefore, from the previously established results on $K$, the result follows. $\square$
+
+::: Corollary 4
+Let $R$ be any non-trivial commutative ring. Then:
+(a) $\LRS_R$ is not cartesian closed.
+(b) $\LRS_R$ does not have cartesian filtered colimits.
+(c) $\LRS_R$ is not regular.
+(d) $\LRS_R$ does not have filtered-colimit-stable epimorphisms.
+(e) $\LRS_R$ does not have effective cocongruences.
+:::
+
+_Proof._ We already know that $\Top$ does not satisfy any of these properties. In order to conclude that $\LRS_R$ does not satisfy any of them either, we fix a quotient field of $R$ as above and consider the functor $K_R$. In each case, this is an easy application of a contrapositive of a result from [here](/content/subcategories) to the functor $K_R$. Namely, (a) follows from Lemma 5; (b) from Lemma 4; (c) from Lemma 7; (d) from the dual of Lemma 2 with the observation that $K_R$ preserves epimorphisms since it has a right adjoint; and (e) from the dual of Lemma 8. $\square$
diff --git a/content/subcategories.md b/content/subcategories.md
index afb257c09..da05f1cec 100644
--- a/content/subcategories.md
+++ b/content/subcategories.md
@@ -1,7 +1,9 @@
---
title: Results on subcategories
description: We prove that several properties of categories descend to suitable subcategories.
-author: Martin Brandenburg
+authors:
+ - Martin Brandenburg
+ - Daniel Schepler
---
## Results on subcategories
@@ -48,3 +50,54 @@ $$
$$
$\square$
+
+::: Lemma 4
+Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite products and filtered colimits, and that $U$ preserves binary products and filtered colimits. If $\D$ has cartesian filtered colimits, then so does $\C$.
+:::
+
+_Proof._
+Let $X$ be an object of $\C$ and $Y : \I \to \C$ a filtered diagram. Then we have the canonical comparison map $c : \colim_{i\in\I} (X \times Y_i) \to X \times \colim_{i\in\I} Y_i$. By the assumptions, $Uc$ is equivalent to the comparison map $\colim_{i\in\I} (UX \times UY_i) \to UX \times \colim_{i\in\I} UY_i$, which is an isomorphism. Since $U$ is fully faithful and therefore conservative, we conclude that $c$ is an isomorphism. $\square$
+
+::: Lemma 5
+Let $U : \C \to \D$ be a fully faithful functor with a right adjoint $R : \D \to \C$ (i.e. $\C$ is equivalent to a coreflective subcategory of $\D$). Assume that $\C$ has binary products, and that $U$ preserves these binary products. If $\D$ is cartesian closed, then so is $\C$, with exponentials in $\C$ given by
+$$[X, Y]_{\C} \cong R([UX, UY]_{\D}).$$
+:::
+
+_Proof._ For any objects $X, Y, Z$ of $\C$ we have natural isomorphisms
+
+$$
+\begin{align*}
+\Hom_\C(Z\times X, Y) & \cong \Hom_\D(UZ \times UX, UY) \\
+& \cong \Hom_\D(UZ, [UX,UY]) \\
+& \cong \Hom_\C\bigl(Z, R([UX,UY])\bigr).
+\end{align*}
+$$
+
+$\square$
+
+::: Corollary 6
+If $\C$ is a cartesian closed category and $P$ is a [subterminal object](https://ncatlab.org/nlab/show/subterminal+object) of $\C$, then the slice category $\C / P$ is also cartesian closed, with exponentials in $\C / P$ given by
+$$[X, Y]_{\C / P} \cong [X, Y]_{\C} \times P.$$
+:::
+
+_Proof._ The forgetful functor $\C / P \to \C$ is fully faithful; it has right adjoint ${-} \times P$; and it preserves binary products (in fact all inhabited limits). Hence, Lemma 5 applies. $\square$
+
+::: Lemma 7
+Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves pullbacks and coequalizers. If $\D$ is regular, then so is $\C$.
+:::
+
+_Proof._ Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullback in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram
+$$X \times_Y X \rightrightarrows X \to \im(f) \xrightarrow{i} Y$$
+where $X \times_Y X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions, the image under $U$ is equivalent to the diagram in $\D$:
+$$UX \times_{UY} UX \rightrightarrows UX \to \im(Uf) \xrightarrow{Ui} UY$$
+where $UX \times_{UY} UX$ is the kernel pair of $Uf$, and $\im(Uf)$ is the coequalizer. Since $Uf$ is a regular epimorphism, we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $f$ is a regular epimorphism. $\square$
+
+::: Lemma 8
+Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves inhabited finite limits and coequalizers. If $\D$ has effective congruences, then so does $\C$.
+:::
+
+_Proof._ Suppose we have a congruence $E \hookrightarrow X\times X$ in $\C$. We can then form the quotient $X \to X/E$ as a coequalizer, along with the kernel pair $X \times_{X/E} X$ and the comparison map $i$ in the diagram below:
+$$E \xrightarrow{i} X \times_{X/E} X \rightrightarrows X \to X/E.$$
+By the assumptions, the image under $U$ is equivalent to the diagram in $\D$:
+$$UE \xrightarrow{Ui} UX \times_{U(X/E)} UX \rightrightarrows UX \to U(X/E).$$
+Here, $UE \rightrightarrows UX$ is a congruence: the map $UE \to UX \times UX$ is a monomorphism since $U$ preserves pullbacks and therefore preserves monomorphisms; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ to reflexivity and symmetry morphisms for $UE$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ to a transitivity morphism for $UE$. This congruence $UE$ of $\D$ is effective, so we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $E$ is effective. $\square$
diff --git a/databases/catdat/data/categories/LRS_R.yaml b/databases/catdat/data/categories/LRS_R.yaml
index 112b01fe8..d50bea326 100644
--- a/databases/catdat/data/categories/LRS_R.yaml
+++ b/databases/catdat/data/categories/LRS_R.yaml
@@ -53,6 +53,22 @@ unsatisfied_properties:
Alternatively, using the usual adjunction between affine schemes and locally ringed spaces (EGA I (1971), Ch. 1, Prop. 1.6.3), a generating set in $\LRS_R$ would induce a generating set in the category of affine $R$-schemes, which contradicts the fact that $\CAlg(R)$ does not have a cogenerating set.
+ - property: cartesian closed
+ proof: This is Corollary 4(a) here.
+ check_redundancy: false
+
+ - property: cartesian filtered colimits
+ proof: This is Corollary 4(b) here.
+
+ - property: regular
+ proof: This is Corollary 4(c) here.
+
+ - property: cofiltered-limit-stable epimorphisms
+ proof: This is Corollary 4(d) here.
+
+ - property: effective cocongruences
+ proof: This is Corollary 4(e) here.
+
special_objects:
initial object:
description: empty space
diff --git a/databases/catdat/data/category-implications/cartesian closed.yaml b/databases/catdat/data/category-implications/cartesian closed.yaml
index a952b1134..a8e6c17e1 100644
--- a/databases/catdat/data/category-implications/cartesian closed.yaml
+++ b/databases/catdat/data/category-implications/cartesian closed.yaml
@@ -107,3 +107,12 @@
- locally cartesian closed
proof: Each slice is thin, semi-strongly connected, and has a terminal object. Thus, it corresponds to a linear order with a largest element $1$. Every such category is cartesian closed, where the exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.
is_equivalence: false
+
+- id: cartesian_closed_thin_implies_lcc
+ assumptions:
+ - cartesian closed
+ - thin
+ conclusions:
+ - locally cartesian closed
+ proof: In a thin category, every object is subterminal. Thus, the result follows from Corollary 6 here.
+ is_equivalence: false
diff --git a/src/lib/server/markdown.ts b/src/lib/server/markdown.ts
index 6285e7a24..2c062079c 100644
--- a/src/lib/server/markdown.ts
+++ b/src/lib/server/markdown.ts
@@ -146,6 +146,7 @@ type ContentMetaData = {
title: string
description: string
author?: string
+ authors?: string[]
}
/**
diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte
index 436fae2e2..3a91d9135 100644
--- a/src/routes/content/[id]/+page.svelte
+++ b/src/routes/content/[id]/+page.svelte
@@ -15,6 +15,8 @@
{#if data.meta_data.author}
Author: {data.meta_data.author}
+{:else if data.meta_data.authors} +Authors: {data.meta_data.authors.join(', ')}
{/if} {#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0} @@ -88,5 +90,9 @@ :global(span.qed) { float: right; } + + :global(p:has(span.qed:only-child)) { + height: 1lh; + } }