diff --git a/.cspell.json b/.cspell.json index 8243dcf5..488347a3 100644 --- a/.cspell.json +++ b/.cspell.json @@ -171,6 +171,7 @@ "groupoid", "groupoids", "Haus", + "hausdorff", "Hertweck", "Heyting", "homotopic", diff --git a/database/data/functors/discrete_topology.yaml b/database/data/functors/discrete_topology.yaml index d5507103..39826026 100644 --- a/database/data/functors/discrete_topology.yaml +++ b/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,15 +15,12 @@ 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. @@ -31,8 +28,8 @@ satisfied_properties: 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}$. diff --git a/database/data/functors/empty_sets.yaml b/database/data/functors/empty_sets.yaml new file mode 100644 index 00000000..b6cbaddf --- /dev/null +++ b/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. diff --git a/database/data/functors/forget_abelian.yaml b/database/data/functors/forget_abelian.yaml index 4a047451..b4d36e89 100644 --- a/database/data/functors/forget_abelian.yaml +++ b/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.' diff --git a/database/data/functors/forget_commutative.yaml b/database/data/functors/forget_commutative.yaml new file mode 100644 index 00000000..0e50c8b4 --- /dev/null +++ b/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 MSE/5133488 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. diff --git a/database/data/functors/forget_finite.yaml b/database/data/functors/forget_finite.yaml index 7b0752a2..c11819ef 100644 --- a/database/data/functors/forget_finite.yaml +++ b/database/data/functors/forget_finite.yaml @@ -13,6 +13,7 @@ tags: related: - id_Set + - forget_finite_group satisfied_properties: - property: fully faithful diff --git a/database/data/functors/forget_finite_abelian_group.yaml b/database/data/functors/forget_finite_abelian_group.yaml new file mode 100644 index 00000000..198dadf5 --- /dev/null +++ b/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 inclusion functor $\FinGrp \hookrightarrow \Grp$ 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 inclusion functor $\FinGrp \hookrightarrow \Grp$, which only involves abelian groups. + + - property: cofinitary + proof: We can take the same counterexample as for the inclusion functor $\FinGrp \hookrightarrow \Grp$, which only involves abelian groups. + + - property: left-invertible + proof: We can use the same proof as for the inclusion functor $\FinGrp \hookrightarrow \Grp$. diff --git a/database/data/functors/forget_finite_group.yaml b/database/data/functors/forget_finite_group.yaml new file mode 100644 index 00000000..f1e77c36 --- /dev/null +++ b/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 MO/513646. diff --git a/database/data/functors/forget_group.yaml b/database/data/functors/forget_group.yaml index 5b79e858..e88b3777 100644 --- a/database/data/functors/forget_group.yaml +++ b/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 diff --git a/database/data/functors/forget_hausdorff.yaml b/database/data/functors/forget_hausdorff.yaml new file mode 100644 index 00000000..5cd12519 --- /dev/null +++ b/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 nLab) 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 $\Haus$ are not stable under filtered colimits, whereas they are in $\Top$. Thus, the claim follows from Lemma 2 here. diff --git a/database/data/functors/forget_inverses.yaml b/database/data/functors/forget_inverses.yaml index f3996d71..be8d4a8e 100644 --- a/database/data/functors/forget_inverses.yaml +++ b/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$. diff --git a/database/data/functors/forget_torsion.yaml b/database/data/functors/forget_torsion.yaml new file mode 100644 index 00000000..1cc5bd19 --- /dev/null +++ b/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. diff --git a/database/data/functors/forget_torsion_free.yaml b/database/data/functors/forget_torsion_free.yaml index e3656799..cde307a1 100644 --- a/database/data/functors/forget_torsion_free.yaml +++ b/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 diff --git a/database/data/functors/indiscrete_topology.yaml b/database/data/functors/indiscrete_topology.yaml index 1f9eeae3..31593840 100644 --- a/database/data/functors/indiscrete_topology.yaml +++ b/database/data/functors/indiscrete_topology.yaml @@ -14,7 +14,7 @@ related: - discrete_topology satisfied_properties: - - property: full + - property: fully faithful proof: This is trivial. - property: preserves initial objects @@ -23,9 +23,6 @@ satisfied_properties: - property: right adjoint proof: 'This functor is right adjoint to the forgetful functor $U_{\Top} : \Top \to \Set$.' - - property: left-invertible - proof: The forgetful functor provides a left inverse. - - property: preserves coequalizers proof: 'This follows easily from the description of coequalizers in $\Set$ and $\Top$, and the fact that if $p : X \to Y$ is a surjective map, then $I(p) : I(X) \to I(Y)$ is a quotient map.'