diff --git a/content/Meas_not_regular.md b/content/Meas_not_regular.md deleted file mode 100644 index 7b077788..00000000 --- a/content/Meas_not_regular.md +++ /dev/null @@ -1,27 +0,0 @@ ---- -title: The category of measurable spaces is not regular -description: An example of a quotient measurable map is given whose product with itself is not a quotient map anymore. ---- - -## $\Meas$ is not regular - -::: Claim -The category $\Meas$ of measurable spaces and measurable maps is not regular. -::: - -_Proof._ -In a regular category, regular epimorphisms are stable under pullbacks and compositions (see Prop. 3.7 at the [nLab](https://ncatlab.org/nlab/show/regular+epimorphism)), which implies that for every regular epimorphism $f : X \to Y$ also $f \times f : X \times X \to Y \times Y$ is a regular epimorphism. We will show that this fails in $\Meas$. - -Let $X \coloneqq [0, 1)$ equipped with the standard Borel $\sigma$-algebra $\B$. Consider the equivalence relation $x \sim y \iff x-y \in \IQ$, let $Y \coloneqq X /{\sim}$ be the set of equivalence classes, and $f: X \to Y$ be the natural projection map. Equip $Y$ with the quotient $\sigma$-algebra $\Sigma_Y$, so that $f$ is a regular epimorphism. - -Now consider the diagonal in the quotient space $\Delta_Y \coloneqq \{(y, y) \mid y \in Y\}$. Then -$$\textstyle (f \times f)^{-1}(\Delta_Y) = \{(x_1, x_2) \in [0, 1)^2 \mid x_1 - x_2 \in \IQ\} \eqqcolon \bigcup_{q \in \IQ} L_q$$ -where each $L_q$ is the intersection of the diagonal level sets of $x_1 - x_2$ with $[0, 1)^2$. Because each line is closed in $\IR^2$, its intersection with $[0, 1)^2$ is a Borel set in $X \times X$. Since a countable union of Borel sets is Borel, $(f \times f)^{-1}(\Delta_Y) \in \B \otimes \B$. - -Now take any set $B \in \Sigma_Y$. Its preimage $f^{-1}(B)$ is a Borel set in $[0, 1)$ that is invariant under rational translations modulo 1. Because the action of $\IQ / \IZ$ on $[0, 1)$ is ergodic, the Lebesgue measure $\lambda(f^{-1}(B))$ must be exactly $0$ or $1$. Assume for contradiction that $\Sigma_Y$ is countably separated, i.e. there exists a countable sequence of measurable sets $(B_n)_{n \geq 1}$ in $\Sigma_Y$ that separates the points of $Y$. Let $A_n \coloneqq f^{-1}(B_n)$. Every $A_n$ has $\lambda(A_n) = 0$ or $\lambda(A_n) = 1$. - -Define a "bad set" $N \subseteq [0, 1)$ as -$$\textstyle N \coloneqq \left( \bigcup_{\lambda(A_n)=0} A_n \right) \cup \left( \bigcup_{\lambda(A_n)=1} A_n^c \right)$$ -Because $N$ is a countable union of sets with measure $0$, we have $\lambda(N) = 0$, and thus $\lambda([0, 1) \setminus N)=1$. For any two points $x, y \in [0, 1) \setminus N$, clearly $x \in A_n \iff y \in A_n$ for every $n$. Consequently, the sequence $(B_n)$ fails to separate $f(x)$ and $f(y)$. Hence, $x \sim y$. Since $[0, 1) \setminus N$ has measure $1$, it is uncountable. Because each equivalence class is only countable, these uncountably many points must belong to uncountably many different equivalence classes. Thus, we can easily pick $x, y \in [0, 1) \setminus N$ where $x \not\sim y$. Thus $\Sigma_Y$ is not countably separated. - -Hence by Theorem 6.5.7 in Bogachev's [Measure theory](https://link.springer.com/book/10.1007/978-3-540-34514-5) $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism. $\square$ diff --git a/content/aleph1-cofiltered-limits-fg-groups.md b/content/aleph1-cofiltered-limits-fg-groups.md deleted file mode 100644 index 3fbcc78b..00000000 --- a/content/aleph1-cofiltered-limits-fg-groups.md +++ /dev/null @@ -1,74 +0,0 @@ ---- -title: ℵ₁-cofiltered limits of finitely generated abelian groups -description: The existence of these limits follows from a couple of reduction arguments. ---- - -## ℵ₁-cofiltered limits of finitely generated abelian groups - -While the category $\Ab_\fg$ of finitely generated abelian groups has neither filtered colimits nor cofiltered limits, it does have $\aleph_1$-filtered colimits and $\aleph_1$-cofiltered limits. The first claim is proved in [MO/400763](https://mathoverflow.net/questions/400763). The second claim is proved here. In fact, we will show that the embedding $\Ab_\fg \hookrightarrow \Ab$ is closed under $\aleph_1$-cofiltered limits. - -Let $D : \I \to \Ab$ be an $\aleph_1$-cofiltered diagram such that each $D(i)$ is finitely generated. We will show that its limit is finitely generated as well. The proof proceeds in three steps: - -1. Reduce to the case where every morphism $D(i \to j) : D(i) \to D(j)$ is surjective. -2. Reduce further to the case where the groups $D(i)$ all have the same rank. -3. Reduce further to the case where the torsion subgroups $T(i)$ all have the same cardinality. - -In case (3), we will see that all morphisms $D(i \to j)$ are bijective, from which the claim follows immediately. - -For $i \in \I$ let -$$S_i \coloneqq \{\im(D(j \to i)) : j \to i\}.$$ -This is a set of subgroups of $D(i)$. Since every subgroup of $D(i)$ is finitely generated, $D(i)$ has only countably many subgroups. Hence $S_i$ is countable as well. For every $H \in S_i$, choose a morphism $i_H \to i$ such that $H = \im(D(i_H \to i))$. Since $\I$ is $\aleph_1$-cofiltered, the diagram consisting of the morphisms $i_H \to i$ admits a cone. That is, there exists a morphism $i_\infty \to i$ together with morphisms $i_\infty \to i_H$ over $i$ for every $H \in S_i$. Now consider the subgroup -$$M(i) \coloneqq \im(D(i_\infty \to i)) \subseteq D(i).$$ -It belongs to $S_i$, but it is also contained in every $H \in S_i$, since $i_\infty \to i$ factors through $i_H \to i$. Hence $M(i)$ is the minimal element of $S_i$ with respect to inclusion. - -For every morphism $k \to i_\infty$ we have -$$M(i) = \im(D(k \to i)),$$ -since the inclusion $\supseteq$ is obvious, while $\subseteq$ follows from the minimality just established. - -Now let $i \to j$ be a morphism. We claim that $D(i) \to D(j)$ maps $M(i)$ onto $M(j)$. Since $\I$ is cofiltered, we can find a commutative diagram - -$$ -\begin{CD} -k @>>> i_\infty @>>> i \\ -@V{=}VV @. @VVV \\ -k @>>> j_\infty @>>> j. -\end{CD} -$$ - -Hence - -$$M(j) = \im(D(k \to j)) = D(i \to j)(\im(D(k \to i))) = D(i \to j)(M(i)).$$ - -The canonical injective homomorphism -$$\textstyle \lim_{i \in \I} M(i) \hookrightarrow \lim_{i \in \I} D(i)$$ -is an isomorphism. Indeed, for every $x \in \lim_{i \in \I} D(i)$, we have $x_j = D(i \to j)(x_i)$ for all $i \to j$, showing that $x_j \in M_j$. Thus, we may replace $D$ by the diagram $M$. - -In other words, we may assume from now on that for every morphism $i \to j$ the induced morphism $D(i) \to D(j)$ is surjective. Then -$$\rank(D(i)) \geq \rank(D(j))$$ -for every morphism $i \to j$. It follows that the set -$$\{\rank(D(i)) : i \in \I\}$$ -is bounded. Indeed, otherwise for every $n \in \IN$ we could choose an object $i_n \in \I$ such that $D(i_n)$ has rank at least $n$. Choosing a cone $(j \to i_n)_{n \in \IN}$, we would obtain a group $D(j)$ of infinite rank, a contradiction. - -Therefore the natural number -$$R \coloneqq \max\{\rank(D(i)) : i \in \I\}$$ -is well-defined. Let $\J \subseteq \I$ be the full subcategory consisting of those objects $i \in \I$ for which $D(i)$ has rank $R$. If $i \to j$ is a morphism and $j \in \J$, then necessarily $i \in \J$ as well. Since $\I$ is cofiltered, it follows from this property that $\J$ is an initial subcategory of $\I$, i.e. that $\J/i$ is connected for every $i \in \I$. Hence the limit of $D$ coincides with the limit of $D|_{\J}$. - -Thus, we may assume from now on that all groups $D(i)$ have the same rank $R$. Let $T(i) \subseteq D(i)$ denote the torsion subgroup, which is finite, and let $F(i) \coloneqq D(i)/T(i)$, which is a finitely generated free abelian group. For a morphism $i \to j$ consider the commutative diagram with exact rows: - -$$ -\begin{CD} -0 @>>> T(i) @>>> D(i) @>>> F(i) @>>> 0 \\ -@. @VVV @VVV @VVV @. \\ -0 @>>> T(j) @>>> D(j) @>>> F(j) @>>> 0 -\end{CD} -$$ - -The homomorphism $F(i) \to F(j)$ is surjective, since $D(i) \to D(j)$ is surjective. Since it is a surjective homomorphism between finitely generated free abelian groups of the same rank, it is an isomorphism. Applying the snake lemma to the diagram above, we conclude that $T(i) \to T(j)$ is surjective. - -As before, it follows that the natural number -$$N \coloneqq \max\{\card(T(i)) : i \in \I\}$$ -is well-defined, and that the full subcategory consisting of those objects $i \in \I$ for which $\card(T(i)) = N$ is initial. Hence we may assume that all groups $T(i)$ have the same cardinality. - -Now for every morphism $i \to j$ the induced homomorphism $T(i) \to T(j)$ is a surjective map between finite sets of the same cardinality, and is therefore bijective. Applying the snake lemma once more to the diagram above, we conclude that $D(i) \to D(j)$ is an isomorphism. - -In this case, the limit of $D$ is simply given by any of the groups $D(i)$, and is therefore finitely generated. diff --git a/content/aleph1-filtered-colimits-in-deloopings.md b/content/aleph1-filtered-colimits-in-deloopings.md deleted file mode 100644 index d9ad3311..00000000 --- a/content/aleph1-filtered-colimits-in-deloopings.md +++ /dev/null @@ -1,118 +0,0 @@ ---- -title: ℵ₁-filtered colimits in deloopings -description: We give a detailed proof that the delooping of the monoid of natural numbers, and likewise the delooping of the large monoid of ordinal numbers, has colimits indexed by ℵ₁-filtered categories. ---- - -## $\aleph_1$-filtered colimits in deloopings - -Every (possibly large) monoid $M$ induces a category $BM$ with just one object. We will show that this category has $\aleph_1$-filtered colimits in the cases $M = \IN$ and $M = \On$ (both respect to addition). - -::: Proposition 1 -The category $B\IN$ has $\aleph_1$-filtered colimits. -::: - -_Proof._ -Let $D : \I \to B\IN$ be an $\aleph_1$-filtered diagram. Every two parallel morphisms $i \rightrightarrows j$ are mapped to the same morphism in $B \IN$, because they are coequalized by some morphism and $(\IN,+)$ is cancellative. Hence, $D$ factors through the preorder reflection of $\I$, and we may therefore assume that $\I$ itself is a preordered set. Thus, the diagram consists of numbers $D(i,j) \in \IN$ for all $i \leq j$ satisfying - -$$D(j,k) + D(i,j) = D(i,k)$$ - -for all $i \leq j \leq k$. In particular, $D(i,j) \leq D(i,k)$. - -Let $i \in \I$. The set of natural numbers $\{D(i,k) : k \geq i\}$ is bounded above. Otherwise, for every $n \in \IN$ we could find $k_n \in \I$ with $k_n \geq i$ and $D(i,k_n) \geq n$. Since $\I$ is $\aleph_1$-filtered, the family $(k_n)_{n \in \IN}$ has an upper bound $k_\infty \in \I$. But then - -$$D(i, k_\infty) = D(k_n,k_\infty) + D(i, k_n) \geq D(i, k_n) \geq n$$ - -for all $n \in \IN$, contradicting the fact that $D(i,k_\infty) \in \IN$. - -Therefore, the maximum - -$$u_i \coloneqq \max \{D(i,k) : k \geq i\} \in \IN$$ - -is well-defined, which we regard as a morphism in $B\IN$. For $i \leq j$ we compute - -$$ -\begin{align*} -u_i & = \max \{D(i,k) : k \geq i\} \\ -& = \max \{D(i,k) : k \geq j\} \\ -& = \max \{ D(j,k) + D(i,j) : k \geq j\} \\ -& = \max \{D(j,k) : k \geq j\} + D(i,j)\\ -& = u_j + D(i,j), -\end{align*} -$$ - -showing that $(u_i)$ defines a cocone. It is universal: let $(v_i)$ be another cocone, i.e. $v_i \in \IN$ and $v_i = v_j + D(i,j)$ for all $i \leq j$. Then $v_i \geq D(i,j)$ for all $i \leq j$, hence $v_i \geq u_i$. Write $v_i = w_i + u_i$ for some uniquely determined $w_i \in \IN$. For $i \leq j$ we compute - -$$w_j + u_j + D(i,j) = v_j + D(i,j) = v_i = w_i + u_i = w_i + u_j + D(i,j),$$ - -hence $w_j = w_i$. Therefore, the $w_i$ are constant, and the required factorization follows. $\square$ - -::: Proposition 2 -The category $B\IN$ is $\aleph_1$-accessible. -::: - -_Proof._ -Based on Proposition 1, it remains to show that the unique object $*$ is $\aleph_1$-presentable, i.e. that for every diagram $D : \I \to B\IN$ as above, the canonical map - -$$\alpha : \colim_{i \in \I} \Hom(*,D(i)) \to \Hom(*,\colim_{i \in \I} D(i))$$ - -is bijective. On objects, we necessarily have $D(i)=*$ and $\colim_{i \in \I} D(i)=*$. Hence, the codomain of $\alpha$ is simply $\IN$, while the domain consists of equivalence classes $[i,n]$ of pairs $(i,n) \in \I \times \IN$, where $(i,n) \sim (j,m)$ iff there exists some $k \geq i,j$ such that - -$$D(i,k) + n = D(j,k) + m.$$ - -By the construction of the colimit cocone, we have - -$$\alpha([i,n]) = u_i + n = \max \{D(i,j) : j \geq i\} + n.$$ - -(1) **The map $\alpha$ is surjective:** Pick some $i \in \I$. Choose $j \geq i$ such that $u_i = D(i,j)$. For all $k \geq j$ we then have - -$$u_i \geq D(i,k) = D(j,k) + D(i,j) = D(j,k) + u_i,$$ - -hence $D(j,k)=0$. Therefore, $u_j=0$, and thus $\alpha([j,n]) = n$ for all $n \in \IN$. - -(2) **The map $\alpha$ is injective:** Assume that $[i,n]$ and $[j,m]$ have the same image. Since $\I$ is filtered, we may assume $i=j$. The condition then becomes $u_i + n = u_i + m$, and therefore $n=m$. This completes the proof. $\square$ - -::: Proposition 3 -The category $B\On$ has $\aleph_1$-filtered colimits. -::: - -_Proof._ -The proof is similar to $B\IN$. Let $\I$ be an $\aleph_1$-filtered small category and $D : \I \to B\On$ a diagram. A cocone $\lambda = (\lambda_i)_{i \in \I}$ for $D$ is a family of ordinals satisfying $\lambda_i = \lambda_j + D(f)$ for every morphism $f: i \to j$ in $\I$. - -We first observe that $D$ factors uniquely through the preorder reflection of $\I$. Indeed, any two parallel morphisms in $\I$ are coequalized by some morphism, and $B\On$ is left cancellative. Thus, we may assume that $\I$ is a preordered set. Each inequality $i \leq j$ in $\I$ is mapped to an ordinal number $\alpha_{i,j} \coloneqq D(i \to j)$, and these numbers satisfy -$$\alpha_{i,k} = \alpha_{j,k} + \alpha_{i,j}$$ -for all $i \leq j \leq k$. In particular, $\alpha_{i,j} \leq \alpha_{i,k}$. - -For fixed $i \in \I$, the collection $\{\alpha_{i,j} : j \geq i\}$ is a set of ordinals because $\I$ is small, hence bounded above in $\On$. We claim that it has a maximum element. Otherwise, we can find a countable chain $i = j_0 \leq j_1 \leq j_2 \leq \dotsc$ in $\I$ such that $\alpha_{i,j_n} < \alpha_{i,j_{n+1}}$ for all $n \in \IN$. Since $\I$ is $\aleph_1$-filtered, there is an upper bound $j_\infty \in \I$ of $(j_n)_{n \in \IN}$. For each $n \in \IN$, the equation -$$\alpha_{i,j_{n+1}} = \alpha_{j_n,j_{n+1}} + \alpha_{i,j_n}$$ -implies that $\alpha_{j_n,j_{n+1}} > 0$. Hence, -$$\alpha_{j_n,j_\infty} = \alpha_{j_{n+1},j_\infty} + \alpha_{j_n,j_{n+1}} > \alpha_{j_{n+1},j_\infty},$$ -so $(\alpha_{j_n,j_\infty})_{n \in \IN}$ is a strictly decreasing infinite sequence of ordinals, contradicting the well-foundedness of $\On$. Thus, the maximum -$$u_i \coloneqq \max \{ \alpha_{i,j} : j \geq i \}$$ -is a well-defined ordinal number, which we regard as a morphism in $B\On$. The family $(u_i)_{i \in \I}$ forms a cocone for $D$, since for all $i \leq j$ we have - -$$ -\begin{align*} -u_i & = \max \{ \alpha_{i,k} : k \geq i \} \\ -& = \max \{ \alpha_{i,k} : k \geq j \} \\ -& = \max \{ \alpha_{j,k} + \alpha_{i,j} : k \geq j \} \\ -& = \max \{ \alpha_{j,k} : k \geq j \} + \alpha_{i,j} \\ -& = u_j + \alpha_{i,j}. -\end{align*} -$$ - -To establish the universal property, let $(\lambda_i)_{i \in \I}$ be any cocone for $D$, so that $\lambda_i = \lambda_j + \alpha_{i,j}$ for all $i \leq j$. The cocone relation $u_i = u_j + \alpha_{i,j}$ implies that $u_i \geq u_j$ whenever $i \leq j$. By the well-foundedness of $\On$, there exists $i_0 \in \I$ such that $u_j = u_{i_0}$ for all $j \geq i_0$. For such $j$, the relation -$$u_{i_0} = u_j + \alpha_{i_0,j} = u_{i_0} + \alpha_{i_0,j}$$ -forces $\alpha_{i_0,j} = 0$. Consequently, -$$u_{i_0} = \max \{ \alpha_{i_0,j} : j \geq i_0 \} = 0.$$ -Define the mediating morphism to be the ordinal $\kappa \coloneqq \lambda_{i_0}$. We must show that $\lambda_i = \kappa + u_i$ for all $i \in \I$. Choose $j \in \I$ with $j \geq i$ and $j \geq i_0$. Since $j \geq i_0$, we have $u_j = 0$ and $\alpha_{i_0,j} = 0$. The cocone condition for $\lambda$ gives -$$\kappa = \lambda_{i_0} = \lambda_j + \alpha_{i_0,j} = \lambda_j.$$ -Applying the cocone conditions for $u$ and $\lambda$ to $i \leq j$, we obtain -$$u_i = u_j + \alpha_{i,j} = 0 + \alpha_{i,j} = \alpha_{i,j}$$ -and -$$\lambda_i = \lambda_j + \alpha_{i,j} = \kappa + \alpha_{i,j} = \kappa + u_i.$$ -This proves the existence of the mediating morphism. - -For uniqueness, suppose $\kappa'$ is any ordinal satisfying $\lambda_i = \kappa' + u_i$ for all $i \in \I$. Evaluating at $i_0$ yields -$$\lambda_{i_0} = \kappa' + u_{i_0} = \kappa' + 0 = \kappa',$$ -hence $\kappa' = \kappa$. Therefore, the cocone $(u_i)_{i \in \I}$ is the colimit of $D$ in $B\On$. -$\square$ diff --git a/content/contribute.md b/content/contribute.md index 2f9b9cb1..8dd0b74e 100644 --- a/content/contribute.md +++ b/content/contribute.md @@ -5,7 +5,7 @@ description: CatDat welcomes contributions from the community, including filling ## How to contribute -_CatDat_ is developed in an open-source [GitHub repository](https://github.com/ScriptRaccoon/catdat) owned by [Martin Brandenburg](https://ncatlab.org/nlab/show/Martin+Brandenburg). It welcomes contributions from the community, including filling in missing information or discovering new combinations of properties. +_CatDat_ is developed in an open-source [GitHub repository](https://github.com/ScriptRaccoon/catdat) by [Martin Brandenburg](https://ncatlab.org/nlab/show/Martin+Brandenburg). It welcomes contributions from the community, including filling in missing information or discovering new combinations of properties. [**Video tutorial**](https://www.youtube.com/watch?v=NoZWdMFfQfg) diff --git a/content/generator_construction.md b/content/generator_construction.md index b8633199..b11cc2cb 100644 --- a/content/generator_construction.md +++ b/content/generator_construction.md @@ -1,9 +1,9 @@ --- -title: Construction of Generators +title: Construction of generators description: How to construct a generator from a generating set --- -## Construction of Generators +## Construction of generators ::: Lemma In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating set, then $U$ is an extremal generator. diff --git a/content/resources.md b/content/resources.md index 6e7d60e9..00cf4846 100644 --- a/content/resources.md +++ b/content/resources.md @@ -1,9 +1,9 @@ --- -title: Resources on Category Theory +title: Resources on category theory description: This is an (incomplete) list of resources on category theory. --- -## Resources on Category Theory +## Resources on category theory This is an (incomplete) list of resources on category theory. diff --git a/content/thin_extremal_generator.md b/content/thin_extremal_generator.md index f1a47f1c..547184f1 100644 --- a/content/thin_extremal_generator.md +++ b/content/thin_extremal_generator.md @@ -1,9 +1,9 @@ --- -title: Thin Category with an Extremal Generator +title: Extremal generators in thin categories description: A result restricting which thin categories can have an extremal generator --- -## Thin Category with an Extremal Generator +## Extremal generators in thin categories ::: Lemma Suppose $G$ is an object of a thin category. Then $G$ is an extremal generator if and only if for every object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism. diff --git a/content/topos-with-generator.md b/content/topos-with-generator.md index 475336ce..da2be294 100644 --- a/content/topos-with-generator.md +++ b/content/topos-with-generator.md @@ -1,9 +1,9 @@ --- -title: Topos with a Generator +title: Topos with a generator description: An elementary topos with a generator has at most two subterminal objects --- -## Topos with a Generator +## Topos with a generator ::: Lemma Suppose a category is coregular, and it has disjoint finite coproducts, a terminal object, and a generator. Then every regular subterminal object (i.e. an object $X$ such that the unique morphism $X \to 1$ is a regular monomorphism) is either initial or terminal. diff --git a/database/data/categories/Ab_fg.yaml b/database/data/categories/Ab_fg.yaml index 5ee7021d..324d7e15 100644 --- a/database/data/categories/Ab_fg.yaml +++ b/database/data/categories/Ab_fg.yaml @@ -32,7 +32,75 @@ satisfied_properties: proof: The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\Ab_{\fg}$ has $\aleph_1$-filtered colimits. Since $\Ab_{\fg}$ is essentially small, there is a set $G$ such that every f.g. abelian group is isomorphic to one in $G$. So trivially it is also a $\aleph_1$-filtered colimit of such objects (take the constant diagram). Finally, every object is $\Ab_{\fg} = \Ab_{\fp}$ is finitely presentable in $\Ab$ and hence also in $\Ab_{\fg}$, a fortiori $\aleph_1$-presentable. - property: ℵ₁-cofiltered limits - proof: A proof can be found here. + proof: >- + In fact, we will show that the embedding $\Ab_\fg \hookrightarrow \Ab$ is closed under $\aleph_1$-cofiltered limits. Let $D : \I \to \Ab$ be an $\aleph_1$-cofiltered diagram such that each $D(i)$ is finitely generated. We will show that its limit is finitely generated as well. The proof proceeds in three steps: + + + 1. Reduce to the case where every morphism $D(i \to j) : D(i) \to D(j)$ is surjective. + + 2. Reduce further to the case where the groups $D(i)$ all have the same rank. + + 3. Reduce further to the case where the torsion subgroups $T(i)$ all have the same cardinality. + + + In case (3), we will see that all morphisms $D(i \to j)$ are bijective, from which the claim follows immediately. + + + For $i \in \I$ let + $$S_i \coloneqq \{\im(D(j \to i)) : j \to i\}.$$ + This is a set of subgroups of $D(i)$. Since every subgroup of $D(i)$ is finitely generated, $D(i)$ has only countably many subgroups. Hence $S_i$ is countable as well. For every $H \in S_i$, choose a morphism $i_H \to i$ such that $H = \im(D(i_H \to i))$. Since $\I$ is $\aleph_1$-cofiltered, the diagram consisting of the morphisms $i_H \to i$ admits a cone. That is, there exists a morphism $i_\infty \to i$ together with morphisms $i_\infty \to i_H$ over $i$ for every $H \in S_i$. Now consider the subgroup + $$M(i) \coloneqq \im(D(i_\infty \to i)) \subseteq D(i).$$ + It belongs to $S_i$, but it is also contained in every $H \in S_i$, since $i_\infty \to i$ factors through $i_H \to i$. Hence $M(i)$ is the minimal element of $S_i$ with respect to inclusion. + + + For every morphism $k \to i_\infty$ we have + $$M(i) = \im(D(k \to i)),$$ + since the inclusion $\supseteq$ is obvious, while $\subseteq$ follows from the minimality just established. + + + Now let $i \to j$ be a morphism. We claim that $D(i) \to D(j)$ maps $M(i)$ onto $M(j)$. Since $\I$ is cofiltered, we can find a commutative diagram + $$\begin{CD} + k @>>> i_\infty @>>> i \\ + @V{=}VV @. @VVV \\ + k @>>> j_\infty @>>> j. + \end{CD}$$ + Hence + $$M(j) = \im(D(k \to j)) = D(i \to j)(\im(D(k \to i))) = D(i \to j)(M(i)).$$ + The canonical injective homomorphism + $$\textstyle \lim_{i \in \I} M(i) \hookrightarrow \lim_{i \in \I} D(i)$$ + is an isomorphism. Indeed, for every $x \in \lim_{i \in \I} D(i)$, we have $x_j = D(i \to j)(x_i)$ for all $i \to j$, showing that $x_j \in M_j$. Thus, we may replace $D$ by the diagram $M$. + + + In other words, we may assume from now on that for every morphism $i \to j$ the induced morphism $D(i) \to D(j)$ is surjective. Then + $$\rank(D(i)) \geq \rank(D(j))$$ + for every morphism $i \to j$. It follows that the set + $$\{\rank(D(i)) : i \in \I\}$$ + is bounded. Indeed, otherwise for every $n \in \IN$ we could choose an object $i_n \in \I$ such that $D(i_n)$ has rank at least $n$. Choosing a cone $(j \to i_n)_{n \in \IN}$, we would obtain a group $D(j)$ of infinite rank, a contradiction. + + + Therefore the natural number + $$R \coloneqq \max\{\rank(D(i)) : i \in \I\}$$ + is well-defined. Let $\J \subseteq \I$ be the full subcategory consisting of those objects $i \in \I$ for which $D(i)$ has rank $R$. If $i \to j$ is a morphism and $j \in \J$, then necessarily $i \in \J$ as well. Since $\I$ is cofiltered, it follows from this property that $\J$ is an initial subcategory of $\I$, i.e. that $\J/i$ is connected for every $i \in \I$. Hence the limit of $D$ coincides with the limit of $D|_{\J}$. + + + Thus, we may assume from now on that all groups $D(i)$ have the same rank $R$. Let $T(i) \subseteq D(i)$ denote the torsion subgroup, which is finite, and let $F(i) \coloneqq D(i)/T(i)$, which is a finitely generated free abelian group. For a morphism $i \to j$ consider the commutative diagram with exact rows: + $$\begin{CD} + 0 @>>> T(i) @>>> D(i) @>>> F(i) @>>> 0 \\ + @. @VVV @VVV @VVV @. \\ + 0 @>>> T(j) @>>> D(j) @>>> F(j) @>>> 0 + \end{CD}$$ + The homomorphism $F(i) \to F(j)$ is surjective, since $D(i) \to D(j)$ is surjective. Since it is a surjective homomorphism between finitely generated free abelian groups of the same rank, it is an isomorphism. Applying the snake lemma to the diagram above, we conclude that $T(i) \to T(j)$ is surjective. + + + As before, it follows that the natural number + $$N \coloneqq \max\{\card(T(i)) : i \in \I\}$$ + is well-defined, and that the full subcategory consisting of those objects $i \in \I$ for which $\card(T(i)) = N$ is initial. Hence we may assume that all groups $T(i)$ have the same cardinality. + + + Now for every morphism $i \to j$ the induced homomorphism $T(i) \to T(j)$ is a surjective map between finite sets of the same cardinality, and is therefore bijective. Applying the snake lemma once more to the diagram above, we conclude that $D(i) \to D(j)$ is an isomorphism. + + + In this case, the limit of $D$ is simply given by any of the groups $D(i)$, and is therefore finitely generated. unsatisfied_properties: - property: small diff --git a/database/data/categories/BN.yaml b/database/data/categories/BN.yaml index 6de618cb..5001c357 100644 --- a/database/data/categories/BN.yaml +++ b/database/data/categories/BN.yaml @@ -36,8 +36,50 @@ satisfied_properties: - property: locally cartesian closed proof: The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, hence cartesian closed. + - property: ℵ₁-filtered colimits + check_redundancy: false + label: BN_aleph1-filtered_colimits + proof: >- + Let $D : \I \to B\IN$ be an $\aleph_1$-filtered diagram. Every two parallel morphisms $i \rightrightarrows j$ are mapped to the same morphism in $B \IN$, because they are coequalized by some morphism and $(\IN,+)$ is cancellative. Hence, $D$ factors through the preorder reflection of $\I$, and we may therefore assume that $\I$ itself is a preordered set. Thus, the diagram consists of numbers $D(i,j) \in \IN$ for all $i \leq j$ satisfying + $$D(j,k) + D(i,j) = D(i,k)$$ + for all $i \leq j \leq k$. In particular, $D(i,j) \leq D(i,k)$. + + + Let $i \in \I$. The set of natural numbers $\{D(i,k) : k \geq i\}$ is bounded above. Otherwise, for every $n \in \IN$ we could find $k_n \in \I$ with $k_n \geq i$ and $D(i,k_n) \geq n$. Since $\I$ is $\aleph_1$-filtered, the family $(k_n)_{n \in \IN}$ has an upper bound $k_\infty \in \I$. But then + $$D(i, k_\infty) = D(k_n,k_\infty) + D(i, k_n) \geq D(i, k_n) \geq n$$ + for all $n \in \IN$, contradicting the fact that $D(i,k_\infty) \in \IN$. + + + Therefore, the maximum + $$u_i \coloneqq \max \{D(i,k) : k \geq i\} \in \IN$$ + is well-defined, which we regard as a morphism in $B\IN$. For $i \leq j$ we compute + $$\begin{align*} + u_i & = \max \{D(i,k) : k \geq i\} \\ + & = \max \{D(i,k) : k \geq j\} \\ + & = \max \{ D(j,k) + D(i,j) : k \geq j\} \\ + & = \max \{D(j,k) : k \geq j\} + D(i,j)\\ + & = u_j + D(i,j), + \end{align*}$$ + showing that $(u_i)$ defines a cocone. It is universal: let $(v_i)$ be another cocone, i.e. $v_i \in \IN$ and $v_i = v_j + D(i,j)$ for all $i \leq j$. Then $v_i \geq D(i,j)$ for all $i \leq j$, hence $v_i \geq u_i$. Write $v_i = w_i + u_i$ for some uniquely determined $w_i \in \IN$. For $i \leq j$ we compute + $$w_j + u_j + D(i,j) = v_j + D(i,j) = v_i = w_i + u_i = w_i + u_j + D(i,j),$$ + hence $w_j = w_i$. Therefore, the $w_i$ are constant, and the required factorization follows. + - property: ℵ₁-accessible - proof: A proof can be found here as Proposition 2. + references: + - BN_aleph1-filtered_colimits + proof: >- + Since we have just proven that $\aleph_1$-filtered colimits exist, it remains to show that the unique object $*$ is $\aleph_1$-presentable, i.e. that for every $\aleph_1$-filtered diagram diagram $D : \I \to B\IN$, the canonical map + $$\alpha : \colim_{i \in \I} \Hom(*,D(i)) \to \Hom(*,\colim_{i \in \I} D(i))$$ + is bijective. On objects, we necessarily have $D(i)=*$ and $\colim_{i \in \I} D(i)=*$. Hence, the codomain of $\alpha$ is simply $\IN$, while the domain consists of equivalence classes $[i,n]$ of pairs $(i,n) \in \I \times \IN$, where $(i,n) \sim (j,m)$ iff there exists some $k \geq i,j$ such that + $$D(i,k) + n = D(j,k) + m.$$ + By the construction of the colimit cocone in the previous proof, we have + $$\alpha([i,n]) = u_i + n = \max \{D(i,j) : j \geq i\} + n.$$ + (1) The map $\alpha$ is surjective: Pick some $i \in \I$. Choose $j \geq i$ such that $u_i = D(i,j)$. For all $k \geq j$ we then have + $$u_i \geq D(i,k) = D(j,k) + D(i,j) = D(j,k) + u_i,$$ + hence $D(j,k)=0$. Therefore, $u_j=0$, and thus $\alpha([j,n]) = n$ for all $n \in \IN$. + + + (2) The map $\alpha$ is injective: Assume that $[i,n]$ and $[j,m]$ have the same image. Since $\I$ is filtered, we may assume $i=j$. The condition then becomes $u_i + n = u_i + m$, and therefore $n=m$. This completes the proof. unsatisfied_properties: - property: one-way diff --git a/database/data/categories/BOn.yaml b/database/data/categories/BOn.yaml index 4c681c40..74b4a44c 100644 --- a/database/data/categories/BOn.yaml +++ b/database/data/categories/BOn.yaml @@ -38,7 +38,47 @@ satisfied_properties: proof: In fact, it is $\kappa$-cofiltered for every cardinal $\kappa$. By the dual of Theorem 2.2 at the nLab it suffices to prove any set of objects has a cone (which is trivial in a one-object category) and that any set of parallel morphisms is equalized by some morphism. Here, this means that for every set of ordinals $A$ there is some ordinal $\beta$ such that $\alpha + \beta$ for $\alpha \in A$ does not depend on $\alpha$. Take $\beta$ to be any ordinal larger than $\sup(A)$ of the form $\omega^\gamma$. It is well-known that $\omega^\gamma$ has the property that $\alpha + \omega^\gamma = \omega^\gamma$ for all $\alpha < \omega^\gamma$ (Kunen's Set Theory, Exercise I.9.53), from which the claim follows. - property: ℵ₁-filtered colimits - proof: A proof can be found here as Proposition 3. + references: + - BN_aleph1-filtered_colimits + proof: >- + The proof is similar to $B\IN$. Let $\I$ be an $\aleph_1$-filtered small category and $D : \I \to B\On$ a diagram. A cocone $\lambda = (\lambda_i)_{i \in \I}$ for $D$ is a family of ordinals satisfying $\lambda_i = \lambda_j + D(f)$ for every morphism $f: i \to j$ in $\I$. + + + We first observe that $D$ factors uniquely through the preorder reflection of $\I$. Indeed, any two parallel morphisms in $\I$ are coequalized by some morphism, and $B\On$ is left cancellative. Thus, we may assume that $\I$ is a preordered set. Each inequality $i \leq j$ in $\I$ is mapped to an ordinal number $\alpha_{i,j} \coloneqq D(i \to j)$, and these numbers satisfy + $$\alpha_{i,k} = \alpha_{j,k} + \alpha_{i,j}$$ + for all $i \leq j \leq k$. In particular, $\alpha_{i,j} \leq \alpha_{i,k}$. + + + For fixed $i \in \I$, the collection $\{\alpha_{i,j} : j \geq i\}$ is a set of ordinals because $\I$ is small, hence bounded above in $\On$. We claim that it has a maximum element. Otherwise, we can find a countable chain $i = j_0 \leq j_1 \leq j_2 \leq \dotsc$ in $\I$ such that $\alpha_{i,j_n} < \alpha_{i,j_{n+1}}$ for all $n \in \IN$. Since $\I$ is $\aleph_1$-filtered, there is an upper bound $j_\infty \in \I$ of $(j_n)_{n \in \IN}$. For each $n \in \IN$, the equation + $$\alpha_{i,j_{n+1}} = \alpha_{j_n,j_{n+1}} + \alpha_{i,j_n}$$ + implies that $\alpha_{j_n,j_{n+1}} > 0$. Hence, + $$\alpha_{j_n,j_\infty} = \alpha_{j_{n+1},j_\infty} + \alpha_{j_n,j_{n+1}} > \alpha_{j_{n+1},j_\infty},$$ + so $(\alpha_{j_n,j_\infty})_{n \in \IN}$ is a strictly decreasing infinite sequence of ordinals, contradicting the well-foundedness of $\On$. Thus, the maximum + $$u_i \coloneqq \max \{ \alpha_{i,j} : j \geq i \}$$ + is a well-defined ordinal number, which we regard as a morphism in $B\On$. The family $(u_i)_{i \in \I}$ forms a cocone for $D$, since for all $i \leq j$ we have + $$\begin{align*} + u_i & = \max \{ \alpha_{i,k} : k \geq i \} \\ + & = \max \{ \alpha_{i,k} : k \geq j \} \\ + & = \max \{ \alpha_{j,k} + \alpha_{i,j} : k \geq j \} \\ + & = \max \{ \alpha_{j,k} : k \geq j \} + \alpha_{i,j} \\ + & = u_j + \alpha_{i,j}. + \end{align*}$$ + To establish the universal property, let $(\lambda_i)_{i \in \I}$ be any cocone for $D$, so that $\lambda_i = \lambda_j + \alpha_{i,j}$ for all $i \leq j$. The cocone relation $u_i = u_j + \alpha_{i,j}$ implies that $u_i \geq u_j$ whenever $i \leq j$. By the well-foundedness of $\On$, there exists $i_0 \in \I$ such that $u_j = u_{i_0}$ for all $j \geq i_0$. For such $j$, the relation + $$u_{i_0} = u_j + \alpha_{i_0,j} = u_{i_0} + \alpha_{i_0,j}$$ + forces $\alpha_{i_0,j} = 0$. Consequently, + $$u_{i_0} = \max \{ \alpha_{i_0,j} : j \geq i_0 \} = 0.$$ + Define the mediating morphism to be the ordinal $\kappa \coloneqq \lambda_{i_0}$. We must show that $\lambda_i = \kappa + u_i$ for all $i \in \I$. Choose $j \in \I$ with $j \geq i$ and $j \geq i_0$. Since $j \geq i_0$, we have $u_j = 0$ and $\alpha_{i_0,j} = 0$. The cocone condition for $\lambda$ gives + $$\kappa = \lambda_{i_0} = \lambda_j + \alpha_{i_0,j} = \lambda_j.$$ + Applying the cocone conditions for $u$ and $\lambda$ to $i \leq j$, we obtain + $$u_i = u_j + \alpha_{i,j} = 0 + \alpha_{i,j} = \alpha_{i,j}$$ + and + $$\lambda_i = \lambda_j + \alpha_{i,j} = \kappa + \alpha_{i,j} = \kappa + u_i.$$ + This proves the existence of the mediating morphism. + + + For uniqueness, suppose $\kappa'$ is any ordinal satisfying $\lambda_i = \kappa' + u_i$ for all $i \in \I$. Evaluating at $i_0$ yields + $$\lambda_{i_0} = \kappa' + u_{i_0} = \kappa' + 0 = \kappa',$$ + hence $\kappa' = \kappa$. Therefore, the cocone $(u_i)_{i \in \I}$ is the colimit of $D$ in $B\On$. unsatisfied_properties: - property: one-way diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index ea7dcacb..af5336c0 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -126,7 +126,27 @@ unsatisfied_properties: - top_no_effective_cocongruences - property: regular - proof: A proof can be found here. + proof: >- + In a regular category, regular epimorphisms are stable under pullbacks and compositions (see Prop. 3.7 at the nLab), which implies that for every regular epimorphism $f : X \to Y$ also $f \times f : X \times X \to Y \times Y$ is a regular epimorphism. We will show that this fails in $\Meas$. + + + Let $X \coloneqq [0, 1)$ equipped with the standard Borel $\sigma$-algebra $\B$. Consider the equivalence relation $x \sim y \iff x-y \in \IQ$, let $Y \coloneqq X /{\sim}$ be the set of equivalence classes, and $f: X \to Y$ be the natural projection map. Equip $Y$ with the quotient $\sigma$-algebra $\Sigma_Y$, so that $f$ is a regular epimorphism. + + + Now consider the diagonal in the quotient space $\Delta_Y \coloneqq \{(y, y) \mid y \in Y\}$. Then + $$\textstyle (f \times f)^{-1}(\Delta_Y) = \{(x_1, x_2) \in [0, 1)^2 \mid x_1 - x_2 \in \IQ\} \eqqcolon \bigcup_{q \in \IQ} L_q$$ + where each $L_q$ is the intersection of the diagonal level sets of $x_1 - x_2$ with $[0, 1)^2$. Because each line is closed in $\IR^2$, its intersection with $[0, 1)^2$ is a Borel set in $X \times X$. Since a countable union of Borel sets is Borel, $(f \times f)^{-1}(\Delta_Y) \in \B \otimes \B$. + + + Now take any set $B \in \Sigma_Y$. Its preimage $f^{-1}(B)$ is a Borel set in $[0, 1)$ that is invariant under rational translations modulo 1. Because the action of $\IQ / \IZ$ on $[0, 1)$ is ergodic, the Lebesgue measure $\lambda(f^{-1}(B))$ must be exactly $0$ or $1$. Assume for contradiction that $\Sigma_Y$ is countably separated, i.e. there exists a countable sequence of measurable sets $(B_n)_{n \geq 1}$ in $\Sigma_Y$ that separates the points of $Y$. Let $A_n \coloneqq f^{-1}(B_n)$. Every $A_n$ has $\lambda(A_n) = 0$ or $\lambda(A_n) = 1$. + + + Define a "bad set" $N \subseteq [0, 1)$ as + $$\textstyle N \coloneqq \left( \bigcup_{\lambda(A_n)=0} A_n \right) \cup \left( \bigcup_{\lambda(A_n)=1} A_n^c \right)$$ + Because $N$ is a countable union of sets with measure $0$, we have $\lambda(N) = 0$, and thus $\lambda([0, 1) \setminus N)=1$. For any two points $x, y \in [0, 1) \setminus N$, clearly $x \in A_n \iff y \in A_n$ for every $n$. Consequently, the sequence $(B_n)$ fails to separate $f(x)$ and $f(y)$. Hence, $x \sim y$. Since $[0, 1) \setminus N$ has measure $1$, it is uncountable. Because each equivalence class is only countable, these uncountably many points must belong to uncountably many different equivalence classes. Thus, we can easily pick $x, y \in [0, 1) \setminus N$ where $x \not\sim y$. Thus $\Sigma_Y$ is not countably separated. + + + Hence by Theorem 6.5.7 in Bogachev's Measure theory $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism. - property: extremal generating set proof: >- diff --git a/database/scripts/proof-length.ts b/database/scripts/proof-length.ts deleted file mode 100644 index 81b14b41..00000000 --- a/database/scripts/proof-length.ts +++ /dev/null @@ -1,76 +0,0 @@ -import { STRUCTURE_TYPES, type StructureType } from '$shared/config' -import { get_client } from '$shared/db' -import { remove_underscores } from '$shared/utils' -get_client - -const db = get_client({ readonly: true }) - -const PROOF_LENGTH_THRESHOLD = 1200 - -report_long_proofs() - -/** - * Prints proofs whose lengths exceed the given threshold and should - * perhaps be moved to a separate content page. - */ -function report_long_proofs() { - for (const type of STRUCTURE_TYPES) { - report_long_property_proofs(type) - } - for (const type of STRUCTURE_TYPES) { - report_long_implication_proofs(type) - } -} - -function report_long_property_proofs(type: StructureType) { - const long_proofs = db - .prepare< - [StructureType, number], - { id: string; property: string; length: number } - >( - `SELECT - structure_id AS id, - property_id AS property, - length(proof) AS length - FROM property_assignments - WHERE type = ? AND is_deduced = FALSE AND length(proof) >= ? - ORDER BY length(proof) DESC` - ) - .all(type, PROOF_LENGTH_THRESHOLD) - - if (!long_proofs.length) return - - console.info(`\n--- Long property proofs (type: ${remove_underscores(type)}) ---`) - - for (const { id, property, length } of long_proofs) { - console.warn( - `🟡 The proof for (${id}, ${property}) has ${length} characters. Consider moving it to a content page.` - ) - } -} - -function report_long_implication_proofs(type: StructureType) { - const long_proofs = db - .prepare<[StructureType, number], { id: string; length: number }>( - `SELECT - id, - length(proof) AS length - FROM implications - WHERE - type = ? - AND is_deduced = FALSE - AND length(proof) >= ? - ORDER BY length(proof) DESC` - ) - .all(type, PROOF_LENGTH_THRESHOLD) - - if (!long_proofs.length) return - - console.info(`\n--- Long implication proofs (type: ${remove_underscores(type)}) ---`) - - for (const { id, length } of long_proofs) { - console.warn( - `🟡 The proof for ${id} has ${length} characters. Consider moving it to a content page.` - ) - } -} diff --git a/package.json b/package.json index d7048574..16e1cb59 100644 --- a/package.json +++ b/package.json @@ -23,7 +23,6 @@ "db:update": "pnpm db:seed && pnpm db:deduce && pnpm db:test && pnpm db:snapshot", "db:watch": "tsx --tsconfig database/tsconfig.json database/scripts/watch.ts", "db:redundancies": "tsx --tsconfig database/tsconfig.json database/scripts/redundancies.ts", - "db:proof-length": "tsx --tsconfig database/tsconfig.json database/scripts/proof-length.ts", "e2e": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test", "e2e:debug": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test --debug", "e2e:ui": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test --ui"