From 4bfc851ae474b4666501a8b3e031cc19c2be9da2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 20:48:46 +0200 Subject: [PATCH 01/15] fully faithful right adjoints are monadic and left-invertible --- database/data/functor-implications/monadic.yaml | 10 ++++++++++ database/data/functors/span_endpoints_inclusion.yaml | 6 ------ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/database/data/functor-implications/monadic.yaml b/database/data/functor-implications/monadic.yaml index d964d199..9742136f 100644 --- a/database/data/functor-implications/monadic.yaml +++ b/database/data/functor-implications/monadic.yaml @@ -20,3 +20,13 @@ - monadic proof: This is the crude monadicity theorem. A proof can be found in Mac Lane & Moerdijk, 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 Beck's monadicity theorem, 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 nLab), which shows that $U$ is left-invertible. + is_equivalence: false diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index 95ede225..b45e5388 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -28,9 +28,3 @@ unsatisfied_properties: - 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 here. - - - property: left adjoint - proof: This follows from the dual of Corollary 4 here. From f104eb2d5d302050d0ad0fa9b10776993c998a41 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 21:09:22 +0200 Subject: [PATCH 02/15] add the forgetful functor for torsion-free abelian groups --- database/data/functors/forget_abelian.yaml | 1 + database/data/functors/forget_inverses.yaml | 1 + .../data/functors/forget_torsion_free.yaml | 36 +++++++++++++++++++ 3 files changed, 38 insertions(+) create mode 100644 database/data/functors/forget_torsion_free.yaml diff --git a/database/data/functors/forget_abelian.yaml b/database/data/functors/forget_abelian.yaml index ea6c02a8..4a047451 100644 --- a/database/data/functors/forget_abelian.yaml +++ b/database/data/functors/forget_abelian.yaml @@ -14,6 +14,7 @@ tags: related: - forget_group - forget_inverses + - forget_torsion_free satisfied_properties: - property: full diff --git a/database/data/functors/forget_inverses.yaml b/database/data/functors/forget_inverses.yaml index ed7df41d..f3996d71 100644 --- a/database/data/functors/forget_inverses.yaml +++ b/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 diff --git a/database/data/functors/forget_torsion_free.yaml b/database/data/functors/forget_torsion_free.yaml new file mode 100644 index 00000000..e3656799 --- /dev/null +++ b/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 $\TorsFreeAb$. + + - 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. From 014d78f824971f85b91ec5195346f4729297e072 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 22:39:17 +0200 Subject: [PATCH 03/15] add more basic implications of functors --- .../limits preservation.yaml | 13 ++++++++++++ database/data/functor-implications/misc.yaml | 21 +++++++++++++++++++ .../functors/span_endpoints_inclusion.yaml | 3 --- 3 files changed, 34 insertions(+), 3 deletions(-) diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index 2cc9670d..d92ac8f9 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/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 diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 9e915b32..066f04cb 100644 --- a/database/data/functor-implications/misc.yaml +++ b/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 diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index b45e5388..a639f7d1 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -23,8 +23,5 @@ satisfied_properties: proof: This follows from the dual of Lemma 2 here. 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.' From 9bc538e86de88ebee8e0ed650f43e01f658976ff Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 22:39:33 +0200 Subject: [PATCH 04/15] add the inclusion functor IN u {oo} ---> On --- database/data/categories/N_oo.yaml | 2 +- .../data/functors/inclusion_ordinals.yaml | 27 +++++++++++++++++++ 2 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 database/data/functors/inclusion_ordinals.yaml diff --git a/database/data/categories/N_oo.yaml b/database/data/categories/N_oo.yaml index 7303fcb0..3cfadcf6 100644 --- a/database/data/categories/N_oo.yaml +++ b/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 diff --git a/database/data/functors/inclusion_ordinals.yaml b/database/data/functors/inclusion_ordinals.yaml new file mode 100644 index 00000000..2e7c9855 --- /dev/null +++ b/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. From b8f472d891a8a91045ad46621ff8f186655f19dc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 09:57:34 +0200 Subject: [PATCH 05/15] explicitly show when no property combinations are missing --- src/routes/missing/+page.svelte | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index 7bbe5334..834ecad2 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -92,14 +92,14 @@ {#each STRUCTURE_TYPES as type} {@const combinations = data.missing_combinations[type]} - {#if combinations.length > 0} -
-

Missing {type} combinations

+
+

Missing {type} combinations

+ {#if combinations.length}

- Among the consistent {type} combinations of the form p ∧ ¬q, the following - are not yet witnessed by a {type} in the database or its dual. If some of these - combinations are + Among the consistent {type} property combinations of the form p ∧ ¬q, + the following are not yet witnessed by a {type} in the database or its dual. + If some of these combinations are inconsistent, this indicates that some implication is missing.

@@ -119,8 +119,15 @@ {/each} -
- {/if} + {:else} +

+ Every consistent {type} property combination of the form p ∧ ¬q is witnessed + by a {type} in the database or its dual. 🎉 +

+ +

—

+ {/if} +
{/each} From dda2d3c054ce2ff3d48c76bd4a3366b65d0e96bc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 11:00:43 +0200 Subject: [PATCH 06/15] add the nerve functor Cat ---> sSet --- .cspell.json | 1 + database/data/functors/nerve.yaml | 44 +++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+) create mode 100644 database/data/functors/nerve.yaml diff --git a/.cspell.json b/.cspell.json index 0a105064..0b248b47 100644 --- a/.cspell.json +++ b/.cspell.json @@ -188,6 +188,7 @@ "Kashiwara", "Kategorien", "katex", + "Kerodon", "Kolmogorov", "Kunen", "Lawvere", diff --git a/database/data/functors/nerve.yaml b/database/data/functors/nerve.yaml new file mode 100644 index 00000000..5b045ed8 --- /dev/null +++ b/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 Kerodon/002Z. + + - 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 nLab. + + - 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 inner horn $\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. From 19ab2ba9b78963fb9d25d1a0cc66803a8a8649db Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 11:56:17 +0200 Subject: [PATCH 07/15] add result: reflectors preserve terminal objects --- database/data/functor-implications/adjoints.yaml | 8 ++++++++ database/data/functors/binary_coproduct_sets.yaml | 3 --- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index 0666b2e4..5fbc20ee 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/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 diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml index ab981434..e2866b18 100644 --- a/database/data/functors/binary_coproduct_sets.yaml +++ b/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.' From 22304582170d1c1e54cc1e25ac373833a5023ecb Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 19:54:01 +0200 Subject: [PATCH 08/15] =?UTF-8?q?add=20the=20Stone-=C4=8Cech=20compactific?= =?UTF-8?q?ation=20functor=20Top=20--->=20CompHaus?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .cspell.json | 6 ++- .../functors/stone-cech-compactification.yaml | 47 +++++++++++++++++++ 2 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 database/data/functors/stone-cech-compactification.yaml diff --git a/.cspell.json b/.cspell.json index 0b248b47..f8e93c63 100644 --- a/.cspell.json +++ b/.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", diff --git a/database/data/functors/stone-cech-compactification.yaml b/database/data/functors/stone-cech-compactification.yaml new file mode 100644 index 00000000..29c2ae86 --- /dev/null +++ b/database/data/functors/stone-cech-compactification.yaml @@ -0,0 +1,47 @@ +id: stone-cech-compactification +name: Stone-ÄŒech compactification functor +notation: $\beta$ +domain: Top +codomain: CompHaus +description: >- + This is the functor $\beta : \Top \to \CompHaus$ that is left adjoint to the inclusion functor $\CompHaus \hookrightarrow \Top$. There are various constructions (see Wikipedia), 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 nLab. + +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 nLab, 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}}$, see for example Theorem 3.1 at the nLab). + + 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: cofinitary + proof: >- + Let $S : \IN \to \IN$ be the successor map. In $\Top$, the limit of the sequence + $$\cdots \xrightarrow{S} \IN \xrightarrow{S} \IN$$ + is empty. Hence, $\beta$ of that limit is also empty. However, the limit of the sequence + $$\cdots \xrightarrow{\beta(S)} \beta(\IN) \xrightarrow{\beta(S)} \beta(\IN)$$ + in $\CompHaus$ is not empty by Lemma 1 here. + + - 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, Stone-ÄŒech compactifications of products, 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. From 6d5c48e5f01103aa9d0af6b326f803ab20f2b797 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 23:20:58 +0200 Subject: [PATCH 09/15] add the functor - x IQ : Top ---> Top --- .../data/functors/countable_copower_sets.yaml | 1 + database/data/functors/rational_product.yaml | 57 +++++++++++++++++++ 2 files changed, 58 insertions(+) create mode 100644 database/data/functors/rational_product.yaml diff --git a/database/data/functors/countable_copower_sets.yaml b/database/data/functors/countable_copower_sets.yaml index 4b4197de..bd01ca6c 100644 --- a/database/data/functors/countable_copower_sets.yaml +++ b/database/data/functors/countable_copower_sets.yaml @@ -14,6 +14,7 @@ related: - id_Set - binary_coproduct_sets - doubling_sets + - rational_product satisfied_properties: - property: preserves equalizers diff --git a/database/data/functors/rational_product.yaml b/database/data/functors/rational_product.yaml new file mode 100644 index 00000000..8cbce702 --- /dev/null +++ b/database/data/functors/rational_product.yaml @@ -0,0 +1,57 @@ +id: rational_product +name: rational product functor +notation: $- \times \IQ$ +domain: Top +codomain: Top +description: This functor maps a topological space $X$ to the topological space $X \times \IQ$, where $\IQ \subseteq \IR$ carries the usual topology. It is a typical example of a functor that preserves epimorphisms but not regular epimorphisms. +nlab_link: null +left_adjoint: null + +tags: + - topology + +related: + - countable_copower_sets + +satisfied_properties: + - property: cofinitary + proof: 'In any category $\C$ with binary products, for every object $Q$, the functor $- \times Q : \C \to \C$ preserves cofiltered limits. This is essentially because limits commute with limits.' + + - property: preserves equalizers + proof: 'In any category $\C$ with equalizers, for every object $Q$, the functor $- \times Q : \C \to \C$ preserves equalizers. This is essentially because limits commute with limits.' + + - property: preserves monomorphisms + proof: 'In any category $\C$, for every object $Q$, the functor $- \times Q : \C \to \C$ preserves monomorphisms. This is straightforward to check.' + + - property: preserves coproducts + proof: This is because $\Top$ is infinitary extensive. + + - property: dominant + proof: For every space $X$ there is a split monomorphism $X \hookrightarrow X \times \IQ$, $x \mapsto (x,0)$. + + - property: preserves epimorphisms + proof: 'Since $\Set$ is cartesian closed, the functor $- \times \IQ : \Set \to \Set$ is a left adjoint and therefore preserves epimorphisms (of course, a direct calculation is also possible). Since the forgetful functor $\Top \to \Set$ preserves binary products and preserves and reflects epimorphisms, it follows that $- \times \IQ : \Top \to \Top$ also preserves epimorphisms.' + + - property: conservative + proof: >- + Let $f : X \to Y$ be a continuous map such that $f \times \IQ$ is a homeomorphism. It follows immediately that $f$ is injective and surjective. It remains to show that $f^{-1} : Y \to X$ is continuous. This is because it can be written as the composition of continuous maps + $$Y \xrightarrow{0} Y \times \IQ \xrightarrow{(f \times \IQ)^{-1}} X \times \IQ \xrightarrow{p_1} X.$$ + +unsatisfied_properties: + - property: preserves terminal objects + proof: The one-point space is mapped to $\IQ$. + + - property: preserves binary products + proof: The canonical continuous map $(X \times Y) \times \IQ \to (X \times \IQ) \times (Y \times \IQ)$ sends an element $((x,y),q)$ to $((x,q),(y,q))$. It is clearly injective, but not surjective as soon as $X$ and $Y$ are non-empty. + + - property: essentially surjective + proof: If $X$ is a non-empty space, then $X \times \IQ$ is infinite. Thus, every non-empty finite space is not in the image. + + - property: finitary + proof: See MSE/1255678. + + - property: preserves regular epimorphisms + proof: 'Based on the description of regular epimorphisms as surjective quotient maps, this amounts to finding a surjective quotient map $p : X \to Y$ such that $p \times \IQ : X \times \IQ \to Y \times \IQ$ (which is certainly surjective) is not a quotient map. The standard example is the projection $p : \IR \to \IR / \IZ$ (where we identify $z \in \IZ$ with $z+1$); see MSE/2969372 for a proof.' + + - property: essentially injective + proof: By Sierpinski's theorem on metric spaces, there is a homeomorphism between $\IQ$ and the coproduct $\IQ \sqcup \IQ$. Alternatively, this can be deduced from Cantor's isomorphism theorem on dense linear orders. Thus, $1 \times \IQ \cong 2 \times \IQ$, but of course $1 \not\cong 2$, where $2 = 1 \sqcup 1$ is the discrete space with two points. From c2a6fade0218859d514e838cb9e3bb30de755a9b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 23:55:23 +0200 Subject: [PATCH 10/15] add the representable functor I ---> Set --- .../walking_morphism_representation.yaml | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 database/data/functors/walking_morphism_representation.yaml diff --git a/database/data/functors/walking_morphism_representation.yaml b/database/data/functors/walking_morphism_representation.yaml new file mode 100644 index 00000000..b146c41f --- /dev/null +++ b/database/data/functors/walking_morphism_representation.yaml @@ -0,0 +1,33 @@ +id: walking_morphism_representation +name: walking morphism representation +notation: $F$ +domain: walking_morphism +codomain: Set +description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{*\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms. +nlab_link: null +left_adjoint: null + +tags: + - category theory + +related: [] + +satisfied_properties: + - property: representable + proof: The functor is isomorphic to $\Hom(1,-)$, since $\Hom(1,0) = \varnothing$ and $\Hom(1,1) = \{\id_1\}$. + + - property: fully faithful + proof: This is easy to check. + + - property: preserves initial objects + proof: The functor maps $0 \mapsto \varnothing$. + + - property: finitary + proof: A direct proof is possible, but we can also use the representation of $I$ as the category of algebras for the finitary algebraic theory having just one equation $x=y$. Then the functor $I \to \Set$ is just its forgetful functor, and is therefore finitary. + +unsatisfied_properties: + - property: preserves epimorphisms + proof: The universal morphism $0 \to 1$ is an epimorphism in $I$ (simply because $I$ is thin), but its image $\varnothing \to \{*\}$ in $\Set$ is not an epimorphism. + + - property: dominant + proof: This is trivial. From b2d17bb738fd4e4a95bf79a54ef9734106b64df6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 00:38:36 +0200 Subject: [PATCH 11/15] add the idempotents functor Ring ---> Set --- database/data/functors/ring_idempotents.yaml | 42 ++++++++++++++++++++ database/data/macros.yaml | 1 + 2 files changed, 43 insertions(+) create mode 100644 database/data/functors/ring_idempotents.yaml diff --git a/database/data/functors/ring_idempotents.yaml b/database/data/functors/ring_idempotents.yaml new file mode 100644 index 00000000..bd70f7bc --- /dev/null +++ b/database/data/functors/ring_idempotents.yaml @@ -0,0 +1,42 @@ +id: ring_idempotents +name: ring idempotents functor +notation: $\Id$ +domain: Ring +codomain: Set +description: This functor sends a ring $R$ to its set $\Id(R)$ of idempotent elements. A ring homomorphism $R \to S$ restricts to a map $\Id(R) \to \Id(S)$. Among other things, it provides an example of a representable functor that does not preserve regular epimorphisms. +nlab_link: null +left_adjoint: null + +tags: + - algebra + +related: [] + +satisfied_properties: + - property: representable + proof: 'The functor is represented by the ring $\IZ[X] / \langle X^2 - X \rangle$.' + + - property: finitary + proof: This is immediate from the construction of filtered colimits in $\Ring$ and $\Set$. Alternatively, this follows from the fact that $\IZ[X] / \langle X^2 - X \rangle$ is a finitely presentable object, since it has a finite presentation in the algebraic theory of rings. + +unsatisfied_properties: + - property: faithful + proof: 'If $R$ is any integral domain, then $\Id(R) = \{0,1\}$ has exactly two elements, and if $f : R \to S$ is a homomorphism between integral domains, then the induced map on idempotents is $0 \mapsto 0$ and $1 \mapsto 1$, regardless of how $f$ is defined. Thus, for example, the two ring homomorphisms $\IZ[T] \rightrightarrows \IZ[T]$, $T \mapsto \pm T$, provide a counterexample.' + + - property: full + proof: 'We have $\Id(\IZ) = \{0,1\}$, and the constant map $0 : \{0,1\} \to \{0,1\}$ is not induced by a ring homomorphism $\IZ \to \IZ$ (which must be the identity anyway).' + + - property: essentially injective + proof: If $R$ is any integral domain, then $\Id(R) = \{0,1\}$ has exactly two elements. Thus, for example, $\Id(\IZ) \cong \Id(\IQ)$, while $\IZ \not\cong \IQ$. + + - property: dominant + proof: There is no ring $R$ with a split monomorphism $\varnothing \hookrightarrow \Id(R)$ since $\Id(R)$ is non-empty. (At least, for every set $X$ there is a ring $R$ with a monomorphism $X \hookrightarrow \Id(R)$.) + + - property: preserves initial objects + proof: The initial ring is $\IZ$, and its set of idempotent elements is $\{0,1\}$, which is not the empty set. + + - property: preserves binary coproducts + proof: The canonical map $\Id(\IZ) \sqcup \Id(\IZ) \to \Id(\IZ \sqcup \IZ)$, where $\sqcup$ denotes the coproduct in the respective categories, is not an isomorphism, since $\Id(\IZ \sqcup \IZ) = \Id(\IZ) = \{0,1\}$, while $\Id(\IZ) \sqcup \Id(\IZ) = \{0,1\} \sqcup \{0,1\}$ has four elements. + + - property: preserves regular epimorphisms + proof: 'The unique ring homomorphism $p : \IZ \to \IZ/6$ is surjective and therefore a regular epimorphism. However, the induced map $\Id(p) : \Id(\IZ) \to \Id(\IZ/6)$ is not surjective: We have $\Id(\IZ) = \{0,1\}$, while $\Id(\IZ/6) = \{0,1,3,4\}$.' diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 07245296..adbe93c1 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -63,6 +63,7 @@ \rank: \operatorname{rank} \Gal: \operatorname{Gal} \Alt: \operatorname{Alt} +\Id: \operatorname{Id} # categories \Set: \mathbf{Set} From 864002ba06e19a24f9ef90e647f4d44d1ed54b50 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 00:41:27 +0200 Subject: [PATCH 12/15] remove "early stage" notice for functors --- src/pages/StructureListPage.svelte | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/pages/StructureListPage.svelte b/src/pages/StructureListPage.svelte index 18200935..86ea64e5 100644 --- a/src/pages/StructureListPage.svelte +++ b/src/pages/StructureListPage.svelte @@ -34,15 +34,6 @@

List of {PLURALS[type]}

- {#if type === 'functor'} - -

- - The functor application is still in its early stages. More functors will be added - soon. -

- {/if} - {#if type === 'morphism'}

From acea4c2a680c303a9e3adfa2e53b98494586481a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 12:50:10 +0200 Subject: [PATCH 13/15] add the inclusion functor FinSet ---> Set --- content/inclusion-functors.md | 17 +++++++++++ database/data/functors/forget_finite.yaml | 35 +++++++++++++++++++++++ database/data/functors/id_Set.yaml | 1 + 3 files changed, 53 insertions(+) create mode 100644 content/inclusion-functors.md create mode 100644 database/data/functors/forget_finite.yaml diff --git a/content/inclusion-functors.md b/content/inclusion-functors.md new file mode 100644 index 00000000..56cf6500 --- /dev/null +++ b/content/inclusion-functors.md @@ -0,0 +1,17 @@ +--- +title: Inclusion functors +description: We gather results about inclusion functors +author: Martin Brandenburg +--- + +# Inclusion functors + +::: Lemma 1 +Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous. +::: + +_Proof._ Let $D : \I \to \C$ be a diagram such that $D$ has a colimit $(u_i : D(i) \to X)$ in $\C$ and $U \circ D$ has a colimit $(v_i : D(i) \to Y)$ in $\D$. There is a unique morphism $f : Y \to X$ such that $f \circ v_i = u_i$ for every $i \in \I$. Moreover, for every object $T \in \C$ the map of sets + +$$f^* : \Hom(X,T) \to \Hom(Y,T)$$ + +is a bijection; both sides identify with cones $D \to T$. Now apply this to $T := Q$ to conclude that $f$ is an isomorphism. $\square$ diff --git a/database/data/functors/forget_finite.yaml b/database/data/functors/forget_finite.yaml new file mode 100644 index 00000000..7b0752a2 --- /dev/null +++ b/database/data/functors/forget_finite.yaml @@ -0,0 +1,35 @@ +id: forget_finite +name: forgetful functor from finite sets to sets +notation: $U_{\FinSet,\Set}$ +domain: FinSet +codomain: Set +description: This functor is the inclusion functor $\FinSet \hookrightarrow \Set$ mapping a finite set to itself. It can also be regarded as a forgetful functor since it makes finite sets "forget" their finiteness. The functor is a basic example of a representable functor which is not a right adjoint. +nlab_link: null +left_adjoint: null + +tags: + - set theory + - forgetful + +related: + - id_Set + +satisfied_properties: + - property: fully faithful + proof: This is trivial. + + - property: representable + proof: It is represented by the singleton set. + + - property: cocontinuous + proof: This follows from Lemma 1 here since $\Set$ has an extremal cogenerator $\{0,1\}$ which is contained in $\FinSet$. + +unsatisfied_properties: + - property: left-invertible + proof: >- + Assume that there is a functor $F : \Set \to \FinSet$ such that $F(X) \cong X$ for every finite set $X$ (we won't even need naturality in $X$ to derive a contradiction). Let $S$ be any infinite set, such as $S = \IN$. Since $F(S)$ is a finite set, $n := \card(F(S))$ is a natural number. Since $S$ is infinite, there is a finite subset $X \subseteq S$ with $n+1$ elements. The inclusion map $X \hookrightarrow S$ is a split monomorphism. It follows that also $F(X) \hookrightarrow F(S)$ is a split monomorphism. But then + $$n = \card(F(S)) \geq \card(F(X)) = \card(X) = n+1$$ + is a contradiction. + + - property: dominant + proof: This is trivial. diff --git a/database/data/functors/id_Set.yaml b/database/data/functors/id_Set.yaml index 125ae365..607ae594 100644 --- a/database/data/functors/id_Set.yaml +++ b/database/data/functors/id_Set.yaml @@ -14,6 +14,7 @@ related: - squaring_sets - doubling_sets - diagonal_sets + - forget_finite satisfied_properties: - property: isomorphism From ed0279f490d893e952cc3c0d1112fa413be4e9f4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 13:36:55 +0200 Subject: [PATCH 14/15] add the inclusion functor 2 ---> I --- .../morphism_endpoints_inclusion.yaml | 40 +++++++++++++++++++ .../functors/span_endpoints_inclusion.yaml | 3 +- 2 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 database/data/functors/morphism_endpoints_inclusion.yaml diff --git a/database/data/functors/morphism_endpoints_inclusion.yaml b/database/data/functors/morphism_endpoints_inclusion.yaml new file mode 100644 index 00000000..0f7dee81 --- /dev/null +++ b/database/data/functors/morphism_endpoints_inclusion.yaml @@ -0,0 +1,40 @@ +id: morphism_endpoints_inclusion +name: morphism endpoints inclusion +notation: $E$ +domain: '2' +codomain: walking_morphism +description: This is the functor that embeds the discrete category $\{0,1\}$ into the walking morphism $\{0 \to 1\}$. It provides an example of a faithful functor that is full on isomorphisms but not full. +nlab_link: null +left_adjoint: null + +tags: + - category theory + +related: + - span_endpoints_inclusion + +satisfied_properties: + - property: full on isomorphisms + proof: This is trivial. + + - property: essentially surjective + proof: It is even bijective on objects. + + - property: continuous + proof: This follows from Lemma 2 here. + + - property: cocontinuous + proof: This follows from the dual of Lemma 2 here. + +unsatisfied_properties: + - property: left-invertible + proof: There are exactly two functors $\{0 \to 1\} \to \{0,1\}$, namely, the two constant functors $0,1$. Each of these does not provide a left inverse. + + - property: right-invertible + proof: There are exactly two functors $\{0 \to 1\} \to \{0,1\}$, namely, the two constant functors $0,1$. Each of these does not provide a right inverse. + + - property: right adjoint + proof: This follows from Corollary 4 here + + - property: left adjoint + proof: This follows from the dual of Corollary 4 here diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index a639f7d1..f4ad455e 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -10,7 +10,8 @@ left_adjoint: null tags: - category theory -related: [] +related: + - morphism_endpoints_inclusion satisfied_properties: - property: fully faithful From 45a8cb4c6452379ac7e9c681d926ad4707d1161d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 13:45:09 +0200 Subject: [PATCH 15/15] add implication: pseudomonic => conservative --- database/data/functor-implications/misc.yaml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 066f04cb..4a39ef92 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -71,6 +71,14 @@ proof: This holds by definition. is_equivalence: true +- id: pseudomonic_consequence + assumptions: + - pseudomonic + conclusions: + - conservative + proof: 'Let $F$ be a pseudomonic functor and let $f$ be a morphism in its domain such that $F(f)$ is an isomorphism. Then $F(f)^{-1} = F(g)$ for some isomorphism $g$ since $F$ is full on isomorphisms. Then $f \circ g$ and $g \circ f$ are identities since $F$ is faithful and their images are identities.' + is_equivalence: false + - id: essentially-surjective_implies_dominant assumptions: - essentially surjective