Add more examples of functors to witness property combinations

.cspell.json

@@ -18,7 +18,8 @@
 		"coloneqq",
 		"FiltVect",
 		"networkidle",
-		"devlog"
+		"devlog",
+		"cech"
 	],
 	"words": [
 		"abelian",
@@ -79,6 +80,7 @@
 		"cofiltering",
 		"cofinal",
 		"cofinitary",
+		"cofinite",
 		"cofull",
 		"cogenerates",
 		"cogenerating",
@@ -92,6 +94,7 @@
 		"comonadic",
 		"comonadicity",
 		"compactification",
+		"compactifications",
 		"conormal",
 		"copower",
 		"copowers",
@@ -156,6 +159,7 @@
 		"functorial",
 		"functors",
 		"Gillam",
+		"Glicksberg",
 		"grothendieck",
 		"Grothendieck",
 		"Groupes",
@@ -188,6 +192,7 @@
 		"Kashiwara",
 		"Kategorien",
 		"katex",
+		"Kerodon",
 		"Kolmogorov",
 		"Kunen",
 		"Lawvere",

database/data/categories/N_oo.yaml

@@ -1,6 +1,6 @@
 id: N_oo
 name: partially ordered set of extended natural numbers
-notation: $(\IN_\infty, \leq)$
+notation: $(\IN \cup \{\infty\}, \leq)$
 objects: natural numbers and $\infty$
 morphisms: 'a unique morphism $(n, m) : n \to m$ if $n \leq m$, where of course $n \leq \infty$ for all $n$'
 description: null

database/data/functor-implications/adjoints.yaml

@@ -54,3 +54,11 @@
     - coreflector
   proof: 'Let $F : \C \to 1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : 1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.'
   is_equivalence: false
+
+- id: reflector_preserves_terminal_objects
+  assumptions:
+    - reflector
+  conclusions:
+    - preserves terminal objects
+  proof: 'Let $\C \subseteq \D$ be a full reflective subcategory with reflector $R : \D \to \C$ and unit morphisms $u(X) : X \to R(X)$ for $X \in \D$. The universal property says that every morphism from $X$ into an object in $\C$ factors uniquely through $u(X)$. Let $1 \in \D$ be a terminal object. We claim that $u(1) : 1 \to R(1)$ is an isomorphism. In fact, since $1$ is terminal, there is a (unique) morphism $v : R(1) \to 1$ in $\D$. The composition $v \circ u(1)$ is the identity since $1$ is terminal. To show that also the composition $u(1) \circ v$ is the identity of $R(1)$, by the universal property of $u(1)$ it suffices to prove $u(1) \circ v \circ u(1) = u(1)$, which is immediate from $v \circ u(1) = \id_1$. This shows $R(1) \cong 1$. Now, since $R(1)$ is an object in $\C$ which is terminal in $\D$, it is a terminal object of $\C$.'
+  is_equivalence: false

database/data/functor-implications/limits preservation.yaml

@@ -223,3 +223,16 @@
     - preserves equalizers
   proof: This is trivial.
   is_equivalence: false
+
+- id: thin_binary_product_preservation
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - thin
+      - semi-strongly connected
+    codomain:
+      - thin
+  conclusions:
+    - preserves binary products
+  proof: 'It is enough to prove that if $P$ is a linearly ordered set and $Q$ is a partially ordered set, then any order-preserving map $f : P \to Q$ preserves binary meets. Let $x,y \in P$. We may assume $x \leq y$. Then $x \wedge y = x$. Since we also have $f(x) \leq f(y)$, we have $f(x) \wedge f(y) = f(x)$. Therefore, $f(x \wedge y) = f(x) \wedge f(y)$ holds.'
+  is_equivalence: false

database/data/functor-implications/misc.yaml

@@ -147,3 +147,24 @@
     - full on isomorphisms
   proof: This is trivial.
   is_equivalence: false
+
+- id: thin_dominant_functor
+  assumptions:
+    - dominant
+  mapped_assumptions:
+    codomain:
+      - regular-subobject-trivial
+  conclusions:
+    - essentially surjective
+  proof: This is trivial since every split monomorphism in the codomain is an isomorphism.
+  is_equivalence: false
+
+- id: automatic_preserves_mono
+  assumptions: []
+  mapped_assumptions:
+    codomain:
+      - left cancellative
+  conclusions:
+    - preserves monomorphisms
+  proof: This is trivial since every morphism in the codomain is a monomorphism.
+  is_equivalence: false

database/data/functor-implications/monadic.yaml

@@ -20,3 +20,13 @@
     - monadic
   proof: This is the crude monadicity theorem. A proof can be found in <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Thm. IV.4.2.
   is_equivalence: false
+
+- id: monadic_fully_faithful
+  assumptions:
+    - fully faithful
+    - right adjoint
+  conclusions:
+    - monadic
+    - left-invertible
+  proof: A direct proof of monadicity is possible and straight forward. Alternatively, one can use <a href="https://ncatlab.org/nlab/show/monadicity+theorem" target="_blank">Beck's monadicity theorem</a>, since a fully faithful functor $U$ is conservative and creates coequalizers of $U$-split pairs. For the left adjoint $L$ the counit $L \circ U \to \id$ is an isomorphism (since $U$ is fully faithful, see Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>), which shows that $U$ is left-invertible.
+  is_equivalence: false

database/data/functors/binary_coproduct_sets.yaml

@@ -41,6 +41,3 @@ unsatisfied_properties:
 
   - property: essentially injective
     proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$.
-
-  - property: reflector
-    proof: 'Its right adjoint, the diagonal functor $\Delta : \Set \to \Set \times \Set$, is faithful, but not full.'

database/data/functors/forget_abelian.yaml

@@ -14,6 +14,7 @@ tags:
 related:
   - forget_group
   - forget_inverses
+  - forget_torsion_free
 
 satisfied_properties:
   - property: full

database/data/functors/forget_inverses.yaml

@@ -15,6 +15,7 @@ related:
   - forget_group
   - forget_abelian
   - forget_group_pointed
+  - forget_torsion_free
 
 satisfied_properties:
   - property: full

database/data/functors/forget_torsion_free.yaml

@@ -0,0 +1,36 @@
+id: forget_torsion_free
+name: forgetful functor from torsion-free abelian groups
+notation: $U_{\TorsFreeAb, \Ab}$
+domain: TorsFreeAb
+codomain: Ab
+description: 'This is the inclusion functor $\TorsFreeAb \hookrightarrow \Ab$. It can also be seen as a forgetful functor which forgets the property of being torsion-free. The functor provides a typical example of a fully faithful functor that does not preserve coequalizers and does not preserve epimorphisms.'
+nlab_link: null
+left_adjoint: null
+
+tags:
+  - algebra
+  - forgetful
+
+related:
+  - forget_abelian
+  - forget_inverses
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: right adjoint
+    proof: The forgetful functor is right adjoint to the functor $\Ab \to \TorsFreeAb$ that sends an abelian group to its torsion-free reflection $A/T(A)$, where $T(A)$ is the torsion subgroup of $A$.
+
+  - property: finitary
+    proof: This comes out of the construction of filtered colimits in <a href="/category/TorsFreeAb">$\TorsFreeAb$</a>.
+
+  - property: preserves regular epimorphisms
+    proof: In both $\Ab$ and $\TorsFreeAb$, regular epimorphisms are exactly the surjective group homomorphisms.
+
+unsatisfied_properties:
+  - property: preserves epimorphisms
+    proof: 'The homomorphism $2 : \IZ \to \IZ$ is an epimorphism in $\TorsFreeAb$, but its image in $\Ab$ is not an epimorphism. See the pages for these categories for descriptions of their epimorphisms.'
+
+  - property: dominant
+    proof: Not every abelian group is torsion-free, and every subgroup of a torsion-free abelian group is torsion-free.

database/data/functors/inclusion_ordinals.yaml

@@ -0,0 +1,27 @@
+id: inclusion_ordinals
+name: inclusion functor from extended natural numbers to ordinal numbers
+notation: $\iota$
+domain: N_oo
+codomain: On
+description: 'This is the inclusion map from the partially ordered set $(\IN \cup \{\infty\},\leq)$ (considered as a thin category as usual) into the partially ordered collection $(\On,\leq)$, where we map $\infty$ to the ordinal $\omega$. It is an example of a functor that preserves binary products, but not terminal objects.'
+nlab_link: https://ncatlab.org/nlab/show/identity+functor
+left_adjoint: null
+
+tags:
+  - set theory
+
+related: []
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: preserves coproducts
+    proof: The map preserves suprema by construction.
+
+  - property: cofinitary
+    proof: More generally, the functor preserves all non-empty indexed limits, because the map of partially ordered sets preserves all non-empty indexed infima.
+
+unsatisfied_properties:
+  - property: preserves terminal objects
+    proof: The terminal object is mapped to $\omega$, which is not terminal. In fact, $\On$ has no terminal object at all.

database/data/functors/nerve.yaml

@@ -0,0 +1,44 @@
+id: nerve
+name: nerve functor
+notation: $N$
+domain: Cat
+codomain: sSet
+description: The nerve of a small category $\C$ is the simplicial set $N(\C)$ whose $n$-simplices are chains of morphisms $X_0 \to \cdots \to X_n$. Among other things, it provides an example of a fully faithful functor that does not preserve regular epimorphisms.
+nlab_link: https://ncatlab.org/nlab/show/nerve
+left_adjoint: null
+
+tags:
+  - category theory
+  - topology
+
+related: []
+
+satisfied_properties:
+  - property: fully faithful
+    proof: See <a href="https://kerodon.net/tag/002Z" target="_blank">Kerodon/002Z</a>.
+
+  - property: preserves coproducts
+    proof: This is immediate from the description of coproducts in $\Cat$ and $\sSet$. A chain of morphisms in a coproduct of categories $\coprod_i \C_i$ must be contained entirely in one of the $\C_i$.
+
+  - property: right adjoint
+    proof: See Theorem 2.1 at the <a href="https://ncatlab.org/nlab/show/nerve+and+realization" target="_blank">nLab</a>.
+
+  - property: finitary
+    proof: 'It suffices to prove that for every $n \in \IN$, the composite functor $N_n : \Cat \to \Set$ is finitary, where $N_n$ maps a small category to its set of $n$-chains of morphisms. This is easy to check directly using the concrete descriptions of filtered colimits in $\Cat$ and $\Set$. Alternatively, one can observe that $N_n$ is represented by the thin category $\{0 \to 1 \to \cdots \to n\}$, which is a finitely presentable object in $\Cat$.'
+
+unsatisfied_properties:
+  - property: preserves regular epimorphisms
+    proof: >-
+      Consider the thin categories $\C = \{0 \to 1, \, 1' \to 2\}$ and $\D = \{0 \to 1 \to 2\}$. There is a regular epimorphism $P : \C \to \D$ that identifies $1$ with $1'$. In fact, it is the coequalizer of the two functors $\{*\} \rightrightarrows \C$ whose images are $1$ and $1'$, respectively.
+      Notice that the map $\Mor(P) : \Mor(\C) \to \Mor(\D)$ is not surjective, as the morphism $0 \to 2$ in $\D$ has no preimage in $\C$. In other words, the map $N_1(P) : N_1(\C) \to N_1(\D)$ is not surjective. Therefore, $N(P)$ is not an epimorphism.
+
+  - property: dominant
+    proof: >-
+      The nerve of a small category $\C$ has the property that the canonical map
+      $$(d_2,d_0) : N_2(\C) \to N_1(\C) \times N_1(\C)$$
+      is injective, where $d_0,d_2$ are the face operators. In fact, this map simply sends a $2$-simplex $X_0 \xrightarrow{f} X_1 \xrightarrow{g} X_2$ to the pair consisting of $X_0 \xrightarrow{f} X_1$ and $X_1 \xrightarrow{g} X_2$.
+      Every simplicial set $S$ with a monomorphism to $N(\C)$ then also has the property that
+      $$(d_2,d_0) : S_2 \to S_1 \times S_1$$
+      is injective. Equivalently, every two morphisms $\Delta^2 \rightrightarrows S$ that coincide on the <a href="https://ncatlab.org/nlab/show/horn#examples" target="_blank">inner horn</a> $\Lambda^2_1 \subseteq \Delta^2$ are already equal. However, the simplicial set
+      $$S := \Delta^2 \sqcup_{\Lambda^2_1} \Delta^2$$
+      does not have this property.

database/data/functors/span_endpoints_inclusion.yaml

@@ -23,14 +23,5 @@ satisfied_properties:
     proof: This follows from the dual of Lemma 2 <a href="/content/functors_on_discrete_categories">here</a>.
 
 unsatisfied_properties:
-  - property: dominant
-    proof: The object $0 \in \Span$ does not admit a split monomorphism to either $1$ or $2$.
-
   - property: left-invertible
     proof: 'Assume that there is a functor $F : \Span \to \{1,2\}$ with $F(E(X)) \cong X$ for $X \in \{1,2\}$. Thus, $F(1) = 1$ and $F(2) = 2$. There are two possible choices for $F(0)$. Without loss of generality, assume that $F(0) = 1$. Then the morphism $0 \to 2$ in the walking span induces a morphism $1 = F(0) \to F(2) = 2$ in the discrete category, but no such morphism exists.'
-
-  - property: right adjoint
-    proof: This follows from Corollary 4 <a href="/content/functors_on_discrete_categories">here</a>.
-
-  - property: left adjoint
-    proof: This follows from the dual of Corollary 4 <a href="/content/functors_on_discrete_categories">here</a>.

database/data/functors/stone-cech-compactification.yaml

@@ -0,0 +1,38 @@
+id: stone-cech-compactification
+name: Stone-Čech compactification functor
+notation: $\beta$
+domain: Top
+codomain: CompHaus
+description: This functor $\beta$ is the left adjoint of the forgetful functor $\CompHaus \hookrightarrow \Top$. There are various constructions (see <a href="https://en.wikipedia.org/wiki/Stone%E2%80%93%C4%8Cech_compactification" target="_blank">Wikipedia</a>), one being that $\beta(X)$ is the closure of the image of the canonical map $X \to [0,1]^{\Hom(X,[0,1])}$. Among other things, this functor provides an example of a reflector that does not preserve binary products.
+nlab_link: https://ncatlab.org/nlab/show/Stone-%C4%8Cech+compactification
+left_adjoint: null
+
+tags:
+  - topology
+
+related: []
+
+satisfied_properties:
+  - property: reflector
+    proof: See for example Theorem 5.2 at the <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space" target="_blank">nLab</a>.
+
+unsatisfied_properties:
+  - property: essentially injective
+    proof: If $X$ is a non-empty indiscrete space, then $\beta(X)$ has only one point.
+
+  - property: faithful
+    proof: If $X$ is an indiscrete space with $n \geq 2$ points, then $\Hom(X,X)$ has $n^n$ elements, but $\Hom(\beta(X),\beta(X))$ has exactly one element, and $n^n > 1$.
+
+  - property: full
+    proof: By Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>, the left adjoint $\beta$ is full if and only if the unit morphism $X \to \beta(X)$ is a split epimorphism in $\Top$ for every $X \in \Top$. But if $X$ is a Tychonoff space, $X \to \beta(X)$ is a monomorphism, so it can only be a split epimorphism when it is an isomorphism, i.e. that $X$ is compact. Thus, $X := \IN$ provides a concrete counterexample.
+
+  - property: preserves regular monomorphisms
+    proof: >-
+      Consider the discrete space $\IN$ of natural numbers. The continuous map $\IN \hookrightarrow \IN \cup \{\infty\}$ into its one-point compactification is an embedding, hence a regular monomorphism in $\Top$, but its image $\beta(\IN) \to \beta(\IN \cup \{\infty\}) \cong \IN \cup \{\infty\}$ cannot be injective, for example since $\beta(\IN)$ is uncountable (more precisely, it has cardinality $2^{2^{\aleph_0}}$).
+      Alternatively, if we view $\beta(\IN)$ as the set of ultrafilters on $\IN$, the map sends the principal ultrafilter $[n]$ to $n$, and every other ultrafilter to $\infty$. So it suffices to construct two non-principal ultrafilters on $\IN$. Let $X$ be the set of even and $Y$ be the set of odd numbers. Then the family containing $X$ and all cofinite subsets of $\IN$ has the finite intersection property, hence is contained in an ultrafilter $U_X$. Similarly, there is an ultrafilter $U_Y$. Then $X \cap Y = \varnothing$ implies $X \in U_X \setminus U_Y$.
+
+  - property: preserves binary products
+    proof: It is a classical result that the canonical map $\beta(\IN \times \IN) \to \beta(\IN) \times \beta(\IN)$ (where $\IN$ carries the discrete topology) is not a homeomorphism. See Glicksberg, <a href="https://doi.org/10.1090/S0002-9947-1959-0105667-4" target="_blank">Stone-Čech compactifications of products</a>, where it shown for infinite completely regular spaces $X,Y$ that $\beta(X \times Y) \to \beta(X) \times \beta(Y)$ is a homeomorphism if and only if $X \times Y$ is pseudo-compact.
+
+  - property: cofinitary
+    proof: TBA

src/routes/missing/+page.svelte

@@ -92,14 +92,14 @@
 {#each STRUCTURE_TYPES as type}
 	{@const combinations = data.missing_combinations[type]}
 
-	{#if combinations.length > 0}
-		<section>
-			<h3>Missing {type} combinations</h3>
+	<section>
+		<h3>Missing {type} combinations</h3>
 
+		{#if combinations.length}
 			<p class="hint">
-				Among the consistent {type} combinations of the form p &and; &not;q, the following
-				are not yet witnessed by a {type} in the database or its dual. If some of these
-				combinations <i>are</i>
+				Among the consistent {type} property combinations of the form p &and; &not;q,
+				the following are not yet witnessed by a {type} in the database or its dual.
+				If some of these combinations <i>are</i>
 				inconsistent, this indicates that some
 				<a href="/{type}-implications">implication</a> is missing.
 			</p>
@@ -119,8 +119,15 @@
 					{/each}
 				</ul>
 			</details>
-		</section>
-	{/if}
+		{:else}
+			<p class="hint">
+				Every consistent {type} property combination of the form p &and; &not;q is witnessed
+				by a {type} in the database or its dual. 🎉
+			</p>
+
+			<p>&mdash;</p>
+		{/if}
+	</section>
 {/each}
 
 <SuggestionForm />