diff --git a/.cspell.json b/.cspell.json
index 02064e53..94a0b930 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -323,6 +323,7 @@
"Vincenzo",
"Vite",
"Wedderburn",
+ "Wengenroth",
"well-copowered",
"Yoneda",
"Zulip"
diff --git a/database/data/categories/CMon.yaml b/database/data/categories/CMon.yaml
index 1951443b..e0a67e53 100644
--- a/database/data/categories/CMon.yaml
+++ b/database/data/categories/CMon.yaml
@@ -69,4 +69,4 @@ special_objects:
special_morphisms:
epimorphisms:
description: A morphism in $\CMon$ is an epimorphism iff it is an epimorphism in $\Mon$, which in turn can be characterized by Isbell's zigzag theorem.
- proof: 'If $f : M \to N$ is a homomorphism of commutative monoids which is an epimorphism in $\Mon$, then it is trivially also an epimorphism in $\CMon$. The converse requires a proof, which can be found at MSE/5133488.'
+ proof: 'If $f : M \to N$ is a homomorphism of commutative monoids which is an epimorphism in $\Mon$, then it is trivially also an epimorphism in $\CMon$. The converse requires a proof, which can be found at MSE/5133488.'
diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml
index 7f9f6c25..dc724e40 100644
--- a/database/data/categories/Man.yaml
+++ b/database/data/categories/Man.yaml
@@ -85,7 +85,7 @@ unsatisfied_properties:
proof: If $\Man$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction.
- property: ℵ₂-small copowers
- proof: A proof can be found at MSE/5083641 (ignore the arguments regarding equal dimension).
+ proof: A proof can be found at MSE/5083641 (ignore the arguments regarding equal dimension).
- property: ℵ₁-cofiltered limits
proof: >-
diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml
index 045d1a7b..9b778385 100644
--- a/database/data/categories/Meas.yaml
+++ b/database/data/categories/Meas.yaml
@@ -14,6 +14,7 @@ related:
comments:
- The thread MSE/5024471 asks for the finitely presentable objects of this category.
+ - Will Sawin has sketched a proof for the co-Malcev property in MO/509552.
satisfied_properties:
- property: locally small
@@ -37,6 +38,14 @@ satisfied_properties:
- property: cocomplete
proof: Take the colimit of the underlying sets and take the largest $\sigma$-algebra making all inclusions measurable. That is, a set is measurable iff its preimage under each inclusion is measurable.
+ - property: coregular
+ proof: >-
+ The proof is similar to the proof for $\Top$. We already know that (finite) colimits and equalizers exist, and that they are preserved by the forgetful functor to $\Set$. It remains to show that regular monomorphisms, i.e. embeddings, are stable under pushouts. Thus, let $i : A \to X$ be an embedding and let $f : A \to Y$ be any measurable map. We claim that the induced measurable map
+ $$j : Y \to Y \sqcup_A X$$
+ is again an embedding. It is certainly injective, since $\Set$ is coregular. More precisely, the underlying set of $Y \sqcup_A X$ can be identified with $Y \sqcup (X \setminus \im(i))$. Now let $T \subseteq Y$ be a measurable subset. Then its preimage $f^*(T) \subseteq A$ is measurable. Since $i$ is an embedding, there exists a measurable subset $S \subseteq X$ such that $i^*(S) = f^*(T)$. Let $u : X \to Y \sqcup_A X$ denote the canonical map, so that $u \circ i = j \circ f$, and consider the subset
+ $$M := j_*(T) \cup u_*(S \setminus \im(i))$$
+ of the pushout. It is straightforward to verify that $j^*(M) = T$ and $u^*(M) = S$. Since both $T$ and $S$ are measurable, it follows that $M$ is measurable. Finally, the equality $j^*(M) = T$ shows that every measurable subset of $Y$ is the preimage of a measurable subset of the pushout. Hence $j$ is an embedding, as claimed.
+
- property: countably extensive
proof: >-
This follows from the countable extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and that they are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets, with measurable subsets given by unions of measurable subsets of the summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique $\sigma$-algebra, it follows immediately that coproducts are disjoint in $\Meas$ as well.
@@ -63,9 +72,6 @@ unsatisfied_properties:
- property: skeletal
proof: This is trivial.
- - property: cartesian filtered colimits
- proof: See MSE/5027218.
-
- 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 \Meas$ which equips a set with the trivial $\sigma$-algebra.
@@ -89,7 +95,7 @@ unsatisfied_properties:
proof: >-
Let $X$ be a set of cardinality $> 2^{\aleph_0}$. We equip $X$ with the discrete $\sigma$-algebra. If $1$ denotes the singleton space, we therefore have $X \cong \coprod_{x \in X} 1$ in $\Meas$. However, we claim that the canonical bijective measurable map
$$\textstyle\coprod_{x,y \in X} 1 \to X \times X$$
- is not an isomorphism, i.e. that $X \times X$ does not carry the discrete $\sigma$-algebra. More precisely, we will show that the diagonal $\Delta \subseteq X \times X$ is not measurable. (This is probably standard, but we include the proof here for lack of a reference.)
+ is not an isomorphism, i.e. that $X \times X$ does not carry the discrete $\sigma$-algebra. More precisely, we will show that the diagonal $\Delta \subseteq X \times X$ is not measurable. (This is well-known and is remarked for example at the end of chapter 1 in Wengenroth's book Wahrscheinlichkeitstheorie, but we include the proof nevertheless.)
Assume that $\Delta \subseteq X \times X$ is measurable. Then (cf. MSE/61617) there is a countable family of rectangles $(A_n \times B_n)_{n \in \IN}$ such that $\Delta \in \sigma(\{A_n \times B_n : n \in \IN\})$. Consider the product of the characteristic functions
$$((\chi_{A_n})_n,(\chi_{B_n})_n) : X \to \{0,1\}^{\IN} \times \{0,1\}^{\IN}.$$
@@ -97,6 +103,9 @@ unsatisfied_properties:
Next, consider the collection of all subsets $E \subseteq X \times X$ with the property that, whenever $x \sim y$, we have $(x,y) \in E \iff (x,x) \in E$. It is easily seen that this collection is a $\sigma$-algebra on $X \times X$. Moreover, it contains each rectangle $A_n \times B_n$. Therefore, it also contains the diagonal $\Delta$. But this means that $x \sim y$ implies $x=y$, i.e. that $\sim$ is trivial. This contradiction proves that the diagonal is not measurable.
+ - property: coaccessible
+ proof: 'The proof is very similar to the proof for $\Top$. Assume $\Meas$ is coaccessible. Let $p : D \to I$ be the identity map from the two-element discrete space to the two-element indiscrete space. Then, a measurable space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete measurable 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.'
+
special_objects:
initial object:
description: empty set with the unique $\sigma$-algebra
diff --git a/database/data/categories/Rel.yaml b/database/data/categories/Rel.yaml
index e01269cb..47ecfb7d 100644
--- a/database/data/categories/Rel.yaml
+++ b/database/data/categories/Rel.yaml
@@ -56,7 +56,7 @@ unsatisfied_properties:
proof: This is trivial.
- property: Cauchy complete
- proof: See MSE/1931577.
+ proof: See MSE/1931577.
- property: normal
proof: The construction of equalizers in $\Rel$ shows that they are injective functions, but MSE/350716 shows that monomorphisms in $\Rel$ don't have to be functions.
diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml
index 0386c524..864ce08b 100644
--- a/database/data/categories/Top.yaml
+++ b/database/data/categories/Top.yaml
@@ -46,7 +46,7 @@ satisfied_properties:
proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$.
- property: coregular
- proof: The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the nLab.
+ proof: The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the nLab. Another proof can be found in MSE/2016945.
- property: filtered-colimit-stable monomorphisms
proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$.
diff --git a/database/data/category-implications/Malcev.yaml b/database/data/category-implications/Malcev.yaml
index 4fcd1898..afd52ba8 100644
--- a/database/data/category-implications/Malcev.yaml
+++ b/database/data/category-implications/Malcev.yaml
@@ -32,7 +32,7 @@
- pointed
conclusions:
- unital
- proof: This follows from Corollary 2.2.10 in Malcev, protomodular, homological and semi-abelian categories. The proof is also written down in MSE/5033161.
+ proof: This follows from Corollary 2.2.10 in Malcev, protomodular, homological and semi-abelian categories. The proof is also written down in MSE/5033161.
is_equivalence: false
- id: biproducts_unital
diff --git a/database/data/category-implications/disjoint coproducts.yaml b/database/data/category-implications/disjoint coproducts.yaml
index 52f0d565..44acb2df 100644
--- a/database/data/category-implications/disjoint coproducts.yaml
+++ b/database/data/category-implications/disjoint coproducts.yaml
@@ -41,7 +41,7 @@
- strongly connected
conclusions:
- disjoint finite products
- proof: See MSE/5130190 for a proof.
+ proof: See MSE/5130190 for a proof.
is_equivalence: false
- id: disjoint_coproduct_cogenerator
diff --git a/database/data/category-implications/subobject classifiers.yaml b/database/data/category-implications/subobject classifiers.yaml
index 4efa2fcd..51680f15 100644
--- a/database/data/category-implications/subobject classifiers.yaml
+++ b/database/data/category-implications/subobject classifiers.yaml
@@ -33,7 +33,7 @@
- regular subobject classifier
conclusions:
- trivial
- proof: See MSE/4086192.
+ proof: See MSE/4086192.
is_equivalence: false
- id: regular_subobjects_trivial