Add the fundamental group functor

.cspell.json

@@ -40,6 +40,7 @@
 		"Birkhoff",
 		"Bogachev",
 		"Borel",
+		"Bredon",
 		"cancellative",
 		"cartesian",
 		"Catabase",
@@ -159,6 +160,7 @@
 		"Haus",
 		"Hertweck",
 		"Heyting",
+		"homotopic",
 		"homotopy",
 		"Hušek",
 		"hypercategories",

databases/catdat/data/categories/Set.yaml

@@ -12,7 +12,7 @@ tags:
 
 related_categories:
   - FinSet
-  - Set*
+  - Set_*
   - Set_c
   - Set_f
   - SetxSet

databases/catdat/data/categories/Set_pointed.yaml

@@ -1,4 +1,4 @@
-id: Set*
+id: Set_*
 name: category of pointed sets
 notation: $\Set_*$
 objects: pointed sets
@@ -11,7 +11,7 @@ tags:
 
 related_categories:
   - Set
-  - Top*
+  - Top_*
 
 satisfied_properties:
   - property: locally small

databases/catdat/data/categories/Setne.yaml

@@ -79,7 +79,7 @@ unsatisfied_properties:
     proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square.
 
   - property: coaccessible
-    proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a> also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to <a href="/category/Set*">$\Set_*$</a>, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in loc. cit.).
+    proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a> also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to <a href="/category/Set_*">$\Set_*$</a>, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in loc. cit.).
 
 special_objects:
   terminal object:

databases/catdat/data/categories/Top.yaml

@@ -13,7 +13,7 @@ tags:
 related_categories:
   - Haus
   - Met_c
-  - Top*
+  - Top_*
 
 satisfied_properties:
   - property: locally small

databases/catdat/data/categories/Top_pointed.yaml

@@ -1,4 +1,4 @@
-id: Top*
+id: Top_*
 name: category of pointed topological spaces
 notation: $\Top_*$
 objects: pointed topological spaces
@@ -10,7 +10,7 @@ tags:
   - topology
 
 related_categories:
-  - Set*
+  - Set_*
   - Top
 
 satisfied_properties:
@@ -52,11 +52,11 @@ satisfied_properties:
     proof: Since embeddings are regular monomorphisms in this category (see below) and hence strong monomorphisms, it suffices to prove that the canonical morphism $X \vee Y \hookrightarrow X \times Y$ is an embedding. For a proof, see <a href="https://math.stackexchange.com/questions/4055988" target="_blank">MSE/4055988</a>.
 
   - property: CIP
-    proof: This follows since <a href="/category/Set*">$\Set_*$</a> has this property and the forgetful functor preserves products and coproducts.
+    proof: This follows since <a href="/category/Set_*">$\Set_*$</a> has this property and the forgetful functor preserves products and coproducts.
 
   - property: cocartesian cofiltered limits
     proof: >-
-      We continue the proof for <a href="/category/Set*">$\Set_*$</a> by showing that the natural bijective map
+      We continue the proof for <a href="/category/Set_*">$\Set_*$</a> by showing that the natural bijective map
       $$\textstyle \alpha : X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$$
       is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^{-1}(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^{-1}(V_i) \cap \lim_i Y_i)$ is $p_i^{-1}(X \vee V_i)$, hence open.
 
@@ -93,13 +93,13 @@ unsatisfied_properties:
     proof: 'The image of $X \vee Y$ in $X \times Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial.'
 
   - property: regular quotient object classifier
-    proof: We can recycle the proof for <a href="/category/Set*">$\Set_*$</a> using discrete topological spaces.
+    proof: We can recycle the proof for <a href="/category/Set_*">$\Set_*$</a> using discrete topological spaces.
 
   - property: coaccessible
-    proof: 'We can adjust the proof for <a href="/category/Top">$\Top$</a> as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since <a href="/category/Set*">$\Set_*$</a> is not coaccessible, this is a contradiction.'
+    proof: 'We can adjust the proof for <a href="/category/Top">$\Top$</a> as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since <a href="/category/Set_*">$\Set_*$</a> is not coaccessible, this is a contradiction.'
 
   - property: cofiltered-limit-stable epimorphisms
-    proof: We already know that <a href="/category/Set*">$\Set_*$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology.
+    proof: We already know that <a href="/category/Set_*">$\Set_*$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology.
 
   - property: effective congruences
     proof: Suppose that $\Top_*$ had effective congruences. Then by <a href="/content/coslice-effective-congruences">this result</a>, <a href="/category/Top">$\Top$</a> would also have effective congruences, which we know is not the case.

databases/catdat/data/functors/forget_group_pointed.yaml

@@ -2,7 +2,7 @@ id: forget_group_pointed
 name: forgetful functor from groups to pointed sets
 notation: $U_{\Grp,\Set_*}$
 source: Grp
-target: Set*
+target: Set_*
 description: This functor maps a group $G$ to its underlying pointed set $U_{\Grp,\Set_*}(G)$, whose base point is the identity element of $G$. It is an example of an essentially surjective functor which is not right-invertible.
 nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
 
@@ -28,7 +28,7 @@ satisfied_properties:
     proof: 'It suffices to prove that $U_{\Grp} : \Grp \to \Set$ preserves them, which follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.'
 
   - property: preserves epimorphisms
-    proof: This follows from the classifications of epimorphisms in <a href="/category/Grp">$\Grp$</a> and in <a href="/category/Set*">$\Set_*$</a>.
+    proof: This follows from the classifications of epimorphisms in <a href="/category/Grp">$\Grp$</a> and in <a href="/category/Set_*">$\Set_*$</a>.
 
   - property: essentially surjective
     proof: Let $(X,x_0)$ be a pointed set. If $X$ is finite, we can endow $X$ with a cyclic group structure in which $x_0$ is the identity element. If $X$ is infinite, there is a bijection between $X$ and the set $P_{<\aleph_0}(X)$ of finite subsets of $X$, and we may assume that $x_0$ is mapped to $\varnothing$. Since $P_{<\aleph_0}(X)$ carries a group structure with identity element $\varnothing$ (it is the underlying set of the vector space $\IF_2^{\oplus X}$), $X$ also carries a group structure with identity element $x_0$.

databases/catdat/data/functors/pi_0.yaml

@@ -11,6 +11,7 @@ tags:
 
 related_functors:
   - forget_topology
+  - pi_1
 
 satisfied_properties:
   - property: preserves products

databases/catdat/data/functors/pi_1.yaml

@@ -0,0 +1,59 @@
+id: pi_1
+name: fundamental group functor
+notation: $\pi_1$
+source: Top_*
+target: Grp
+description: The fundamental group $\pi_1(X,x_0)$ of a pointed topological space $(X,x_0)$ is the group of homotopy classes of loops at $x_0$. The group operation is concatenation of paths. For example, we have $\pi_1(S^1,1) \cong \IZ$ (see Hatcher's <a href="https://pi.math.cornell.edu/~hatcher/AT/ATpage.html" target="_blank">Algebraic Topology</a>, Theorem 1.7).
+nlab_link: https://ncatlab.org/nlab/show/fundamental+group
+
+tags:
+  - topology
+
+related_functors:
+  - pi_0
+
+satisfied_properties:
+  - property: preserves products
+    proof: This is straightforward to check. A reference for binary products is Theorem III.2.6 in Bredon's <a href="https://doi.org/10.1007/978-1-4757-6848-0" target="_blank">Topology and Geometry</a>. The general case works exactly the same.
+
+  - property: right-invertible
+    proof: The classifying space $BG$ of a group $G$ is functorial in $G$ and satisfies $\pi_1(BG) \cong G$; see Hatcher's <a href="https://pi.math.cornell.edu/~hatcher/AT/ATpage.html" target="_blank">Algebraic Topology</a>, Example 1B.7.
+
+unsatisfied_properties:
+  - property: conservative
+    proof: 'The inclusion map $(\{0\},0) \hookrightarrow ([0,1],0)$ induces an isomorphism of groups $\pi_1(\{0\},0) \to \pi_1([0,1],0)$ (both groups are trivial), but is not an isomorphism itself.'
+
+  - property: faithful
+    proof: 'Any two pointed continuous maps $(\IR,0) \to (\IR,0)$, such as $x \mapsto \pm x$, have the same image under $\pi_1$ since $\pi_1(\IR,0)$ is the trivial group. More generally, homotopic pointed maps have the same image under $\pi_1$.'
+
+  - property: full
+    proof: See <a href="https://math.stackexchange.com/questions/414093" target="_blank">MSE/414093</a>.
+
+  - property: essentially injective
+    proof: We have $\pi_1(\{0\},0) \cong \pi_1([0,1],0)$ (both groups are trivial), but $(\{0\},0) \not\cong ([0,1],0)$.
+
+  - property: preserves monomorphisms
+    proof: The functor $\pi_1$ maps the embedding $(S^1,1) \hookrightarrow (\IC,1)$ to the trivial group homomorphism $\IZ \to \{1\}$, which is not injective.
+
+  - property: preserves epimorphisms
+    proof: The functor $\pi_1$ maps the epimorphism $(\IR,0) \to (S^1,1)$, $t \mapsto e^{2 \pi i t}$, to the trivial group homomorphism $\{1\} \to \IZ$, which is not surjective.
+
+  - property: preserves reflexive coequalizers
+    proof: 'The previous counterexample of an epimorphism $f : (\IR,0) \to (S^1,1)$ that is not preserved by $\pi_1$ is actually an open map and hence a regular epimorphism, and in <a href="/category/Top_*">$\Top_*$</a>, every regular epimorphism $f : X \to Y$ is the coequalizer of the reflexive pair $p_1,p_2 : X \times_Y X \rightrightarrows Y$.'
+
+  - property: preserves binary coproducts
+    proof: See <a href="https://math.stackexchange.com/questions/3991443" target="_blank">MSE/3991443</a> or <a href="https://math.stackexchange.com/questions/2788471" target="_blank">MSE/2788471</a> for counterexamples. See <a href="https://math.stackexchange.com/questions/4625240" target="_blank">MSE/4625240</a> for conditions which binary products are preserved.
+
+  - property: finitary
+    proof: >-
+      Consider the sequence of pointed spaces
+      $$(S^1,1) \xrightarrow{f} (S^1,1) \xrightarrow{f} (S^1,1) \xrightarrow{f} \cdots \tag{S}$$
+      where $f(z) \coloneqq z^2$. The induced sequence of fundamental groups is isomorphic to
+      $$\IZ \xrightarrow{2} \IZ \xrightarrow{2} \IZ \xrightarrow{2} \cdots,$$
+      whose colimit is $\IZ[1/2]$, the group of dyadic rationals.
+      In contrast, since $f$ is a surjective open map, the colimit $(X,x_0)$ of (S) is a quotient of $(S^1,1)$, namely $(S^1 / G,[1])$, where $G \subseteq S^1$ is the subgroup of elements $a \in S^1$ satisfying $a^{2^n}=1$ for some $n \in \IN$.
+      The quotient $S^1 / G$ is indiscrete: any non-empty open subset pulls back to a non-empty open subset of $S^1$ that is $G$-invariant, and this must be all of $S^1$ since $G \subseteq S^1$ is dense.
+      Now it is easy to check that the fundamental group of an indiscrete pointed space is trivial. This proves that $\pi_1$ does not preserve the colimit of (S).
+
+  - property: cofinitary
+    proof: See <a href="https://math.stackexchange.com/questions/3680659" target="_blank">MSE/3680659</a>.

databases/catdat/scripts/expected-data/decided-categories.json

@@ -11,10 +11,10 @@
 	"FinSet",
 	"Set",
 	"Set_op",
-	"Set*",
+	"Set_*",
 	"Top",
 	"Top_op",
-	"Top*",
+	"Top_*",
 	"Vect",
 	"FinVect_f",
 	"FinVect_c",