diff --git a/content/Meas_not_regular.md b/content/Meas_not_regular.md deleted file mode 100644 index b4f8e72c..00000000 --- a/content/Meas_not_regular.md +++ /dev/null @@ -1,28 +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. -author: Nekoma ---- - -## $\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/separated_objects_quasitopos.md b/content/separated_objects_quasitopos.md new file mode 100644 index 00000000..36e5dd7a --- /dev/null +++ b/content/separated_objects_quasitopos.md @@ -0,0 +1,23 @@ +--- +title: Quasitopoi of Separated Objects +description: Some results concerning the full subcategory of separated objects for a Lawvere-Tierney topology on a topos +author: Daniel Schepler +--- + +## Results Concerning Quasitopoi of Separated Objects + +### Special Morphisms + +::: Lemma 1 +Let $\T$ be an elementary topos with a Lawvere-Tierney topology $j$. Then in the full subcategory $\Sep(j)$ of $j$-separated objects:
+(a) The monomorphisms are the morphisms whose image in $\T$ are monomorphisms.
+(b) The epimorphisms are the morphisms whose image in $\T$ are $j$-dominant (i.e. the image calculated in $\T$ is a $j$-dense subobject of the codomain).
+(c) The regular monomorphisms are the morphisms whose image in $\T$ are $j$-closed monomorphisms.
+(d) The regular epimorphisms are the morphisms whose image in $\T$ are epimorphisms. +::: + +_Proof._ Recall that $\Sep(j)$ is a reflective subcategory of $\T$, where the reflector takes an object $X$ to the quotient $X_{\sep}$ of $X$ by the congruence defined by the $j$-closure of the diagonal in $X\times X$. Also recall that the equalizer of $j, \id : \Omega_\T \rightrightarrows \Omega_\T$ is a $j$-separated object $\Omega_j$ which serves as the regular subobject classifier in $\Sep(j)$, and since $j$ is idempotent, this can also be described as the image (in $\T$) of $j$.
+(a) ($\Rightarrow$) This follows from the fact that $\Sep(j)$ is a reflective subcategory of $\T$. ($\Leftarrow$) This is trivial for any subcategory.
+(b) ($\Rightarrow$) Given a morphism $f : X \to Y$, form the image $\im(f)$ in $\T$, which corresponds to a morphism $\chi_{\im(f)} : Y \to \Omega_\T$. Then $j \circ \chi_{\im(f)} \circ f = j\circ \top_X = \top_X = \top_Y \circ f$ as morphisms $Y \to \Omega_j$, so if $f$ is an epimorphism in $\Sep(j)$, then we conclude $j \circ \chi_{\im(f)} = \top_Y$. However, $j \circ \chi_{\im(f)} : Y \to \Omega_j \hookrightarrow \Omega$ is the characteristic morphism of the $j$-closure of $\im(f)$, so we conclude that $j$-closure is all of $Y$. ($\Leftarrow$) Given a morphism $f : X \to Y$ of $j$-separated objects whose image in $\T$ is $j$-dense, suppose we have two morphisms $g, h : Y \rightrightarrows Z$ with $g \circ f = h \circ f$. Then since $Z$ is $j$-separated, the equalizer of $g$ and $h$ is $j$-closed; it also contains the image of $f$ and thus is $j$-dense. We conclude that the equalizer is all of $Y$.
+(c) ($\Rightarrow$) Any equalizer in $\T$ of $f, g : X \rightrightarrows Y$ with $Y$ $j$-separated is a $j$-closed subobject of $X$. If $X$ is $j$-separated as well, then that equalizer subobject is automatically separated, and agrees with the equalizer in $\Sep(j)$. ($\Leftarrow$) For a $j$-closed subobject $f : X \hookrightarrow Y$, we see that the characteristic morphism in $\T$, $\chi_X : Y \to \Omega_\T$, factors through $\Omega_j$. Now $X$ is the equalizer of $\chi_X, \top : Y \rightrightarrows \Omega_j$.
+(d) ($\Rightarrow$) We can calculate the coequalizer of $f, g : X \rightrightarrows Y$ in $\Sep(j)$ by taking the coequalizer $Z$ in $\T$ and then applying the reflector to get $Z_{sep}$. We see that both $Y \to Z$ and $Z \to Z_{sep}$ are epimorphisms in $\T$. ($\Leftarrow$) Suppose $f : X \to Y$ is an epimorphism in $\T$ of $j$-separated objects. Then the subcategory inclusion functor preserves the kernel pair $X \times_Y X \rightrightarrows X$, and since $f$ is a regular epimorphism in $\T$, this kernel pair has coequalizer $f : X \to Y$ in $\T$. Since $Y$ was already $j$-separated, the kernel pair also has coequalizer $f : X \to Y$ in $\Sep(j)$. $\square$ diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index 80e08f45..ecb5e3fb 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -43,9 +43,6 @@ unsatisfied_properties: - property: cogenerating set proof: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in $\Mon$, which we know does not exist.' - - property: regular - proof: See Example 3.14 at the nLab. - - property: coregular proof: 'We already know that $\Mon$ is not coregular, in fact there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' diff --git a/databases/catdat/data/categories/LRS_R.yaml b/databases/catdat/data/categories/LRS_R.yaml index 9bb3f576..315cc69e 100644 --- a/databases/catdat/data/categories/LRS_R.yaml +++ b/databases/catdat/data/categories/LRS_R.yaml @@ -62,6 +62,7 @@ unsatisfied_properties: - property: regular proof: This is Corollary 4(c) here. + check_redundancy: false - property: cofiltered-limit-stable epimorphisms proof: This is Corollary 4(d) here. diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index d7ce5a65..26e7c004 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -56,9 +56,6 @@ unsatisfied_properties: - property: balanced proof: Take a set $X$ with two different $\sigma$-algebras $\A \subset \B$ (for example, $\A = \{\varnothing,X\}$ and $\B = P(X)$ when $X$ has at least $2$ elements), then the identity map $(X,\B) \to (X,\A)$ provides a counterexample. - - property: Malcev - proof: Use that $\Set$ is not Malcev and endow sets with the trivial $\sigma$-algebra. - - property: cartesian filtered colimits proof: See MSE/5027218. @@ -68,9 +65,6 @@ unsatisfied_properties: - property: effective cocongruences proof: 'The proof is similar to the one for $\Top$: Use the trivial $\sigma$-algebra on a two-point set.' - - property: regular - proof: A proof can be found here. - special_objects: initial object: description: empty set with the unique $\sigma$-algebra diff --git a/databases/catdat/data/categories/Met_oo.yaml b/databases/catdat/data/categories/Met_oo.yaml index ee2171c2..43c0b4dc 100644 --- a/databases/catdat/data/categories/Met_oo.yaml +++ b/databases/catdat/data/categories/Met_oo.yaml @@ -60,9 +60,6 @@ unsatisfied_properties: - property: effective cocongruences proof: The same counterexample as for $\Met$ works here. The difference in this case is that a binary copower of two copies of $(0,1)$ does exist in $\Met_\infty$. However, this would assign a distance of $\infty$ between points in $(-1,0)$ and points in $(0,1)$, which does not agree with the chosen subspace metric on $(-1,0) \cup (0,1)$. - - property: regular - proof: We can take the same counterexample as for $\PMet$. - special_objects: initial object: description: empty metric space diff --git a/databases/catdat/data/categories/Pos.yaml b/databases/catdat/data/categories/Pos.yaml index 5e46bcea..c3986dbd 100644 --- a/databases/catdat/data/categories/Pos.yaml +++ b/databases/catdat/data/categories/Pos.yaml @@ -45,9 +45,6 @@ unsatisfied_properties: - property: balanced proof: The inclusion $\{0,1\} \to \{0 < 1\}$ provides a counterexample (where in the domain there is no relation between $0$ and $1$). - - property: regular - proof: See Example 3.14 at the nLab. - - property: Malcev proof: 'Consider the subposet $\{(a,b) : a \leq b \}$ of $\IN^2$.' diff --git a/databases/catdat/data/categories/Prost.yaml b/databases/catdat/data/categories/Prost.yaml index c120b60d..3346dec3 100644 --- a/databases/catdat/data/categories/Prost.yaml +++ b/databases/catdat/data/categories/Prost.yaml @@ -41,18 +41,12 @@ satisfied_properties: proof: The set $\{0,1\}$ with the chaotic preorder $(0 \leq 1$, $1 \leq 0)$ is a regular subobject classifier since order-preserving maps $P \to \{0,1\}$ correspond to subsets of $P$. unsatisfied_properties: - - property: regular - proof: See Example 3.14 at the nLab. - - property: balanced proof: The inclusion $\{0,1\} \to \{0 < 1\}$ provides a counterexample (where in the domain there is no relation between $0$ and $1$). - property: skeletal proof: This is trivial. - - property: Malcev - proof: 'Consider the subproset $\{(a,b) : a \leq b \}$ of $\IN^2$.' - - property: co-Malcev proof: 'See MO/509552: Consider the forgetful functor $U : \Prost \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index d491880c..3cfb9760 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -55,9 +55,6 @@ unsatisfied_properties: - property: CSP proof: Assume that $\coprod_n \IZ \to \prod_n \IZ$ is an epimorphism in $\Rng$. Then $((\coprod_n \IZ)^+)^{\ab} \to \prod_n \IZ$ would be an epimorphism in $\CRing$, where $(-)^+$ denotes the unitalization and $(-)^{\ab}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\card(S) \leq \card(R)$ by SP/04W0. Since $((\coprod_n \IZ)^+)^{\ab}$ is countable and $\prod_n \IZ$ is not, we get a contradiction. - - property: regular subobject classifier - proof: 'Assume that $\Rng$ has a subobject classifier $\Omega$. Since $0$ is a zero object, every regular subobject $R \subseteq S$ would be the kernel of some homomorphism $S \to \Omega$. In particular, it would be an ideal. Now take any pair of homomorphisms $f,g : S \rightrightarrows T$ in $\Ring$. Their equalizer $R \subseteq S$ is also the equalizer in $\Rng$, and it contains $1 \in S$. If it was an ideal, then $R = S$, and hence $f = g$, which is absurd.' - - property: coregular proof: 'We can copy the proof for $\Ring$. In short, the inclusion of diagonal matrices $\IQ^2 \hookrightarrow M_2(\IQ)$ is a regular monomorphism, but becomes zero after taking the pushout with $p_1 : \IQ^2 \twoheadrightarrow \IQ$ because $M_2(\IQ)$ is simple.' diff --git a/databases/catdat/data/categories/SepPsh(X).yaml b/databases/catdat/data/categories/SepPsh(X).yaml new file mode 100644 index 00000000..ea33e8be --- /dev/null +++ b/databases/catdat/data/categories/SepPsh(X).yaml @@ -0,0 +1,77 @@ +id: SepPsh(X) +name: category of separated presheaves +notation: $\SepPsh(X)$ +objects: separated presheaves of sets on a topological space $X$ +morphisms: morphisms of presheaves +description: Here, we assume that the topological space $X$ is such that there is a non-empty family of open subsets whose union is not in the family, since otherwise this category is almost the category of all presheaves. For a few of the properties, we will strengthen this assumption to the assumption that there are two open subsets $U, V$ such that neither is contained in the other. +nlab_link: https://ncatlab.org/nlab/show/separated+presheaf + +tags: + - algebraic geometry + - topology + +related_categories: + - Sh(X) + - Set + +satisfied_properties: + - property: locally small + proof: This is easy. + + - property: Grothendieck quasitopos + proof: It is equivalent to $\BiSep(\Open(X), J, K)$ where $J$ is the trivial Grothendieck topology and $K$ is the open covering topology. + + - property: cocartesian cofiltered limits + proof: 'Let $c : \F \sqcup \lim_{i\in I} \G_i \to \lim_{i\in I} (\F \sqcup \G_i)$ be the comparison map. Using the description of coproducts below, we see that for non-empty $U$, both sides of $c(U)$ can be calculated component-wise. Therefore, for those $U$, the conclusion follows from the corresponding fact in $\Set$. For $U = \varnothing$, we can see that both sides of $c(\varnothing)$ are empty if and only if $\F(\varnothing) = \varnothing$ and $\G_i(\varnothing) = \varnothing$ for some $i$, and otherwise both sides are a singleton.' + +unsatisfied_properties: + - property: skeletal + proof: Consider the constant presheaves for two non-equal singleton sets. + + - property: disjoint finite coproducts + proof: The equalizer of the two coprojections $1 \rightrightarrows 1 + 1$ has value $1$ at $\varnothing$. + + - property: generator + proof: 'The subcategory $\Sh(X)$ of $\SepPsh(X)$ is reflective by Johnstone Prop A.2.6.12 and A.4.4.4. Therefore, if $\SepPsh(X)$ had a generator then so would $\Sh(X)$, which we know is not the case.' + + - property: effective congruences + proof: >- + Let $\{ U_i : i \in I \}$ be a non-empty family of open sets whose union $U$ is not in the family. In particular, this implies $U \ne \varnothing$. We then consider the relation $\E$ on $\F \coloneqq y_U + y_U '$ where for $x_1, x_2 \in \F(V)$, $(x_1, x_2) \in \E(V)$ if and only if either $x_1 = x_2$ or $V \subseteq U_i$ for some $i \in I$. It is easy to see that $\E$ is a congruence. However, $\E \hookrightarrow \F \times \F$ is not a regular monomorphism: to see this, use the description of regular monomorphisms below, and observe that $(\id_U, \id_U ') \notin \E(U)$ but its restriction is in $\E(U_i)$ for each $i$. On the other hand, any effective congruence would necessarily be an equalizer. + + - property: semi-strongly connected + proof: Let $U$ and $V$ be two open subsets such that neither is contained in the other. Then there is neither a morphism $y_U \to y_V$ nor a morphism $y_V \to y_U$. + + - property: co-Malcev + proof: >- + Let $U$ and $V$ be two open subsets such that neither is contained in the other. We will let $\F \coloneqq y_{U \cup V}$, which represents the functor of sections over $U \cup V$, and then consider the reflexive relation on such sections $a, b \in \G(U \cup V)$ where $a \sim b$ if and only if there exists $c \in \G(U\cup V)$ such that $c |_U = a |_U$ and $c |_V = b |_V$. Note that since $\G$ is separated, such a $z$ is unique if it exists. From this, we can see that this relation is representable by the colimit of a diagram where the objects are $y_U$, $y_V$, and three copies of $y_{U\cup V}$, and the morphisms are canonical morphisms from $y_U$ to the first and third copies of $y_{U\cup V}$ and canonical morphisms from $y_V$ to the second and third copies of $y_{U\cup V}$. In fact, we can see that the presheaf colimit is separated, so this presheaf colimit is also the colimit in $\SepPsh(X)$. + + For a more concrete description of the presheaf colimit $\E$, if $W \not\subseteq U\cup V$, then $\E(W) = \varnothing$. If $W \subseteq U\cup V$ but $W \not\subseteq U$ and $W \not\subseteq V$, then $\E(W) \simeq \{ a_W, b_W, c_W \}$. If $W \subseteq U$ but $W \not\subseteq V$, then $\E(W) \simeq \{ a_W = c_W, b_W \}$; similarly, if $W \subseteq V$ but $W \not\subseteq U$, then $\E(W) \simeq \{ a_W, b_W = c_W \}$. Finally, if $W \subseteq U \cap V$, then $\E(W) \simeq \{ a_W = b_W = c_W \}$. The restriction maps of $\E$ are induced by $a_W \mapsto a_{W'}, b_W \mapsto b_{W'}, c_W \mapsto c_{W'}$. + + Now if $\E$ were cosymmetric, with cosymmetry morphism $s : \E \to \E$, then $c' \coloneqq s(c_{U\cup V}) \in \E(U\cup V)$ would have to satisfy $c' |_U = s(c_{U\cup V} |_U) = s(a_U) = b_U$ and $c' |_V = s(c_{U\cup V} |_V) = s(b_V) = a_V$. However, none of $a_{U\cup V}, b_{U\cup V}, c_{U\cup V}$ satisfies these conditions. + +special_objects: + initial object: + description: empty presheaf sending every open set to $\varnothing$ + terminal object: + description: constant presheaf with value a singleton + coproducts: + description: take the section-wise disjoint union, and then collapse the value at $\varnothing$ to a singleton if it is non-empty + products: + description: section-wise defined direct product + +special_morphisms: + isomorphisms: + description: morphisms of separated presheaves that are bijective on every open set + proof: This is easy. + monomorphisms: + description: morphisms of separated presheaves that are injective on every open set + proof: This is a corollary of Lemma 1(a) here. + epimorphisms: + description: 'morphisms of separated presheaves $\varphi : \F \to \G$ which are "locally surjective": for every local section $g \in \G(U)$ there is an open covering $\bigcup_{i\in I} U_i = U$ such that each $g|_{U_i} \in \G(U_i)$ is contained in the image of $\varphi(U_i) : \F(U_i) \to \G(U_i)$' + proof: This is a corollary of Lemma 1(b) here. + regular monomorphisms: + description: 'morphisms of separated presheaves $\varphi : \F \hookrightarrow \G$ that are injective on every open set, and such that "every section of $\G$ which is locally in $\F$ is itself in $\F$": if a local section $g \in \G(U)$ has an open covering $\bigcup_{i\in I} U_i = U$ such that each $g|_{U_i} \in \G(U_i)$ is contained in the image of $\varphi(U_i) : \F(U_i) \to \G(U_i)$, then $g$ is contained in the image of $\varphi(U) : \F(U) \to \G(U)$' + proof: This is a corollary of Lemma 1(c) here. + regular epimorphisms: + description: morphisms of separated presheaves that are surjective on every open set + proof: This is a corollary of Lemma 1(d) here. diff --git a/databases/catdat/data/categories/Sh(X).yaml b/databases/catdat/data/categories/Sh(X).yaml index 507d4795..c8d0d4e7 100644 --- a/databases/catdat/data/categories/Sh(X).yaml +++ b/databases/catdat/data/categories/Sh(X).yaml @@ -14,6 +14,7 @@ related_categories: - Set - SetxSet - Sh(X,Ab) + - SepPsh(X) comments: - It is likely that none of the currently remaining unknown properties (locally ℵ₁-presentable, exact filtered colimits, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$. diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index c6a2b274..db13dc52 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -63,18 +63,12 @@ unsatisfied_properties: - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits, see MSE/1255678.' - - property: regular - proof: See Example 3.14 at the nLab. - - property: accessible proof: In fact, it does not have any small colimit-dense subcategory by MSE/4097315. For a related result, see MO/288648. - property: coaccessible proof: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete 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: Malcev - proof: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces. - - property: co-Malcev proof: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' diff --git a/databases/catdat/data/category-implications/congruences.yaml b/databases/catdat/data/category-implications/congruences.yaml index d3dc5a24..7550cbeb 100644 --- a/databases/catdat/data/category-implications/congruences.yaml +++ b/databases/catdat/data/category-implications/congruences.yaml @@ -111,6 +111,36 @@ Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is Example 2.2.18 in Malcev, protomodular, homological and semi-abelian categories. An alternative proof of this special case is given later in A.5.17. is_equivalence: false +- id: regular_extensive_consequences + assumptions: + - extensive + - regular + - quotients of congruences + conclusions: + - effective cocongruences + proof: >- + Suppose $p : X+X' \twoheadrightarrow E$ is a cocongruence, with coreflexivity morphism $r : E \to X$ and cotransitivity morphism $t : E \to E +_X E'$. (Here $X'$ is an isomorphic copy of $X$; $E'$ is an isomorphic copy of $E$; and $E +_X E'$ is the coproduct modulo the relations $p(x') = p(x)'$, i.e. it is equivalent to the pushout of $E \xleftarrow{p\circ i_2} X \xrightarrow{p\circ i_1} E$. Since both these morphisms are (split) monomorphisms, the pushout exists by this result.) + + We now claim that we have pullback diagrams + $$\begin{CD} + X @> p \circ i_1 >> E @. \quad @. X' @> p \circ i_2 >> E \\ + @V p \circ i_1 VV @VV t V @. @V p \circ i_2 VV @VV t V \\ + E @> i_1 >> E +_X E' @. \quad @. E' @> i_2 >> E +_X E'. + \end{CD}$$ + For the left diagram, suppose we have generalized elements $e_1, e_2 \in E$ such that $t(e_1) = i_1(e_2) \in E +_X E'$. Then we have two retractions of $t$, $s_1 : E +_X E' \to E$, defined by $e \mapsto p(r(e)), e' \mapsto e'$; and $s_2 : E +_X E' \to E$, defined by $e \mapsto e, e' \mapsto p(r(e)')$. To check for instance that $s_1$ is a retraction, note that $s_1(t(p(x))) = s_1(p(x)) = p(r(p(x)) = p(x)$ and $s_1(t(p(x'))) = s_1(p(x')') = p(x')$ and then use the assumption that $p$ is an epimorphism; the proof for $s_2$ is similar. Therefore, $e_1 = s_1(t(e_1)) = s_1(i_1(e_2)) = p(r(e_2))$. On the other hand, $e_1 = s_2(t(e_1)) = s_2(i_1(e_2)) = e_2$. Therefore, $e_1 = e_2 = p(r(e_2))$, so the generalized element $r(e_2)$ of $X$ maps to $e_1$ and $e_2$ respectively as required. On the other hand, since $p\circ i_1 : X \to E$ is a (split) monomorphism, the uniqueness of the generalized element of $X$ is automatic, completing the proof that the left diagram is a pullback square. The proof for the right diagram is similar. + + Now, using extensivity, we can combine these into a pullback diagram + $$\begin{CD} + X+X' @> p >> E \\ + @VVV @VV t V \\ + E+E' @>>> E +_X E'. + \end{CD}$$ + Since both morphisms $X \to E$ and $X \to E'$ used in the pushforward are monomorphisms, by the construction here, the morphism $E+E' \to E +_X E'$ is a regular epimorphism. Therefore, by the assumption that the category is regular, we have that $p$ is in fact a regular epimorphism. + + From here, essentially the same argument as in this proof applies to show that $E$ is effective. + + is_equivalence: false + - id: pretopos_balanced assumptions: - effective congruences diff --git a/databases/catdat/data/category-implications/topos.yaml b/databases/catdat/data/category-implications/topos.yaml index 80d56add..c91f053a 100644 --- a/databases/catdat/data/category-implications/topos.yaml +++ b/databases/catdat/data/category-implications/topos.yaml @@ -32,10 +32,10 @@ - id: topos_implies_coregular assumptions: - - elementary topos + - quasitopos conclusions: - coregular - proof: This is proven in Johnstone, A2.6.3 (for every quasitopos). + proof: This is proven in Johnstone, A2.6.3. is_equivalence: false - id: grothendieck_topos_definition @@ -70,12 +70,15 @@ - id: topos_no_stable_epis assumptions: - - elementary topos + - quasitopos - cofiltered-limit-stable epimorphisms - countable coproducts conclusions: - - trivial - proof: Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$. + - thin + proof: >- + Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. Now let $\bar 0$ be the coimage of the unique morphism $0 \to 1$, so that we get a factorization $0 \twoheadrightarrow \bar 0 \hookrightarrow 1$ where $0 \twoheadrightarrow \bar 0$ is an epimorphism and $\bar 0 \to 1$ is a regular monomorphism. Then since $\bar 0$ is a quotient of $0$, the coslice over $\bar 0$ is equivalent to a full subcategory. Moreover, the coslice is again a quasitopos with countable coproducts, and the inclusion functor preserves and reflects limits and inhabited colimits. In fact, this coslice is also a solid quasitopos (meaning exactly that the unique morphism from its initial object $\bar 0$ to its terminal object $1$ is a regular monomorphism), which implies that it has disjoint finite coproducts by Johnstone, ???. Since the coslice is locally cartesian closed, we conclude that it is countably extensive. Also, each $N_{\geq n}$ is in the coslice. From this, we can conclude that $\lim_n N_{\geq n} \simeq \bar 0$ in the coslice, and therefore also in the original quasitopos. + + There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. Thus, $0 \to 1$ is an epimorphism. It follows that for any parallel pair $f, g : X \rightrightarrows Y$, the corresponding morphisms $1 \rightrightarrows [X, Y]$ are equal, so that $f = g$. is_equivalence: false - id: pretopos_definition @@ -86,3 +89,68 @@ - extensive proof: This is true by definition. is_equivalence: true + +- id: quasitopos_definition + assumptions: + - quasitopos + conclusions: + - finitely complete + - finitely cocomplete + - locally cartesian closed + - regular subobject classifier + proof: This is true by definition. + is_equivalence: true + +- id: quasitopos_consequence + assumptions: + - quasitopos + conclusions: + - effective cocongruences + proof: >- + Suppose $p : X+X' \rightrightarrows E$ is a cocongruence, with coreflexivity morphism $r : E \to X$ and cotransitivity morphism $t : E \to E +_X E'$. (Here $X'$ is an isomorphic copy of $X$; $E'$ is an isomorphic copy of $E$; and $E +_X E'$ is the coproduct modulo the relations $p(x') = p(x)'$, i.e. it is equivalent to the pushout of $E \xleftarrow{p\circ i_2} X \xrightarrow{p\circ i_1} E$.) Now by Johnstone, ???, the quasitopos is equivalent to a comma category $H \mathop{\downarrow} F$ where $H$ is the poset category of a Heyting algebra, and $F : H \to S$ is a functor from $H$ to a solid quasitopos $S$ (meaning a quasitopos in which $! : 0 \to 1$ is a regular monomorphism). However, since we have morphisms $X \to E$ and $E \to X$, we see that the $H$-components of $X$ and $E$ are isomorphic, and similarly for $E +_X E'$. Therefore, we may work in the full subcategory with constant $H$-component $X_H = E_H$; this is equivalent to the slice category $S / F(X_H)$ which is again a solid quasitopos. This shows that without loss of generality, we may assume the original quasitopos is solid; and therefore, by Johnstone, ???, the quasitopos has disjoint coproducts and is therefore extensive. However, in that subcategory, this result applies to show that $E$ is an effective cocongruence; and since the inclusion functor into the original quasitopos preserves inhabited limits and inhabited colimits, we see that $E$ is effective in the original quasitopos as well. + is_equivalence: false + +- id: balanced_quasitopos_is_topos + assumptions: + - quasitopos + - balanced + conclusions: + - elementary topos + proof: This is proven in Johnstone, A2.6.3. + is_equivalence: false + +- id: Giraud_for_quasitopos + assumptions: + - Grothendieck quasitopos + conclusions: + - quasitopos + - locally presentable + proof: See Johnstone, C2.2.13, which proves that a category is a Grothendieck quasitopos if and only if it is a locally essentially small, cocomplete quasitopos with a small strong generating set, which in turn is equivalent to the category being locally presentable and locally cartesian closed, such that all regular congruences are effective. (Note that Johnstone uses "small generating set" in the statement, but Johnstone's definition of "generating set" matches what would usually be called a "strong generating set", or "extremal generating set" in the terminology of nLab.) This is sufficient to establish the forward implication. For the reverse implication, note that any locally presentable category is locally essentially small and cocomplete; and it has a small strong generating set by Adamek-Rosicky, Theorem 1.20 in Chapter 1. + is_equivalence: true + +- id: Malcev_quasitopos_is_thin + assumptions: + - regular subobject classifier + - Malcev + conclusions: + - thin + proof: 'By a proof similar to this we conclude that every regular monomorphism is an isomorphism. Applying this to the equalizer of any parallel pair $f, g : X \rightrightarrows Y$, we conclude that $f = g$.' + is_equivalence: false + +- id: Grothendieck_quasitopos_consequences + assumptions: + - Grothendieck quasitopos + conclusions: + - exact filtered colimits + - cogenerator + proof: >- + To show that a Grothendieck quasitopos has exact filtered colimits, note that $\BiSep(\C, J, K)$ is a reflective subcategory of $\Sh(\C, J)$, with the reflector preserving finite limits. (This is a special case of the more general situation of $\Sep(j)$ being a reflective subcategory of $\T$ whenever $j$ is a Lawvere-Tierney topology on an elementary topos $\T$ with the reflector preserving finite limits.) The result follows from Lemma 3 here. + + As for having a cogenerator: we have that $\Sh(\C, K)$ is a reflective subcategory of $\BiSep(\C, J, K)$, with the reflector being the restriction of the $K$-sheafification functor to the subcategory $\BiSep(\C, J, K)$. Also, recall in general that if $\F$ is a presheaf on $\C$, then the morphism $\F \to \F^+_K$ has $K$-dense presheaf image, and if $\F$ is $K$-separated then the morphism $\F \to \F^+_K$ is a monomorphism. Thus, for $\F$ an object of $\BiSep(\C, J, K)$, the morphism $\eta_\F : \F \to \F^+_K$ is both a monomorphism and an epimorphism in $\BiSep(\C, J, K)$. Now, let $Q$ be a cogenerator of the Grothendieck topos $\Sh(\C, K)$, and suppose we have a parallel pair of morphisms $f, g : \F \rightrightarrows \G$ in $\BiSep(\C, J, K)$ such that $f \ne g$. Then since $\eta_\G : \G \to \G^+_K$ is a monomorphism, we have $f^+ \ne g^+$. Therefore, there exists $h : \G^+_K \to Q$ such that $h \circ f^+_K \ne h \circ g^+_K$. Since $\eta_\F$ is an epimorphism, we conclude $h \circ f^+_K \circ \eta_\F \ne h \circ g^+_K \circ \eta_G$, and thus $h \circ \eta_\G \circ f \ne h \circ \eta_\G \circ g$. + + $$\begin{CD} + \F @> f > g > \G \\ + @V \eta_\F VV @V \eta_\G VV \\ + \F^+_K @> f^+_K > g^+_K > \G^+_K @> h >> Q + \end{CD}$$ + is_equivalence: false diff --git a/databases/catdat/data/category-properties/Grothendieck quasitopos.yaml b/databases/catdat/data/category-properties/Grothendieck quasitopos.yaml new file mode 100644 index 00000000..3a4ecadc --- /dev/null +++ b/databases/catdat/data/category-properties/Grothendieck quasitopos.yaml @@ -0,0 +1,11 @@ +id: Grothendieck quasitopos +relation: is a +description: Given a small category $\C$ with a pair of Grothendieck topologies $J \subseteq K$, we define $\BiSep(\C, J, K)$ to be the full subcategory of presheaves on $\C$ which are both a sheaf for the $J$ topology and also separated for the $K$ topology. A Grothendieck quasitopos is a category which is equivalent to $\BiSep(\C, J, K)$ for some $\C, J, K$. Equivalently, a category is a Grothendieck quasitopos if and only if it is equivalent to the full subcategory of separated objects for a Lawvere-Tierney topology on a Grothendieck topos. For the equivalence, see Johnstone, C2.2.13. +nlab_link: https://ncatlab.org/nlab/show/quasitopos +invariant_under_equivalences: true + +related_properties: + - quasitopos + - Grothendieck topos + - elementary topos + - locally presentable diff --git a/databases/catdat/data/category-properties/Grothendieck topos.yaml b/databases/catdat/data/category-properties/Grothendieck topos.yaml index 6c05d94a..5e4ae1c7 100644 --- a/databases/catdat/data/category-properties/Grothendieck topos.yaml +++ b/databases/catdat/data/category-properties/Grothendieck topos.yaml @@ -6,3 +6,4 @@ invariant_under_equivalences: true related_properties: - elementary topos + - Grothendieck quasitopos diff --git a/databases/catdat/data/category-properties/elementary topos.yaml b/databases/catdat/data/category-properties/elementary topos.yaml index 5686a0f4..a7e96bd0 100644 --- a/databases/catdat/data/category-properties/elementary topos.yaml +++ b/databases/catdat/data/category-properties/elementary topos.yaml @@ -11,3 +11,5 @@ related_properties: - natural numbers object - subobject classifier - pretopos + - quasitopos + - Grothendieck quasitopos diff --git a/databases/catdat/data/category-properties/quasitopos.yaml b/databases/catdat/data/category-properties/quasitopos.yaml new file mode 100644 index 00000000..fe5c4d36 --- /dev/null +++ b/databases/catdat/data/category-properties/quasitopos.yaml @@ -0,0 +1,17 @@ +id: quasitopos +relation: is a +description: >- + A quasitopos is a category which is finitely complete, finitely cocomplete, locally cartesian closed, and has a regular subobject classifier. This gives the category properties similar to those of an elementary topos; a major difference is that a quasitopos need not be balanced. + + Note that some authors use a strong subobject classifier in place of a regular subobject classifier in the definition, i.e. a morphism $\top : 1 \to \Omega$ which classifies strong monomorphisms. For the equivalence of these definitions, see MSE/4335533. +nlab_link: https://ncatlab.org/nlab/show/quasitopos +invariant_under_equivalences: true + +related_properties: + - finitely complete + - finitely cocomplete + - locally cartesian closed + - regular subobject classifier + - elementary topos + - Grothendieck quasitopos + - balanced diff --git a/databases/catdat/data/category-properties/regular subobject classifier.yaml b/databases/catdat/data/category-properties/regular subobject classifier.yaml index fda2e901..590189f3 100644 --- a/databases/catdat/data/category-properties/regular subobject classifier.yaml +++ b/databases/catdat/data/category-properties/regular subobject classifier.yaml @@ -12,3 +12,4 @@ invariant_under_equivalences: true related_properties: - finitely complete - subobject classifier + - quasitopos diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 64b607a5..bc65344e 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -18,6 +18,7 @@ \D: \mathcal{D} \E: \mathcal{E} \F: \mathcal{F} +\G: \mathcal{G} \I: \mathcal{I} \J: \mathcal{J} \O: \mathcal{O} @@ -49,7 +50,6 @@ \im: \operatorname{im} \lcm: \operatorname{lcm} \Spec: \operatorname{Spec} -\Sh: \operatorname{Sh} \ord: \operatorname{ord} \diag: \operatorname{diag} \Sub: \operatorname{Sub} @@ -61,6 +61,7 @@ \cod: \operatorname{cod} \rank: \operatorname{rank} \Gal: \operatorname{Gal} +\Open: \operatorname{Open} # categories \Set: \mathbf{Set} @@ -120,3 +121,7 @@ \Isom: \mathbf{Isom} \Pair: \mathbf{Pair} \Span: \mathbf{Span} +\Sh: \mathbf{Sh} +\Sep: \mathbf{Sep} +\BiSep: \mathbf{BiSep} +\SepPsh: \mathbf{SepPsh} diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 8e906067..08f365c3 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -169,5 +169,7 @@ "subobject-trivial": false, "quotient-trivial": false, "locally finite": false, - "pretopos": false + "pretopos": false, + "quasitopos": false, + "Grothendieck quasitopos": false } diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 5596e679..658bf742 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -112,6 +112,8 @@ "ℵ₂-small powers": true, "ℵ₂-small copowers": true, "pretopos": true, + "quasitopos": true, + "Grothendieck quasitopos": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index 8da72ea9..47a69a18 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -169,5 +169,7 @@ "locally finite": false, "Barr-coexact": false, "Barr-exact": false, - "pretopos": false + "pretopos": false, + "quasitopos": false, + "Grothendieck quasitopos": false }