diff --git a/.cspell.json b/.cspell.json index ce804428..8d7ec4c2 100644 --- a/.cspell.json +++ b/.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", diff --git a/databases/catdat/data/categories/Set.yaml b/databases/catdat/data/categories/Set.yaml index 8008f4f3..96acaef9 100644 --- a/databases/catdat/data/categories/Set.yaml +++ b/databases/catdat/data/categories/Set.yaml @@ -12,7 +12,7 @@ tags: related_categories: - FinSet - - Set* + - Set_* - Set_c - Set_f - SetxSet diff --git a/databases/catdat/data/categories/Set_pointed.yaml b/databases/catdat/data/categories/Set_pointed.yaml index e14cfef7..6550f72c 100644 --- a/databases/catdat/data/categories/Set_pointed.yaml +++ b/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 diff --git a/databases/catdat/data/categories/Setne.yaml b/databases/catdat/data/categories/Setne.yaml index e4c3c5ef..b598b79f 100644 --- a/databases/catdat/data/categories/Setne.yaml +++ b/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 Adamek-Rosicky also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to $\Set_*$, 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 Adamek-Rosicky also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to $\Set_*$, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in loc. cit.). special_objects: terminal object: diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index c6a2b274..32e5d93c 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -13,7 +13,7 @@ tags: related_categories: - Haus - Met_c - - Top* + - Top_* satisfied_properties: - property: locally small diff --git a/databases/catdat/data/categories/Top_pointed.yaml b/databases/catdat/data/categories/Top_pointed.yaml index 73930b88..1f54c3bd 100644 --- a/databases/catdat/data/categories/Top_pointed.yaml +++ b/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 MSE/4055988. - property: CIP - proof: This follows since $\Set_*$ has this property and the forgetful functor preserves products and coproducts. + proof: This follows since $\Set_*$ has this property and the forgetful functor preserves products and coproducts. - property: cocartesian cofiltered limits proof: >- - We continue the proof for $\Set_*$ by showing that the natural bijective map + We continue the proof for $\Set_*$ 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 $\Set_*$ using discrete topological spaces. + proof: We can recycle the proof for $\Set_*$ using discrete topological spaces. - property: coaccessible - proof: 'We can adjust the proof for $\Top$ 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 Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' + proof: 'We can adjust the proof for $\Top$ 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 Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' - property: cofiltered-limit-stable epimorphisms - proof: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology. + proof: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here 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 this result, $\Top$ would also have effective congruences, which we know is not the case. diff --git a/databases/catdat/data/functors/forget_group_pointed.yaml b/databases/catdat/data/functors/forget_group_pointed.yaml index f33a87f3..1ef1628f 100644 --- a/databases/catdat/data/functors/forget_group_pointed.yaml +++ b/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 nLab.' - property: preserves epimorphisms - proof: This follows from the classifications of epimorphisms in $\Grp$ and in $\Set_*$. + proof: This follows from the classifications of epimorphisms in $\Grp$ and in $\Set_*$. - 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$. diff --git a/databases/catdat/data/functors/pi_0.yaml b/databases/catdat/data/functors/pi_0.yaml index 00c7d98b..96e33cc8 100644 --- a/databases/catdat/data/functors/pi_0.yaml +++ b/databases/catdat/data/functors/pi_0.yaml @@ -11,6 +11,7 @@ tags: related_functors: - forget_topology + - pi_1 satisfied_properties: - property: preserves products diff --git a/databases/catdat/data/functors/pi_1.yaml b/databases/catdat/data/functors/pi_1.yaml new file mode 100644 index 00000000..be68e2b6 --- /dev/null +++ b/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 Algebraic Topology, 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 Topology and Geometry. 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 Algebraic Topology, 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 MSE/414093. + + - 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 $\Top_*$, 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 MSE/3991443 or MSE/2788471 for counterexamples. See MSE/4625240 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 MSE/3680659. diff --git a/databases/catdat/scripts/expected-data/decided-categories.json b/databases/catdat/scripts/expected-data/decided-categories.json index 4a982575..ff088f53 100644 --- a/databases/catdat/scripts/expected-data/decided-categories.json +++ b/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",