Prove remaining properties of the category of locally ringed spaces

.cspell.json

@@ -39,6 +39,7 @@
 		"anneaux",
 		"Aronszajn",
 		"Artin",
+		"Artinian",
 		"Auslander",
 		"Axiomatising",
 		"axiomatization",
@@ -217,6 +218,7 @@
 		"functionals",
 		"functor",
 		"functorial",
+		"functoriality",
 		"functors",
 		"Gillam",
 		"Gille",
@@ -312,6 +314,7 @@
 		"Neumann",
 		"Neves",
 		"Niefield",
+		"nilpotent",
 		"nilradical",
 		"nimbers",
 		"nlab",
@@ -377,6 +380,7 @@
 		"Sierpiński",
 		"simplicial",
 		"simplicially",
+		"Šmulian",
 		"Specker",
 		"Strecker",
 		"subalgebra",
@@ -414,7 +418,6 @@
 		"surjective",
 		"surjectivity",
 		"surjects",
-		"Šmulian",
 		"Szamuely",
 		"Tarski",
 		"tensoring",
@@ -429,6 +432,7 @@
 		"Tyrer",
 		"Ulmer",
 		"ultrafilters",
+		"ultrapower",
 		"uncountably",
 		"unital",
 		"unitalization",

CLAUDE.md

@@ -120,7 +120,7 @@ Content:
 - **Easy to understand**: state the claim or key idea first, then the details ("We claim that ... To see this, ..."). Name objects and morphisms explicitly with source and target (`f : X \to Y`). For unsatisfied properties, give a concrete counterexample (e.g. "the embedding $C_2 \hookrightarrow S_3$") rather than an existence argument, whenever possible.
 - **Complete**: do not skip steps. Phrases like "It is easy to see" or "clearly" are only for exceptional cases, namely steps that are routine for the intended reader. One-line proofs such as "This is trivial." or "This holds by definition." are only for claims that follow immediately from the definitions.
 - **Classifications and equivalences**: when one direction is immediate, prove only the other one and say so ("For the non-trivial direction, ..."), as in most special-morphism proofs. In content pages, mark the two directions with `($\implies$)` and `($\impliedby$)`, and steps in a cycle of equivalences with `(1) $\implies$ (2)`.
-- **Building on known facts**: a proof may use properties of the same structure that are assigned earlier in the file or deduced from them ("We already know that ..."), as well as its classification of special morphisms ("(see below)"). Results about other structures may be used with a link to them. If a proof depends on the proof of another assignment, give that assignment a `label` of the form `<structure id>_<short description>` (e.g. `grp_no_cogenerator`) and list the label under `references`.
+- **Building on known facts**: a proof may use properties of the same structure that are assigned earlier in the file or deduced from them ("We already know that ..."), as well as its classification of special morphisms ("(see below)"). Results about other structures may be used with a link to them. **Whenever a proof refers to the proof of another assignment**, give that assignment a `label` of the form `<structure id>_<short description>` (e.g. `Grp_no_cogenerator`) and list the label under `references` of the citing assignment. This applies to every kind of reference, including loose ones such as "see the proof for $\LRS_R$" or "the idea is the same as in the proof for $\CAlg(R)$". It is essential to avoid dead references: assignments are regularly removed when they become redundant (e.g. after a new implication), and since `references` is a foreign key to the label, `db:seed` then fails instead of silently keeping a proof that refers to a deleted one. Without the reference, nothing detects this. Before removing a labeled assignment, rewrite the citing proofs.
 - **Reuse instead of repetition**: put general lemmas in `content/` pages instead of repeating an argument in several YAML files, and apply them explicitly, e.g. "apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the forgetful functor $\Ab \to \Grp$".
 - **Generalize concrete proofs**: once a proof for a specific structure works, check which features of the structure it really uses. If these are general properties (e.g. infinitary extensivity, existence of certain limits), state the result as an implication, or as a lemma in a `content/` page if it cannot be phrased with existing properties. An implication is much more powerful than a single assignment: the deduction system applies it, and its dual, to every structure, which decides further properties and makes existing direct proofs redundant. After adding one, run `pnpm db:update` and remove the redundant assignments (or mark them with `check_redundancy: false` if other proofs cite them). Example: the proof that $\LRS_R$ is not coaccessible only used that $\LRS_R$ is infinitary extensive, which led to the implication `infinitary_extensive_not_coaccessible`. It also decided `Met_c` and made the proofs for `LRS_R`, `Sch_R`, `Top`, and `Quiv_fc` redundant.
 

content/local-ring-epimorphisms.md

@@ -0,0 +1,32 @@
+---
+title: Epimorphisms of local commutative rings
+description: The codomain of an epimorphism in the category of local commutative rings is not much larger than its domain. This is used to prove that the category of locally ringed spaces is well-powered.
+---
+
+# Epimorphisms of local commutative rings
+
+We consider the category of local commutative rings and local homomorphisms.
+
+::: Lemma
+Let $\varphi : A \to B$ be a local homomorphism of local commutative rings which is an epimorphism in the category of local commutative rings and local homomorphisms. Then $|B| \leq \max(|A|,\aleph_0)$.
+:::
+
+::: Proof
+The homomorphism $\varphi$ factors as a surjective homomorphism $A \to \varphi(A)$ followed by the inclusion $\varphi(A) \hookrightarrow B$. The ring $\varphi(A)$ is local since it is a non-zero quotient ring of $A$. The inclusion $\varphi(A) \hookrightarrow B$ is a local homomorphism and an epimorphism in the category of local commutative rings and local homomorphisms, and $|\varphi(A)| \leq |A|$. Hence, we may assume that $A$ is a subring of $B$ and that $\varphi$ is the inclusion.
+
+A _system_ over $A$ in the variables $Y_1,\dotsc,Y_n$ consists of finitely many polynomials $p_1,\dotsc,p_k \in A[Y_1,\dotsc,Y_n]$ and a subset $J \subseteq \{1,\dotsc,n\}$. A _solution_ of the system is a tuple $(c_1,\dotsc,c_n) \in B^n$ with $p_i(c_1,\dotsc,c_n) = 0$ for all $i$ and $c_j \in \m_B$ for all $j \in J$. We say that the system _determines_ $b \in B$ if it has a solution and every solution $(c_1,\dotsc,c_n)$ satisfies $c_1 = b$. Every system determines at most one element, and there are at most $\max(|A|,\aleph_0)$ systems over $A$. Hence, it suffices to prove that every $b \in B$ is determined by some system over $A$.
+
+Assume that $b \in B$ is not determined by any system over $A$. Let $\F$ be the set of finite subsets of $B$ containing $b$. For $F \in \F$ we consider the system $\Sigma_F$ over $A$ in the variables $Y_x$ for $x \in F$, enumerated such that $Y_b$ is the first variable, which consists of the polynomials
+
+- $Y_x + Y_{x'} - Y_{x''}$ for $x,x',x'' \in F$ with $x + x' = x''$,
+- $Y_x Y_{x'} - Y_{x''}$ for $x,x',x'' \in F$ with $x x' = x''$,
+- $Y_a - a$ for $a \in F \cap A$,
+
+and the subset $F \cap \m_B \subseteq F$. The tuple $(x)_{x \in F}$ is a solution of $\Sigma_F$. Since $\Sigma_F$ does not determine $b$, it has another solution $(g_F(x))_{x \in F}$ with $g_F(b) \neq b$. We extend $g_F$ to a map $g_F : B \to B$ by $g_F(x) \coloneqq 0$ for $x \notin F$.
+
+For a finite subset $E \subseteq B$ let $\F_{\supseteq E} \coloneqq \{F \in \F : E \subseteq F\}$. These sets are non-empty since $E \cup \{b\} \in \F_{\supseteq E}$, and they satisfy $\F_{\supseteq E} \cap \F_{\supseteq E'} = \F_{\supseteq E \cup E'}$. Hence, they have the finite intersection property, so that there is an ultrafilter $\U$ on $\F$ containing all of them. Let $T \coloneqq B^\F / \U$ be the ultrapower, i.e. the quotient of the ring $B^\F$ by the ideal of all families $(t_F)_{F \in \F}$ with $\{F \in \F : t_F = 0\} \in \U$. We write $[t_F]$ for the class of $(t_F)_{F \in \F}$. Then $T$ is a local commutative ring whose maximal ideal $\m_T$ consists of the classes $[t_F]$ with $\{F \in \F : t_F \in \m_B\} \in \U$. Indeed, these classes form an ideal not containing $1$, and every other class $[t_F]$ has $t_F \in B^\times$ for all $F$ in a set $M \in \U$, so that it is invertible with inverse $[u_F]$, where $u_F \coloneqq t_F^{-1}$ for $F \in M$ and $u_F \coloneqq 0$ otherwise. (Alternatively, this follows from [Łoś's theorem](https://en.wikipedia.org/wiki/Ultraproduct#%C5%81o%C5%9B's_theorem).)
+
+We define two maps $\delta, g : B \to T$ by $\delta(x) \coloneqq [x]$ and $g(x) \coloneqq [g_F(x)]$. The map $\delta$ is a local homomorphism since $x \in \m_B$ implies $[x] \in \m_T$. For $x,x' \in B$ and all $F \in \F_{\supseteq \{x,x',x+x',xx'\}}$ we have
+$$g_F(x + x') = g_F(x) + g_F(x'), \quad g_F(x x') = g_F(x) \, g_F(x'),$$
+and for $a \in A$ and all $F \in \F_{\supseteq \{a\}}$ we have $g_F(a) = a$. Since $1 \in A$, this shows that $g$ is a ring homomorphism with $g(a) = \delta(a)$ for all $a \in A$. Moreover, $g$ is local since $g_F(x) \in \m_B$ for $x \in \m_B$ and all $F \in \F_{\supseteq \{x\}}$. Since the inclusion $A \hookrightarrow B$ is an epimorphism, we get $\delta = g$. But $g_F(b) \neq b$ for all $F \in \F$, so that $g(b) \neq \delta(b)$, a contradiction.
+:::

content/subcategories.md

@@ -117,20 +117,16 @@ Finally, to prove the parenthetical remark, assume that $\C$ has binary products
 :::
 
 ::: Lemma 9
-Let $L$ be a functor which is left adjoint to a faithful functor $U$. Then $L$ preserves generating collections. (Thus in particular, any reflective subcategory of a category with a generating collection also has a generating collection; and similarly for a single generator.)
+Let $U : \C \to \D$ be a faithful functor with a left adjoint $L : \D \to \C$. Then $L$ preserves generating collections. If $U$ is also conservative, then $L$ preserves extremal generating collections. (Thus in particular, any reflective subcategory of a category with a generating collection also has a generating collection; and similarly for a single generator.)
 :::
 
 ::: Proof
-If $S$ is a generating collection,
+Let $S$ be a collection of objects of $\D$. By the adjunction, the functor
+$$(\Hom(L(G),-))_{G \in S} : \C \to (\Set^+)^S$$
+is isomorphic to the composition of $U : \C \to \D$ followed by
+$$(\Hom(G,-))_{G \in S} : \D \to (\Set^+)^S.$$
 
-$$
-\begin{align*}
-\prod_{G\in S} \Hom(L(G),-) & \cong \prod_{G\in S} \Hom(G,U(-)) \\
-& \cong \left( \prod_{G\in S} \Hom(G,-) \right) \circ U
-\end{align*}
-$$
-
-is a composition of faithful functors, hence faithful.
+If $S$ is a generating collection, this is a composition of faithful functors, hence faithful. If $S$ is an extremal generating collection and $U$ is conservative, this is a composition of faithful conservative functors, hence faithful and conservative.
 :::
 
 ::: Lemma 10