Add various inclusion functors

.cspell.json

@@ -171,6 +171,7 @@
 		"groupoid",
 		"groupoids",
 		"Haus",
+		"hausdorff",
 		"Hertweck",
 		"Heyting",
 		"homotopic",

database/data/functors/discrete_topology.yaml

@@ -3,7 +3,7 @@ name: discrete topology functor
 notation: $D$
 domain: Set
 codomain: Top
-description: This functor maps a set $X$ to the discrete topological space $D(X) \coloneqq (X, P(X))$ in which every subset is open.
+description: This functor maps a set $X$ to the discrete topological space $D(X) \coloneqq (X, P(X))$ in which every subset is open. It is a typical example of a fully faithful functor that preserves finite but does not preserve infinite products.
 nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology
 left_adjoint: null
 
@@ -15,24 +15,21 @@ related:
   - indiscrete_topology
 
 satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
   - property: left adjoint
     proof: 'This functor is left adjoint to the forgetful functor $U_{\Top} : \Top \to \Set$.'
 
-  - property: left-invertible
-    proof: The forgetful functor provides a left inverse.
-
-  - property: full
-    proof: This is trivial.
-
   - property: preserves finite products
     proof: It is easy to check that a finite product of discrete spaces is again discrete.
 
   - property: preserves equalizers
     proof: This follows since a subspace of a discrete space is again discrete.
 
 unsatisfied_properties:
-  - property: preserves products
-    proof: An infinite product of discrete spaces is usually not discrete, e.g. $\{0,1\}^{\IN}$.
-
   - property: dominant
     proof: A subspace of a discrete space is again discrete. Hence, if $Y$ is any non-discrete space such as $\IR$ with the Euclidean topology, there is no set $X$ with a regular (or even split) monomorphism $Y \hookrightarrow D(X)$.
+
+  - property: preserves products
+    proof: An infinite product of discrete spaces is usually not discrete, e.g. $\{0,1\}^{\IN}$.

database/data/functors/empty_sets.yaml

@@ -0,0 +1,34 @@
+id: empty_sets
+name: empty functor to the category of sets
+notation: $!_{\Set}$
+domain: '0'
+codomain: Set
+description: 'Every category $\C$ has a unique functor $!_{\C} : \varnothing \to \C$. Here, we specify $\C = \Set$, but most of the properties do not depend on the choice of $\C$, as long as $\C$ is non-empty. This is the simplest example of a functor to $\Set$ that is both continuous and cocontinuous, but is neither representable nor a left or right adjoint.'
+nlab_link: null
+left_adjoint: null
+
+tags:
+  - set theory
+
+related:
+  - trivial_sets
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: continuous
+    proof: 'For every category $\C$ the unique functor $!_{\C} : \varnothing \to \C$ is continuous, since no diagram in $\varnothing$ has a limit.'
+
+  - property: cocontinuous
+    proof: 'For every category $\C$ the unique functor $!_{\C} : \varnothing \to \C$ is cocontinuous, since no diagram in $\varnothing$ has a colimit.'
+
+unsatisfied_properties:
+  - property: left-invertible
+    proof: There is no functor $\Set \to \varnothing$ at all.
+
+  - property: dominant
+    proof: This is trivial.
+
+  - property: representable
+    proof: There cannot be any representing object.

database/data/functors/forget_abelian.yaml

@@ -15,17 +15,15 @@ related:
   - forget_group
   - forget_inverses
   - forget_torsion_free
+  - forget_commutative
 
 satisfied_properties:
-  - property: full
+  - property: fully faithful
     proof: This is trivial.
 
   - property: right adjoint
     proof: The abelianization functor $\Grp \to \Ab$, $G \mapsto G^{\ab}$ provides a left adjoint.
 
-  - property: left-invertible
-    proof: The abelianization functor $\Grp \to \Ab$, $G \mapsto G^{\ab}$ provides a left inverse.
-
   - property: preserves coequalizers
     proof: 'This follows from the concrete construction of coequalizers, but it can also be proven as follows: Assume that $f,g : A \rightrightarrows B$ have coequalizer $p : B \to C$ in $\Ab$. If $G$ is any group and $h : B \to G$ is a homomorphism with $hf = hg$, consider the image factorization $h = i h''$ of $h$. We have $h'' f = h'' g$, and the image $\im(h)$ is abelian. Hence, there is a unique homomorphism $k : C \to \im(h)$ with $kp = h''$. Hence, $ik : C \to G$ satisfies $ikp = h$. Uniqueness follows since we already know that the forgetful functor is preserves epimorphisms.'
 

database/data/functors/forget_commutative.yaml

@@ -0,0 +1,41 @@
+id: forget_commutative
+name: forgetful functor from commutative rings to rings
+notation: $U_{\CRing,\Ring}$
+domain: CRing
+codomain: Ring
+description: This is the inclusion functor $\CRing \hookrightarrow \Ring$ that maps a commutative ring to itself, regarded merely as a ring.
+nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
+left_adjoint: null # TODO: add the left adjoint to the database
+
+tags:
+  - algebra
+  - forgetful
+
+related:
+  - forget_abelian
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: right adjoint
+    proof: 'The functor $\Ring \to \CRing$, $R \mapsto R/\langle xy - yx : x,y \in R \rangle$ provides a left adjoint.'
+
+  - property: preserves initial objects
+    proof: In both categories, the ring $\IZ$ is initial.
+
+  - property: finitary
+    proof: 'Since the forgetful functor $U_{\Ring} : \Ring \to \Set$ is finitary and conservative, it suffices to prove that the composition $U_{\Ring} \circ U_{\CRing,\Ring} : \CRing \to \Set$ is finitary. This is just the forgetful functor $U_{\CRing} : \CRing \to \Set$ and is therefore finitary.'
+
+  - property: preserves coequalizers
+    proof: 'First of all, the functor preserves regular epimorphisms, since they are surjective homomorphisms in both categories. Now assume that $f,g : A \rightrightarrows B$ have coequalizer $p : B \to C$ in $\CRing$. If $T$ is any ring and $h : B \to T$ is a homomorphism with $hf = hg$, consider the image factorization $h = i h''$ of $h$. We have $h'' f = h'' g$, and the image $\im(h)$ is commutative. Hence, there is a unique homomorphism $k : C \to \im(h)$ with $kp = h''$. Hence, $ik : C \to G$ satisfies $ikp = h$. Uniqueness follows since we already know that the forgetful functor preserves regular epimorphisms.'
+
+  - property: preserves epimorphisms
+    proof: This is not formal. See <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a> for a proof.
+
+unsatisfied_properties:
+  - property: dominant
+    proof: This is trivial.
+
+  - property: preserves binary coproducts
+    proof: The coproduct of $\IZ[X]$ and $\IZ[Y]$ in $\CRing$ is the polynomial ring $\IZ[X,Y]$ in which $X,Y$ commute. Their coproduct in $\Ring$ is the non-commutative polynomial ring $\IZ\langle X,Y \rangle$ in which $X,Y$ do not commute.

database/data/functors/forget_finite.yaml

@@ -13,6 +13,7 @@ tags:
 
 related:
   - id_Set
+  - forget_finite_group
 
 satisfied_properties:
   - property: fully faithful

database/data/functors/forget_finite_abelian_group.yaml

@@ -0,0 +1,42 @@
+id: forget_finite_abelian_group
+name: forgetful functor from finite abelian groups to abelian groups
+notation: $U_{\FinAb, \Ab}$
+domain: FinAb
+codomain: Ab
+description: 'This is the inclusion functor $\FinAb \hookrightarrow \Ab$ that maps a finite abelian group to itself, regarded as an abelian group that has "forgotten" that it is finite. It provides an example of a fully faithful functor that is neither finitary nor cofinitary.'
+nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
+left_adjoint: null
+
+tags:
+  - algebra
+  - forgetful
+
+related:
+  - forget_finite_group
+  - forget_torsion
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: exact
+    proof: This follows from the construction of finite limits and colimits in $\FinAb$.
+
+  - property: preserves products
+    proof: The proof is identical to the proof that the <a href="/functor/forget_finite_group">inclusion functor $\FinGrp \hookrightarrow \Grp$</a> preserves products.
+
+  - property: preserves coproducts
+    proof: The proof is a minor variation of the proof that products are preserved, using the fact that finite coproducts and finite products coincide. Namely, one can show that a family of finite abelian groups has a coproduct in $\FinAb$ if and only if almost all groups are trivial.
+
+unsatisfied_properties:
+  - property: dominant
+    proof: This is trivial.
+
+  - property: finitary
+    proof: We can take the same counterexample as for the <a href="/functor/forget_finite_group">inclusion functor $\FinGrp \hookrightarrow \Grp$</a>, which only involves abelian groups.
+
+  - property: cofinitary
+    proof: We can take the same counterexample as for the <a href="/functor/forget_finite_group">inclusion functor $\FinGrp \hookrightarrow \Grp$</a>, which only involves abelian groups.
+
+  - property: left-invertible
+    proof: We can use the same proof as for the <a href="/functor/forget_finite_group">inclusion functor $\FinGrp \hookrightarrow \Grp$</a>.

database/data/functors/forget_finite_group.yaml

@@ -0,0 +1,67 @@
+id: forget_finite_group
+name: forgetful functor from finite groups to groups
+notation: $U_{\FinGrp, \Grp}$
+domain: FinGrp
+codomain: Grp
+description: 'This is the inclusion functor $\FinGrp \hookrightarrow \Grp$. It can also be viewed as a forgetful functor that forgets the property of being finite. Among other things, it provides an example of a fully faithful functor that is neither finitary nor cofinitary.'
+nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
+left_adjoint: null
+
+tags:
+  - algebra
+  - forgetful
+
+related:
+  - forget_group
+  - forget_finite
+  - forget_torsion
+  - forget_finite_abelian_group
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: left exact
+    proof: This follows from the construction of finite limits in $\FinGrp$.
+    check_redundancy: false
+
+  - property: preserves coequalizers
+    proof: This follows from the construction of coequalizers in $\FinGrp$.
+
+  - property: preserves products
+    proof: >-
+      It is sufficient to prove that if a family of finite groups $(G_i)_{i \in I}$ has a product $P$ in $\FinGrp$, then almost all $G_i$ are trivial; then the product reduces to a finite product, which is clearly preserved. Note that it is not enough to prove that the $\Grp$-product is infinite; this argument would be circular, since it assumes that the $\FinGrp$-product is equal to the $\Grp$-product.
+      Assume that there are infinitely many indices $i_1,i_2,\dotsc$ for which $G_{i_n}$ is non-trivial. Let $N \geq 1$. There is a canonical homomorphism $P \to \prod_{n=1}^{N} G_{i_n}$ to the finite product (which definitely exists), and by using trivial homomorphisms, we see that it is actually a split epimorphism. Therefore,
+      $$\textstyle\card(P) \geq \prod_{i=1}^{N} \card(G_{i_n}) \geq \prod_{i=1}^{N} 2 = 2^N.$$
+      Since this holds for all $N$, we obtain a contradiction to the finiteness of $P$.
+
+  - property: preserves coproducts
+    proof: >-
+      It is sufficient to prove that if a family of finite groups $(G_i)_{i \in I}$ has a coproduct $C$ in $\FinGrp$, then at most one $G_j$ is non-trivial; then the coproduct is simply $G_j$, and it is clearly preserved. Note that it is not enough to prove that the $\Grp$-coproduct is infinite; this argument would be circular, since it assumes that the $\FinGrp$-coproduct is equal to the $\Grp$-coproduct.
+      Let $\coprod_{i \in I} G_i$ denote the coproduct of $(G_i)_{i \in I}$ in $\Grp$, which can be constructed as the free product. Assume that two groups in the family are non-trivial, say $G_0$ and $G_1$ for some indices $0,1 \in I$.
+      We claim that the canonical homomorphism $G_0 \sqcup G_1 \to C$ is a monomorphism. If $x$ is a non-trivial element in the free product $G_0 \sqcup G_1$, which is well-known to be residually finite, there is some finite group $H$ and a homomorphism $\varphi : G_0 \sqcup G_1 \to H$ with $\varphi(x) \neq 1$. The homomorphism $\varphi$ corresponds to two homomorphisms $\varphi_0 : G_0 \to H$ and $\varphi_1 : G_1 \to H$. For all $i \neq 0,1$, let $\varphi_i : G_i \to H$ be the trivial homomorphism. The universal property of $C$ yields a unique homomorphism $\psi : C \to H$ that extends each $\varphi_i$. It maps the image of $x$ in $C$ to $\varphi(x) \neq 1$, so that this image is non-trivial, as claimed.
+      However, $G_0 \sqcup G_1$ is an infinite group (which can be seen from the usual element description of a free product), so it cannot embed into the finite group $C$. This contradiction finishes the proof.
+
+unsatisfied_properties:
+  - property: dominant
+    proof: This is trivial.
+
+  - property: left-invertible
+    proof: 'Assume that there is a functor $F : \Grp \to \FinGrp$ with natural isomorphisms $F(G) \cong G$ for finite groups $G$. Consider the group $A := F(\prod_{n \geq 1} \IZ/n)$. For every $n \geq 1$ there is a split monomorphism from $\IZ/n$ to $\prod_{n \geq 1} \IZ/n$. It induces a split monomorphism from $F(\IZ/n) \cong \IZ/n$ to $A$, so that $\card(A) \geq n$. But then $A$ cannot be finite.'
+
+  - property: finitary
+    proof: >-
+      Let $Q$ be any non-trivial abelian divisible torsion group, such as $Q = \IQ / \IZ$. Let $\I$ be the poset of finite subgroups of $Q$ and let $D : \I \to \FinGrp$ be the diagram $D(A)=A$. Of course, the colimit of $U \circ D : \I \to \Grp$ is $Q$, where $U : \FinGrp \hookrightarrow \Grp$ is the inclusion functor. However, it turns out that the colimit of $D$ also exists and is the trivial group $1$. To prove this, let $G$ be any finite group. Then we compute:
+      $$\Hom(D,\Delta(G)) \cong \Hom(U \circ D, \Delta(U(G))) \cong \Hom(Q,U(G))$$
+      But every homomorphism $Q \to U(G)$ is trivial because its image is a finite divisible abelian group. Thus, $\Hom(Q,U(G)) \cong \Hom(1,G)$, proving that $1$ is a colimit of $D$. This shows that the colimit of $D$ is not preserved by $U$.
+
+      For example, when $Q = \IQ / \IZ$, the diagram is isomorphic to $(\IN_{>0},\mid)^{\op} \to \FinGrp$, mapping $n$ to the cyclic group $\IZ/n$, and its (trivial) colimit is not preserved by $U$.
+
+  - property: cofinitary
+    proof: >-
+      Let $p$ be a prime, and consider the sequence of projection homomorphisms
+      $$\cdots \to \IZ/p^3 \to \IZ/p^2 \to \IZ/p.$$
+      Its limit in $\Grp$ is the additive group $\IZ_p$ of $p$-adic integers. However, its limit in $\FinGrp$ exists and is the trivial group. This is because a cone in $\FinGrp$ over that sequence with vertex $G \in \FinGrp$ can be identified with a homomorphism $G \to \IZ_p$ in $\Grp$, which must be trivial since its image is a finite torsion-free group.
+
+  - property: right exact
+    proof: See <a href="https://mathoverflow.net/questions/513646" target="_blank">MO/513646</a>.

database/data/functors/forget_group.yaml

@@ -16,6 +16,7 @@ related:
   - forget_ring
   - forget_abelian
   - forget_group_pointed
+  - forget_finite_group
 
 satisfied_properties:
   - property: representable

database/data/functors/forget_hausdorff.yaml

@@ -0,0 +1,38 @@
+id: forget_hausdorff
+name: forgetful functor from Hausdorff spaces to topological spaces
+notation: $U_{\Haus,\Top}$
+domain: Haus
+codomain: Top
+description: This is the inclusion functor $\Haus \hookrightarrow \Top$ that maps a Hausdorff space to itself. It can also be viewed as a forgetful functor, since Hausdorff spaces "forget" that they are Hausdorff.
+nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
+left_adjoint: null # TODO: add the Hausdorff reflection functor
+
+tags:
+  - topology
+  - forgetful
+
+related:
+  - forget_topology
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: right adjoint
+    proof: The Hausdorff reflection (see <a href="https://ncatlab.org/nlab/show/Hausdorff+space#HausdorffReflectionViaHomsIntoAllHausdorffSpaces" target="_blank">nLab</a>) provides a left adjoint $\Top \to \Haus$.
+
+  - property: preserves coproducts
+    proof: This follows easily from the elementary fact that the $\Top$-coproduct of a family of Hausdorff spaces is again Hausdorff.
+
+  - property: preserves regular epimorphisms
+    proof: This follows from the classifications of regular epimorphisms in $\Haus$ and $\Top$; in both cases, they are surjective quotient maps.
+
+unsatisfied_properties:
+  - property: preserves epimorphisms
+    proof: The inclusion $\IQ \hookrightarrow \IR$ is an epimorphism in $\Haus$ (since it has dense image), but not an epimorphism in $\Top$ (since it is not surjective).
+
+  - property: dominant
+    proof: A subspace of a Hausdorff space is again Hausdorff, and not every space is Hausdorff.
+
+  - property: finitary
+    proof: The inclusion functor certainly preserves monomorphisms, and in fact all limits. We know that monomorphisms in <a href="/category/Top">$\Haus$</a> are not stable under filtered colimits, whereas they are in <a href="/category/Top">$\Top$</a>. Thus, the claim follows from Lemma 2 <a href="/content/subcategories">here</a>.

database/data/functors/forget_inverses.yaml

@@ -18,7 +18,7 @@ related:
   - forget_torsion_free
 
 satisfied_properties:
-  - property: full
+  - property: fully faithful
     proof: It is a standard fact from group theory that a multiplicative map already preserves inverses.
 
   - property: right adjoint
@@ -27,9 +27,6 @@ satisfied_properties:
   - property: left adjoint
     proof: 'This functor is left adjoint to the functor $(-)^{\times} : \Mon \to \Grp$ that sends a monoid $M$ to its group of units $M^{\times} \coloneqq \{(a,b) \in M^2 : ab = ba = 1 \}$. In fact, if $M$ is a monoid and $G$ is a group, there is a bijection $\Hom(U_{\Grp,\Mon}(G),M) \to \Hom(G,M^{\times})$ given by mapping $\varphi$ to $g \mapsto (\varphi(g),\varphi(g^{-1}))$.'
 
-  - property: left-invertible
-    proof: 'The group of units functor $(-)^{\times} : \Mon \to \Grp$ provides a left inverse.'
-
 unsatisfied_properties:
   - property: dominant
     proof: Every submonoid of a group is cancellative. Thus, if $M$ is a non-cancellative monoid such as $(\IN,\cdot,1)$, there cannot be a group $G$ with a (split) monomorphism $M \hookrightarrow G$.

database/data/functors/forget_torsion.yaml

@@ -0,0 +1,34 @@
+id: forget_torsion
+name: forgetful functor from torsion abelian groups to abelian groups
+notation: $U_{\TorsAb, \Ab}$
+domain: TorsAb
+codomain: Ab
+description: 'This is the inclusion functor $\TorsAb \hookrightarrow \Ab$. It can also be viewed as a forgetful functor that forgets the property of being torsion. It is a typical example of a fully faithful functor that preserves finite products but does not preserve infinite products.'
+nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
+left_adjoint: null # we only have the torsion functor Ab -> Ab in the database, not Ab -> TorsAb
+
+tags:
+  - algebra
+  - forgetful
+
+related:
+  - forget_abelian
+  - forget_finite_abelian_group
+  - forget_torsion_free
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: left exact
+    proof: This follows from the construction of finite limits in $\TorsAb$.
+
+  - property: left adjoint
+    proof: 'This functor is left adjoint to the torsion subgroup functor $T : \Ab \to \TorsAb$, since for every torsion abelian group $A$ and every abelian group $B$, every homomorphism $A \to B$ restricts to a homomorphism $A \to T(B)$.'
+
+unsatisfied_properties:
+  - property: dominant
+    proof: This is trivial.
+
+  - property: preserves products
+    proof: The product of the family $(\IZ/n)_{n \geq 1}$ in $\TorsAb$ is $T(\prod_{n \geq 1} \IZ/n)$, where $T(-)$ denotes the torsion subgroup and $\prod$ denotes the usual product in $\Ab$. This is not equal to $\prod_{n \geq 1} \IZ/n$ since, for example, $([1],[1],\dotsc)$ is not a torsion element.

database/data/functors/forget_torsion_free.yaml

@@ -1,5 +1,5 @@
 id: forget_torsion_free
-name: forgetful functor from torsion-free abelian groups
+name: forgetful functor from torsion-free abelian groups to abelian groups
 notation: $U_{\TorsFreeAb, \Ab}$
 domain: TorsFreeAb
 codomain: Ab
@@ -14,6 +14,7 @@ tags:
 related:
   - forget_abelian
   - forget_inverses
+  - forget_torsion
 
 satisfied_properties:
   - property: fully faithful