Provide details for extensivity proofs

.cspell.json

@@ -46,6 +46,7 @@
 		"brauer",
 		"Bredon",
 		"cancellative",
+		"Carboni",
 		"cartesian",
 		"Catabase",
 		"catdat",
@@ -77,6 +78,7 @@
 		"coequalizes",
 		"coexact",
 		"coexponentials",
+		"coextensivity",
 		"cofiltered",
 		"cofiltering",
 		"cofinal",

content/subcategories.md

@@ -83,7 +83,7 @@ _Proof._ The forgetful functor $\C / P \to \C$ is fully faithful; it has right a
 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
+_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 pullbacks 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$$
@@ -119,3 +119,9 @@ Any fully faithful functor reflects extremal generating sets (and therefore, by
 :::
 
 _Proof:_ Under the given assumptions, we can factor $\C \to (\Set^+)^S$, $X \mapsto (\Hom_\C(G, X))_{G\in S}$, as being isomorphic to the composition of $U : \C \to D$ followed by $Y \mapsto (\Hom_\D(UG, Y))_{G\in S}$, using the assumption on $U$ to identify $\Hom_\D(UG, UX)$ with $\Hom_C(G, X)$ naturally in $X$. In this composition, the first is fully faithful and therefore also conservative; and the second is assumed to be faithful and conservative. Therefore, the composition is also faithful and conservative. <span class="qed">$\square$</span>
+
+::: Lemma 11
+Let $U : \C \to \D$ be a faithful conservative functor (for example, a fully faithful functor). Assume that $\D$ is extensive, that $\C$ has finite coproducts and pullbacks along coproduct inclusions, and that $U$ preserves both. Then $\C$ is extensive. A similar statement holds for infinitary extensive (and countably extensive) categories, in which case we assume that $\C$ has all coproducts (resp. all countable coproducts) and that $U$ preserves these.
+:::
+
+_Proof._ This is straight forward. We need to prove that finite coproducts are disjoint and stable under pullbacks in $\C$. If $A,B \in \C$, the coproduct inclusion $A \to A + B$ is a monomorphism: Since $U$ is faithful, it suffices to prove that its image under $U$ is a monomorphism. Since $U$ preserves finite coproducts, the image identifies with the coproduct inclusion $U(A) \to U(A) + U(B)$, which is a monomorphism since $\D$ is extensive. Moreover, the unique morphism $0 \to A \times_{A + B} B$ is an isomorphism: Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the unique morphism $0 \to U(A) \times_{U(A) + U(B)} U(B)$, which is an isomorphism since $\D$ is extensive. This proves that finite coproducts are disjoint in $\C$. To prove that they are stable under pullbacks, let $T \to A + B$ be any morphism in $\C$, and consider the pullbacks $T_A := T \times_{A + B} A$ and $T_B := T \times_{A + B} B$. We need to show that the canonical morphism $T_A + T_B \to T$ is an isomorphism. Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the canonical morphism $U(T)_{U(A)} + U(T)_{U(B)} \to U(T)$ induced by the morphism $U(T) \to U(A) + U(B)$ in $\D$, which is an isomorphism since $\D$ is extensive. <span class="qed">$\square$</span>

database/data/categories/CRing.yaml

@@ -32,7 +32,21 @@ satisfied_properties:
     proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
 
   - property: coextensive
-    proof: '[Sketch] A ring homomorphism $f : A \times B \to R$ yields the idempotent element $e \coloneqq 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) \coloneqq f(a,0)$ and $f_B : B \to (1-e)R$, $f_B(b) \coloneqq f(0,b)$.'
+    proof: >-
+      We already know that $\CRing$ has products and pushouts, since it is finitary algebraic. Concretely, the pushout of a span $A \leftarrow R \rightarrow B$ can be constructed as the tensor product $A \otimes_R B$ with the obvious multiplication. Finite products are disjoint because the projection $p_1 : A \times B \to A$ is clearly surjective, hence an epimorphism, and the tensor product $A \otimes_{p_1,A \times B,p_2} B = 0$ is the zero ring (the terminal object), since
+      $$a \otimes b = a \cdot p_1(1,0) \otimes b = a \otimes p_2(1,0) \cdot b = a \otimes 0 = 0.$$
+      It remains to check that finite products are stable under pushouts. Let
+      $$f : A \times B \to T$$
+      be a ring homomorphism, and consider the pushouts
+      $$\begin{align*}
+      T_A & := A \otimes_{p_1,A \times B,f} T \\
+      T_B & := B \otimes_{p_2,A \times B,f} T.
+      \end{align*}$$
+      We need to prove that the canonical homomorphism
+      $$T \to T_A \times T_B$$
+      is an isomorphism. Since $p_1 : A \times B \to A$ is surjective with kernel $0 \times B = \langle (0,1) \rangle$, we have $T_A = T/\langle f(1,0)\rangle$, and likewise, $T_B = T/\langle f(0,1) \rangle$. The elements $f(1,0)$ and $f(0,1)$ are orthogonal idempotents in $T$. Therefore, the claim follows from the well-known result in commutative algebra that if $R$ is a commutative ring and $e \in R$ is an idempotent, then $R \to R/\langle e \rangle \times R/\langle 1-e \rangle$ is an isomorphism. One can also deduce this from the Chinese Remainder Theorem.
+
+      An alternative proof, which we only sketch, uses the category of locally ringed spaces <a href="/category/LRS_R">$\LRS$</a>, which is infinitary extensive. It follows that the category of affine schemes is extensive by Lemma 11 <a href="/content/subcategories">here</a>, and this category is anti-equivalent to $\CRing$. This argument is not circular since our proof of extensivity of $\LRS$ does not use coextensivity of $\CRing$.
 
 unsatisfied_properties:
   - property: skeletal

database/data/categories/Cat.yaml

@@ -27,15 +27,15 @@ satisfied_properties:
   - property: semi-strongly connected
     proof: Every non-empty category is weakly terminal (by using constant functors).
 
-  - property: infinitary extensive
-    proof: '[Sketch] This is straight forward from the fact that <a href="/category/Set">$\Set$</a> is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.'
-
   - property: extremal generator
     proof: >-
       The <a href="/category/walking_morphism">walking morphism</a> $I$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $I$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms.
 
       In fact, $I$ is an extremal generator: suppose $F : \C \to \D$ is a functor which induces a bijection $\Mor(\C) \to \Mor(\D)$. By considering the images of identity morphisms in $\C$, we see that $F$ is injective on objects; and then by considering the preimages of identity morphisms in $\D$, we see that $F$ is surjective on objects. By assumption, $F$ is also bijective on morphisms, so $F$ is an isomorphism of categories.
 
+  - property: infinitary extensive
+    proof: 'We have just seen that the walking morphism is an extremal generator, which means that the functor $\Mor : \Cat \to \Set$ is faithful and conservative. Moreover, $\Cat$ has coproducts and pullbacks, since it is locally finitely presentable. The functor $\Mor$ preserves coproducts by their concrete description and, being representable, also preserves pullbacks. Therefore, the claim follows from the extensivity of $\Set$ and Lemma 11 <a href="/content/subcategories">here</a>.'
+
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.
@@ -94,7 +94,7 @@ special_objects:
   terminal object:
     description: <a href="/category/1">trivial category</a>
   coproducts:
-    description: disjoint unions
+    description: disjoint unions with no morphisms between objects in distinct summands
   products:
     description: direct products with pointwise operations
 

database/data/categories/CompHaus.yaml

@@ -53,7 +53,7 @@ satisfied_properties:
       with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c'' \in C$, by Urysohn''s lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c'') = 1$. Also, by Tietze''s extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c''))$, we conclude that $j(c) \ne j(c'')$. This shows that $j$ is injective, so it is a regular monomorphism.'
 
   - property: extensive
-    proof: This follows as for <a href="/category/Top">$\Top$</a> or <a href="/category/Haus">$\Haus$</a> since finite coproducts in $\CompHaus$ are formed as disjoint union spaces with the disjoint union topology.
+    proof: This follows from Lemma 11 <a href="/content/subcategories">here</a> since <a href="/category/Top">$\Top$</a> is infinitary extensive and its full subcategory $\CompHaus$ is closed under pullbacks and finite coproducts in $\Top$.
 
   - property: cofiltered-limit-stable epimorphisms
     proof: 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by lemma 1 <a href="/content/comphaus_copresentable">here</a>, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.'

database/data/categories/FinSet.yaml

@@ -14,7 +14,7 @@ related:
   - FS
   - Set
   - Set_c
-  - Set_f
+  - Set_ff
 
 satisfied_properties:
   - property: locally small

database/data/categories/FreeAb.yaml

@@ -37,7 +37,7 @@ satisfied_properties:
 
   - property: regular
     proof: |-
-      This follows formally from the fact that <a href="/category/Ab">$\Ab$</a> is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a> it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup of $B$, hence free abelian, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms.
+      This follows formally from the fact that <a href="/category/Ab">$\Ab$</a> is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a> it suffices to prove that there are (reg epi, mono)-factorizations that are stable under pullbacks. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup of $B$, hence free abelian, and $A \to C$ is surjective. Clearly, surjective homomorphisms are stable under pullbacks. It remains to show that they coincide with the regular epimorphisms.
       (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\Ab$. Since $A \times_B A$ is free abelian (as a subgroup of $A \times A$), $f$ is also a coequalizer in $\FreeAb$.
       (2) If $f : A \to B$ is a regular epimorphism in $\FreeAb$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective.
 

database/data/categories/Haus.yaml

@@ -35,7 +35,7 @@ satisfied_properties:
     check_redundancy: false
 
   - property: infinitary extensive
-    proof: This follows exactly as for <a href="/category/Top">$\Top$</a> since Hausdorff spaces are closed under taking subspaces and coproducts in $\Top$.
+    proof: This follows from Lemma 11 <a href="/content/subcategories">here</a> since <a href="/category/Top">$\Top$</a> is infinitary extensive and its full subcategory $\Haus$ is closed under pullbacks and coproducts in $\Top$.
 
   - property: well-powered
     proof: This is clear from the classification of monomorphisms as injective continuous maps.

database/data/categories/LRS_R.yaml

@@ -29,7 +29,20 @@ satisfied_properties:
     proof: This follows from the characterization of epimorphisms below.
 
   - property: infinitary extensive
-    proof: '[Sketch] Since <a href="/category/Top">$\Top$</a> is infinitary extensive, a morphism $f : Y \to \coprod_i X_i \eqqcolon X$ yields a decomposition $Y = \coprod_i Y_i$ (as topological spaces) with continuous maps $f_i : Y_i \to X_i$. Endow the open subset $Y_i \subseteq Y$ with the restricted sheaf. Then each $f_i$ becomes a morphism of locally ringed spaces, and $Y = \coprod_i Y_i$ holds as locally ringed spaces.'
+    proof: >-
+      The proof works for both ringed and locally ringed spaces and relies on the fact that <a href="/category/Top">$\Top$</a> is infinitary extensive.
+
+      First, recall some basic facts about open embeddings (often called open immersions in the context of schemes). If $(X,\O_X)$ is a locally ringed space and $U \subseteq X$ is an open subset, then, letting $\O_U := (\O_X)|_U$, the pair $(U,\O_U)$ is again a locally ringed space. There is an inclusion morphism $(i,i^\sharp) : (U,\O_U) \to (X,\O_X)$, where $i$ is the inclusion map and $i^\sharp : \O_X \to i_* \O_U$ is defined via restriction maps. This is a monomorphism, and a morphism into $(X,\O_X)$ factors through it if and only if the image of its underlying map is contained in $U$. We will refer to any monomorphism isomorphic to one of this form as an open embedding.
+
+      Pullbacks along open embeddings exist and are themselves open embeddings. Indeed, if $(f,f^\sharp) : (X,\O_X) \to (Y,\O_Y)$ is a morphism of locally ringed spaces and $V \subseteq Y$ is an open subset, then $f^*(V) \subseteq X$ is an open subset, and $(f^*(V),\O_{f^*(V)}) \hookrightarrow (X,\O_X)$ is the pullback of $(f,f^\sharp)$ along $(V,\O_V) \hookrightarrow (Y,\O_Y)$.
+
+      Since $\LRS_R$ is cocomplete, coproducts exist. Concretely, the coproduct of a family of locally ringed spaces $(X_i,\O_{X_i})$ is the locally ringed space $(X,\O_X)$, where $X := \coprod_i X_i$ and $\O_X(U) := \prod_i \O_{X_i}(U \cap X_i)$. Notice that the coproduct inclusions are open embeddings. Hence, pullbacks along coproduct inclusions exist.
+
+      That coproducts are disjoint in $\LRS_R$ follows from the corresponding property of $\Top$ together with the following observations. By the descriptions above, the forgetful functor $\LRS_R \to \Top$ preserves coproducts and pullbacks along open embeddings (although it does not preserve pullbacks in general), and the empty topological space admits a unique structure sheaf, up to isomorphism, making it into a locally ringed space.
+
+      It remains to prove that coproducts are stable under pullbacks. To this end, let $(f,f^\sharp) : (T,\O_T) \to \coprod_i (X_i,\O_{X_i})$ be a morphism. Then $T_i := f^*(X_i) \subseteq T$ is an open subset, and for $i \neq j$ we have $T_i \cap T_j = \varnothing$ because $X_i \cap X_j = \varnothing$ in the coproduct. We must show that the canonical morphism $(g,g^\sharp) : \coprod_i (T_i,\O_{T_i}) \to (T,\O_T)$ is an isomorphism. The underlying continuous map $g$ is a homeomorphism because coproducts in $\Top$ are stable under pullbacks. It therefore remains to show that $g^\sharp : \O_T \to g_* \O$, where $\O$ denotes the structure sheaf of the coproduct, is an isomorphism. Equivalently, for every open subset $U \subseteq T$, we must show that the canonical ring homomorphism
+      $$\textstyle \O_T(U) \to \prod_{i \in I} \O_{T_i}(U \cap T_i) = \prod_{i \in I} \O_T(U \cap T_i)$$
+      is an isomorphism. This is precisely the sheaf axiom applied to the open cover of $U$ by the pairwise disjoint open subsets $U \cap T_i$.
 
 unsatisfied_properties:
   - property: skeletal