diff --git a/.cspell.json b/.cspell.json index 0a105064..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", @@ -188,6 +192,7 @@ "Kashiwara", "Kategorien", "katex", + "Kerodon", "Kolmogorov", "Kunen", "Lawvere", 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/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/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/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/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.' 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. 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. 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. diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index 95ede225..a639f7d1 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -23,14 +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.' - - - 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/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. 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}