From e49cd748aef8f405de209fea9aed2dc6c121a771 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 20:48:46 +0200 Subject: [PATCH 01/18] 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 70c022267866f66827618c1b4825cff9ebc790b6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 21:09:22 +0200 Subject: [PATCH 02/18] 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 290da5d7fc2a32293153127be173bb9d30e05e95 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 22:39:17 +0200 Subject: [PATCH 03/18] 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 9804cd0f..71d31cd5 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -159,3 +159,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 e3f58401876e712192593d4ea1da1d1ea39866df Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 22 Jul 2026 22:39:33 +0200 Subject: [PATCH 04/18] 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 ecd3999c..97cf0733 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 45f4acbdafcf5f403ca6fc9478c7f8c6e4b6f82f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 09:57:34 +0200 Subject: [PATCH 05/18] 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 cf19ee1d7f26d3b3bbf51d327229a58e527a7f6d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 11:00:43 +0200 Subject: [PATCH 06/18] 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 993abc8866592b4457f8792761c39f981623008f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 11:56:17 +0200 Subject: [PATCH 07/18] 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 77f29374374851aa16e482128d86554aa460895f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 19:54:01 +0200 Subject: [PATCH 08/18] =?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 33b8903b7f5d3f0ae82e4ba9ebc605b5374920e4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 23:20:58 +0200 Subject: [PATCH 09/18] 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 0b7aac1e03ee89c107f53d18e3b7f400277364bf Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Jul 2026 23:55:23 +0200 Subject: [PATCH 10/18] 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 cd2a6e103f30fd1341cffb838d1f5462e6ac934b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 00:38:36 +0200 Subject: [PATCH 11/18] 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 f88bfaf0..9a8600f8 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -65,6 +65,7 @@ \Gal: \operatorname{Gal} \Alt: \operatorname{Alt} \Open: \operatorname{Open} +\Id: \operatorname{Id} # categories \Set: \mathbf{Set} From 33615a4b13dca77d19045e4abb2ad1c49e64b5bc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 00:41:27 +0200 Subject: [PATCH 12/18] 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 ba3358fb89126b16dcdf7ddaf0f6531a0310c676 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 12:50:10 +0200 Subject: [PATCH 13/18] 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 14713192b4c3f0dfc1137066935d505974fc5049 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 13:36:55 +0200 Subject: [PATCH 14/18] 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 d0c882ff1a3aeb6831ce0dd451cf002369869175 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 24 Jul 2026 13:45:09 +0200 Subject: [PATCH 15/18] 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 71d31cd5..7ae06713 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -83,6 +83,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 From 07b886a03b9055f51fcfa47a000374c682d45ede Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 25 Jul 2026 11:10:00 +0200 Subject: [PATCH 16/18] add the Brauer group functor Fld ---> Ab --- .cspell.json | 3 ++ database/data/categories/Fld.yaml | 2 +- .../limits preservation.yaml | 11 ++++ database/data/functors/brauer_group.yaml | 53 +++++++++++++++++++ database/data/macros.yaml | 1 + 5 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 database/data/functors/brauer_group.yaml diff --git a/.cspell.json b/.cspell.json index f8e93c63..40fd51a8 100644 --- a/.cspell.json +++ b/.cspell.json @@ -43,6 +43,7 @@ "Birkhoff", "Bogachev", "Borel", + "brauer", "Bredon", "cancellative", "cartesian", @@ -155,6 +156,7 @@ "foundedness", "freyd", "Freyd", + "Frobenius", "functor", "functorial", "functors", @@ -227,6 +229,7 @@ "nilradical", "nlab", "Noetherian", + "Noncommutative", "objectwise", "pointwise", "Pontryagin", diff --git a/database/data/categories/Fld.yaml b/database/data/categories/Fld.yaml index 4795866c..946d2732 100644 --- a/database/data/categories/Fld.yaml +++ b/database/data/categories/Fld.yaml @@ -81,5 +81,5 @@ special_morphisms: description: purely inseparable homomorphisms proof: See MSE/687869. regular monomorphisms: - description: A Galois extension is a regular monomorphism iff it is procyclic, and the general case can be reduced to this situation; see the reference for details. + description: A Galois extension is a regular monomorphism iff it is procyclic, and the general case can be reduced to this situation; see MSE/5129895 for details. proof: See MSE/5129895. diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index d92ac8f9..37167108 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/database/data/functor-implications/limits preservation.yaml @@ -224,6 +224,17 @@ proof: This is trivial. is_equivalence: false +- id: trivial_coreflexive_equalizer_preservation + # TODO: rework this once we add "split-epi-trivial" + assumptions: [] + mapped_assumptions: + domain: + - regular-quotient-trivial + conclusions: + - preserves coreflexive equalizers + proof: 'Let $f,g : X \rightrightarrows Y$ be a coreflexive pair, i.e. there is a morphism $r : Y \to X$ with $rf = rg = \id_X$. Then $r$ is a split and hence regular epimorphism. Thus, $r$ is an isomorphism. But then $f=g$, and $\id_Y$ is an equalizer of $f,g$. This equalizers is obviously preserved.' + is_equivalence: false + - id: thin_binary_product_preservation assumptions: [] mapped_assumptions: diff --git a/database/data/functors/brauer_group.yaml b/database/data/functors/brauer_group.yaml new file mode 100644 index 00000000..a246a578 --- /dev/null +++ b/database/data/functors/brauer_group.yaml @@ -0,0 +1,53 @@ +id: brauer_group +name: Brauer group functor +notation: $\Br$ +domain: Fld +codomain: Ab +description: The Brauer group $\Br(K)$ of a field $K$ consists of equivalence classes of central simple algebras over $K$, where $A \sim B$ iff $A \otimes_K M_n(K) \cong B \otimes_K M_n(K)$ for some $n \geq 0$. The group structure is given by $[A] \cdot [B] := [A \otimes_K B]$ and $[A]^{-1} := [A^{\op}]$. A homomorphism $K \to L$ induces the homomorphism $\Br(K) \to \Br(L)$ defined by $[A] \mapsto [A \otimes_K L]$. For details, see e.g. Chapter 4 in Noncommutative Algebra by Farb-Dennis. +nlab_link: https://ncatlab.org/nlab/show/Brauer+group +left_adjoint: null + +tags: + - algebra + +related: [] + +comments: + - 'For the image of the functor $\Br : \Fld \to \Ab$, see MO/130778.' + +satisfied_properties: + - property: preserves terminal objects + # TODO: automate the + proof: This is trivial since $\Fld$ has no terminal object. + + - property: preserves initial objects + # TODO: automate the + proof: This is trivial since $\Fld$ has no initial object. + +unsatisfied_properties: + - property: essentially injective + proof: The Brauer group of any algebraically closed field is trivial. A reference is Noncommutative Algebra by Farb-Dennis, the examples after Proposition 4.3. + + - property: faithful + proof: The identity $\IC \to \IC$ and the complex conjugation $\IC \to \IC$ are mapped to the same endomorphism of $\Br(\IC)$ because $\Br(\IC)$ is trivial. + + - property: conservative + proof: Take any proper embedding of two algebraically closed fields, for example $\overline{\IQ} \hookrightarrow \IC$. It is mapped to an isomorphism since the Brauer group of an algebraically closed field is trivial. + + - property: full + proof: The group $\Br(\IR)$ is cyclic of order $2$ (generated by the quaternion algebra) by Frobenius' theorem on real division algebras; a reference is Noncommutative Algebra by Farb-Dennis, the examples after Proposition 4.3. In particular, there are two homomorphisms of groups $\Br(\IR) \to \Br(\IR)$. But it is well-known that there is only one homomorphism of fields $\IR \to \IR$, the identity (MSE/449404). + + - property: preserves regular monomorphisms + proof: The embedding $\IR \hookrightarrow \IC$ is a regular monomorphism in $\Fld$ as it is the equalizer of the identity and the complex conjugation on $\IC$. However, the induced homomorphism $\Br(\IR) \to \Br(\IC)$ is not injective since $\Br(\IC)$ is trivial and $\Br(\IR)$ is cyclic of order $2$. + + - property: dominant + proof: This is because the Brauer group of a field is always a torsion group, see Corollary 4.15 in Noncommutative Algebra by Farb-Dennis. + + - property: preserves binary products + proof: >- + A functor preserving binary products also preserves subterminal objects. In $\Fld$, the field $\IQ$ is subterminal. However, $\Br(\IQ)$ is not subterminal in $\Ab$, since otherwise it would be trivial, which is not the case. In fact, the rational quaternion algebra + $$H(\IQ) = \langle i,j : i^2=j^2=-1, ij=-ji \rangle_{\IQ}$$ + is a non-trivial central finite-dimensional division algebra over $\mathbb{Q}$, and more precisely, $\Br(\IQ)$ is an infinite abelian group. See for example Exercise 4 in Section 12.5 in Associative Algebras by Pierce. + + - property: preserves binary coproducts + proof: If $K$ is any field of characteristic $0$, then $K \sqcup \IQ = K$ in $\Fld$. More precisely, the cospan $\IQ \rightarrow K \leftarrow K$ is a coproduct, where the map on the right is the identity. However, the cospan $\Br(\IQ) \rightarrow \Br(K) \leftarrow \Br(K)$ is not a coproduct, since otherwise $\Br(\IQ)$ would be trivial. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 9a8600f8..bcb0b582 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -66,6 +66,7 @@ \Alt: \operatorname{Alt} \Open: \operatorname{Open} \Id: \operatorname{Id} +\Br: \operatorname{Br} # categories \Set: \mathbf{Set} From 4638ff6e45c79989bc0b68cfe2d2a6a9c811bfe5 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 25 Jul 2026 11:48:55 +0200 Subject: [PATCH 17/18] update end-to-end tests on missing data --- tests/missing.spec.ts | 40 +++++++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 15 deletions(-) diff --git a/tests/missing.spec.ts b/tests/missing.spec.ts index c9fed2ca..400c819e 100644 --- a/tests/missing.spec.ts +++ b/tests/missing.spec.ts @@ -20,8 +20,7 @@ test('user can navigate to the page with missing data', async ({ page }) => { await expect(page).toHaveURL('/missing') }) -// this can be adjusted if at some point in the future everything is known, -// but that is unlikely +// this can be adjusted if at some point all categories are understood test('user can see categories with missing data', async ({ page }) => { await page.goto('/missing', { waitUntil: 'networkidle' }) @@ -47,9 +46,8 @@ test('user can see categories with missing data', async ({ page }) => { await page.waitForURL('/category/*') }) -// this can be adjusted if at some point in the future a functor -// is not fully understood anymore -test('user can see no functors with missing data', async ({ page }) => { +// this can be adjusted if at some point all functors are understood +test('user can see one functor with missing data', async ({ page }) => { await page.goto('/missing', { waitUntil: 'networkidle' }) await expect( @@ -63,11 +61,10 @@ test('user can see no functors with missing data', async ({ page }) => { hasText: 'Functors with unknown properties' }) - await expect(functors_section.getByRole('link')).toHaveCount(0) + await expect(functors_section.getByRole('link')).toHaveCount(1) }) -// this can be adjusted if at some point in the future a morphism -// is not fully understood anymore +// this can be adjusted if at some point not all morphisms are understood test('user can see no morphisms with missing data', async ({ page }) => { await page.goto('/missing', { waitUntil: 'networkidle' }) @@ -85,6 +82,7 @@ test('user can see no morphisms with missing data', async ({ page }) => { await expect(morphisms_section.getByRole('link')).toHaveCount(0) }) +// this can be adjusted if at some point every category combination is witnessed test('user can see missing category combinations', async ({ page }) => { await page.goto('/missing', { waitUntil: 'networkidle' }) @@ -103,7 +101,8 @@ test('user can see missing category combinations', async ({ page }) => { ).toBeVisible() }) -test('user can see missing functor combinations', async ({ page }) => { +// this can be adjusted if at some point a functor combination is not witnessed +test('user cannot see any missing functor combinations', async ({ page }) => { await page.goto('/missing', { waitUntil: 'networkidle' }) const combinations_section = page.locator('section', { @@ -112,11 +111,22 @@ test('user can see missing functor combinations', async ({ page }) => { await expect(combinations_section).toBeVisible() - await combinations_section - .locator('summary', { hasText: /Show all \d+ combinations/ }) - .click() + await expect(combinations_section).toHaveText( + /.+Every consistent functor property combination.+is witnessed/ + ) +}) - await expect( - combinations_section.locator('li', { hasText: /[A-Za-z]+ ∧ ¬[A-Za-z]+/ }).first() - ).toBeVisible() +// this can be adjusted if at some point a morphism combination is not witnessed +test('user cannot see any missing morphism combinations', async ({ page }) => { + await page.goto('/missing', { waitUntil: 'networkidle' }) + + const combinations_section = page.locator('section', { + hasText: 'Missing morphism combinations' + }) + + await expect(combinations_section).toBeVisible() + + await expect(combinations_section).toHaveText( + /.+Every consistent morphism property combination.+is witnessed/ + ) }) From 559149a6df37066d0c7fbb0eb3f0436e7517d1e9 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 25 Jul 2026 12:56:17 +0200 Subject: [PATCH 18/18] Br is finitary --- database/data/functors/brauer_group.yaml | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/database/data/functors/brauer_group.yaml b/database/data/functors/brauer_group.yaml index a246a578..436b9734 100644 --- a/database/data/functors/brauer_group.yaml +++ b/database/data/functors/brauer_group.yaml @@ -3,7 +3,7 @@ name: Brauer group functor notation: $\Br$ domain: Fld codomain: Ab -description: The Brauer group $\Br(K)$ of a field $K$ consists of equivalence classes of central simple algebras over $K$, where $A \sim B$ iff $A \otimes_K M_n(K) \cong B \otimes_K M_n(K)$ for some $n \geq 0$. The group structure is given by $[A] \cdot [B] := [A \otimes_K B]$ and $[A]^{-1} := [A^{\op}]$. A homomorphism $K \to L$ induces the homomorphism $\Br(K) \to \Br(L)$ defined by $[A] \mapsto [A \otimes_K L]$. For details, see e.g. Chapter 4 in Noncommutative Algebra by Farb-Dennis. +description: The Brauer group $\Br(K)$ of a field $K$ consists of equivalence classes of central simple algebras over $K$, where $A \sim B$ iff $A \otimes_K M_n(K) \cong B \otimes_K M_n(K)$ for some $n \geq 0$. The group structure is given by $[A] \cdot [B] := [A \otimes_K B]$, $1 := [K]$ and $[A]^{-1} := [A^{\op}]$. A homomorphism $K \to L$ induces the homomorphism $\Br(K) \to \Br(L)$ defined by $[A] \mapsto [A \otimes_K L]$. For details, see e.g. Chapter 4 in Noncommutative Algebra by Farb-Dennis. nlab_link: https://ncatlab.org/nlab/show/Brauer+group left_adjoint: null @@ -17,13 +17,31 @@ comments: satisfied_properties: - property: preserves terminal objects - # TODO: automate the + # TODO: automate this proof: This is trivial since $\Fld$ has no terminal object. - property: preserves initial objects - # TODO: automate the + # TODO: automate this proof: This is trivial since $\Fld$ has no initial object. + - property: finitary + proof: >- + Let $F = \colim_i F_i$ be a filtered colimit of fields. We first show that the canonical map + $$\alpha : \colim_i \Br(F_i) \to \Br(F)$$ + is surjective. Let $A$ be a central simple algebra over $F$. Since it finite-dimensional, it has a finite presentation over $F$. The relations are non-commutative polynomials in $F$, thus have coefficients in some $F_i$ (more precisely, the image of $F_i \to F$ in $F$). We may therefore lift this presentation to $F_i$ and find an algebra $A_i$ over $F_i$ with an isomorphism $A_i \otimes_{F_i} F \cong A$. We need to show that $A_i$ is a central simple algebra. First, we have $A_i \neq 0$ and $\dim_{F_i}(A_i) = \dim_F(A) < \infty$. If $x \in Z(A_i)$, then $x \otimes 1 \in Z(A_i \otimes_{F_i} F) = F$. From linear algebra we know that the intersection of $A_i$ and $F$ in $A_i \otimes_{F_i} F$ is $F_i$, so that $x \in F_i$, as claimed. Finally, to show that $A_i$ is simple, let $I$ be a two-sided ideal in $A_i$. Then $I \otimes_{F_i} F$ is a two-sided ideal in the tensor product. Thus, it is either zero, which also gives $I=0$ by linear algebra, or it is $A_i \otimes_{F_i} F$, which gives $I=A_i$ by linear algebra. Therefore, $[A_i]$ is a well-defined preimage of $[A]$ in $\Br(F_i)$. + + To show that the canonical map $\alpha$ is injective, choose an element in its kernel. It is induced by an element in some $\Br(F_i)$, say $[A]$ for a central simple algebra $A$ over $F_i$. Then $[A \otimes_{F_i} F] = 1$ in $\Br(F)$ means that there is some $n \geq 0$ such that + $$A \otimes_{F_i} M_n(F) \cong A \otimes_{F_i} F \otimes_F M_n(F) \cong M_n(F)$$ + as $F$-algebras. Since $M_n(F) = M_n(F_i) \otimes_{F_i} F$, this means that + $$(A \otimes_{F_i} M_n(F_i)) \otimes_{F_i} F \cong M_n(F_i) \otimes_{F_i} F.$$ + In general, if $R,S$ are two finitely presentable $F_i$-algebras with an isomorphism of $F$-algebras + $$R \otimes_{F_i} F \cong S \otimes_{F_i} F,$$ + then there is some $i \to j$ such that this isomorphism is induced by an isomorphism of $F_j$-algebras + $$R \otimes_{F_i} F_j \cong S \otimes_{F_i} F_j;$$ + this is easily checked by using the finite presentations and $F = \colim_i F_i$. Therefore, in our case, there is some $i \to j$ and an isomorphism between + $$(A \otimes_{F_i} M_n(F_i)) \otimes_{F_i} F_j \cong (A \otimes_{F_i} F_j) \otimes_{F_j} M_n(F_j)$$ + and $M_n(F_i) \otimes_{F_i} F_j \cong M_n(F_j)$. In other words, $[A]$ is contained in the kernel of $\Br(F_i) \to \Br(F_j)$, which means that it vanishes in the colimit, as claimed. + unsatisfied_properties: - property: essentially injective proof: The Brauer group of any algebraically closed field is trivial. A reference is Noncommutative Algebra by Farb-Dennis, the examples after Proposition 4.3.