Add more examples of functors to witness property combinations

.cspell.json

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

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. <span class="qed">$\square$</span>

database/data/categories/N_oo.yaml

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

database/data/functor-implications/adjoints.yaml

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

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

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

database/data/functor-implications/misc.yaml

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

database/data/functor-implications/monadic.yaml

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

database/data/functors/binary_coproduct_sets.yaml

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

database/data/functors/countable_copower_sets.yaml

@@ -14,6 +14,7 @@ related:
   - id_Set
   - binary_coproduct_sets
   - doubling_sets
+  - rational_product
 
 satisfied_properties:
   - property: preserves equalizers

database/data/functors/forget_abelian.yaml

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

database/data/functors/forget_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 <a href="/content/inclusion-functors">here</a> since <a href="/category/Set">$\Set$</a> 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.

database/data/functors/forget_inverses.yaml

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

database/data/functors/forget_torsion_free.yaml

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

database/data/functors/id_Set.yaml

@@ -14,6 +14,7 @@ related:
   - squaring_sets
   - doubling_sets
   - diagonal_sets
+  - forget_finite
 
 satisfied_properties:
   - property: isomorphism

database/data/functors/inclusion_ordinals.yaml

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

database/data/functors/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 <a href="/content/functors_on_discrete_categories">here</a>.
+
+  - property: cocontinuous
+    proof: This follows from the dual of Lemma 2 <a href="/content/functors_on_discrete_categories">here</a>.
+
+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 <a href="/content/functors_on_discrete_categories">here</a>
+
+  - property: left adjoint
+    proof: This follows from the dual of Corollary 4 <a href="/content/functors_on_discrete_categories">here</a>

database/data/functors/nerve.yaml

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